At the INRIA Sophia-Antipolis (France), a PhD position for three years is available on a research project devoted to
Code-based techniques for proved provable cryptography
Starting date of this PhD position: as soon as possible.

No matter how carefully crafted cryptographic systems are, experience has shown that effective attacks can remain hidden for years. Thus, cryptographers increasingly advocate provable security, where new systems are published with a rigorous definition of their security goals and a mathematical proof that they meet their goals. While the adoption of provable security significantly enhances confidence in cryptosystems, the increasing complexity and diversity of the and diversity tends to increase, the community has become aware that the point has been reached where it is no longer viable to construct or verify cryptographic proofs by hand. Shoup [Shoup04] Bellare and Rogaway [BeRo04], and [Halevi05] advocate the construction of cryptographic proofs as sequences of probabilistic games as a natural solution for taming the complexity of the task. The basic idea of these works is to use a fully-specified programming language to code those games and to use language-based techniques (observational equivalence, program transformations) for manipulating and reasoning about them.

Detailed description

The objective of the thesis is to provide the necessary infrastructure to formalize game-based proofs, and to use the infrastructure to prove the correctness of cryptographic schemes and information flow type systems for languages with cryptographic primitives. During the first year of the thesis, the objective is to contribute to the formalization of a probabilistic programming language of games, to develop the machinery required for game-based proofs (e.g. reflective tactics that synthesize necessary conditions for guaranteeing observational equivalence) and to formalize a library of security properties expressed in a game-based setting. The objective of the second year is to develop tactics for the game transformations described in [BeRo04] (thus dealing with program optimizations, as well transformations specific to game-based proofs). In order to validate the applicability of the setting, the student shall simultaneously perform small-size case studies. At the end of the second year, a formalization of security proofs of selected cryptographic schemes should be complete. The objective of the third year is to extend these results to the verification of cryptographic protocols.

We also expect the student to be marginally involved in machine checking proofs of computational soundness of information flow type systems for languages with cryptographic primitives, since many of the libraries that will be developed by the student will also be useful for this purpose.

At the end of the thesis, the student will have a double expertise in cryptography and machine-checked proofs using the Coq proof assistant, and have published in conferences in cryptography, programming languages, and verification.

Candidates should preferrely have experience in using Coq or similar proof assistants. Background knowledge in cryptography is greatly appreciated but not required.

Relevant literature

[Shoup04] V. Shoup. Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332. November 2004. [http://eprint.iacr.org/2004/332.pdf]

[BeRo04] M. Bellare and P. Rogaway. The security of triple encryption and a framework for code-based game-playing proofs. /Advances in Cryptology/ Eurocrypt 2006, LNCS 4004, Springer, pp. 409-426, 2006. [http://eprint.iacr.org/2004/331.pdf]

[Halevi05] S. Halevi. A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181. June 2005. [http://eprint.iacr.org/2005/181.pdf]

Information and application
For further information about these positions please contact either:

Gilles Barthe      Gilles.Barthe@sophia.inria.fr
Benjamin Grégoire      Benjamin.Gregoire@sophia.inria.fr