Combining program generation and formal proof verification, we are now able to discover new cryptographic systems and prove their resistance to many classes of attacks.
Alan Turing's legacy in computer science spans many domains including: computability theory, cryptology, and foundations of software engineering. These three domains contribute to recent results with exciting implications for the study of cryptographic systems. In work started six years ago, Gilles Barthe, César Kunz (initially at INRIA, now at IMDEA, Madrid), Benjamin Grégoire, Sylvain Heraud (INRIA), Yassine Lakhnech (University of Grenoble), and Santiago Zanella-Béguelin (initially at INRIA, now at Microsoft Research) have developed several methods to study cryptographic systems with increasing levels of automation.
This joint research effort has resulted in new tools for the design and study of cryptographic systems. The traditional approach, which relies on pen-and-paper exploration and human reviewing to design and build trust in cryptographic systems, is not only seriously flawed, as shown by the many errors routinely discovered in published proofs, but also hopelessly ineffective given the myriad of design possibilities for cryptographic systems. This research aims at speeding up the process of both exploring new designs and verifying their robustness.
The research started by developing libraries for the Coq interactive theorem prover that capture precisely the mathematical notions that serve as foundations to prove that, for instance, an encryption algorithm preserves the confidentiality of messages. These notions build on programming language theory, because a language is needed to describe cryptographic systems and the possible attacks against them. This also requires some computability theory, because feasible attacks can only make use of "reasonable" amounts of resources (time and memory). All this must also be combined with probability theory, because cyptographic systems are probabilistic in nature and they must hold against attacks that succeed despite a small probability of success - as the old adage goes: "attacks always get better, they never get worse".
The library that they obtained, called CertiCrypt, made it possible to verify formally the proofs of known cryptographic systems, interacting with the Coq theorem prover to develop the proofs. Significant results obtained in this manner include proofs of the security of the widely deployed OAEP encryption scheme and the Full-Domain Hash signature scheme [1,2].
The experience and firm foundations gathered from CertiCrypt, led to a new tool, EasyCrypt, which greatly automates the task of building proofs by relying on automated, rather than interactive, theorem provers. As an added benefit, this also requires less expertise and effort from users. This technology relies on two languages: one to describe cryptographic systems and attacks, and one to describe proofs of security. Proofs are by reduction and structured as sequences of games played between a challenger and an attacker. The initial game encodes the security goal, while the final game encodes a problem assumed to be computationally hard. The final statement gives an upper bound on the winning probability of the attacker in the initial game as a function of the probability of solving the problem encoded in the last game. An impressive outcome of this approach is a machine-checked proof of the Cramer-Shoup encryption scheme, which previously seemed inaccessible to formal analysis. This work received the best paper award at the CRYPTO 2011 conference [3].
The latest advances have evolved from studying individual cryptographic systems to studying whole families of systems. Encryption schemes, for instance, are generally built by combining a few basic blocks in a few possible ways. All possible combinations can be represented as a formal language, which makes it possible to systematically explore each of them and analyze their security. Most schemes turn out to be weak (they are vulnerable to known attacks), but others are secure; for many of these, an independently verifiable proof in EasyCrypt can be generated automatically. This new development, which is pending publication, gives a systematic way to discover new cryptographic systems with nice properties and machine-checked proofs.
With the help of Yves Bertot, Inria
Link:
http://easycrypt.gforge.inria.fr/
References:
[1] G. Barthe et al.: “Formal Certification of Code-Based Cryptographic Proofs”, in proceedings of POPL 2009, ACM 2009, pp.90-101, http://dx.doi.org/ 10.1145/1480881.1480894
[2] G. Barthe et al.: Beyond Provable Security. Verifiable IND-CCA Security of OAEP ", in Proceedings "Topics in Cryptology - CT-RSA 2011", Springer LNCS vol. 6558, pp. 180-196, 2011
[3] G. Barthe et al.: "Computer-Aided Security Proofs for the Working Cryptographer" in proceedings "Advances in Cryptology - CRYPTO 2011", Springer LNCS vol. 6841, pp. 71-90 (Best Paper Award)
Please contact:
Benjamin Grégoire
Inria, France
E-mail:
