The Coq mailing list

[Benjamin Gregoire <Benjamin.Gregoire AT sophia.inria.fr>]

PhD Position: Code-based techniques for proved provable cryptography
===========================================================================================

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.

      


Background information
============================================================================================

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 AT sophia.inria.fr
 Benjamin Grégoire     
Benjamin.Gregoire AT sophia.inria.fr