CryptoVerif: Cryptographic protocol verifier in the computational model

Project leader:

Project participant:

• secrecy;
• correspondences, which include in particular authentication.

The generated proofs are proofs by sequences of games, as used by cryptographers. These proofs are valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. CryptoVerif can also evaluate the probability of success of an attack against the protocol as a function of the probability of breaking each cryptographic primitive and of the number of sessions (exact security).

This prover is available below. This software is under development; please use it at your own risk. Comments and bug reports welcome.

Source download

Binary download

Mailing List

• To subscribe to the list, send an email to sympa-AT-inria.fr (replace -AT- with @) with subject "subscribe cryptoverif <your name>" (without quotes).
• To post on the list, send an email to cryptoverif-AT-inria.fr (replace -AT- with @. Note: to avoid spam, you must subscribe to the list in order to be allowed to post.)

Applications of CryptoVerif

• security proof of the FDH signature scheme (with David Pointcheval)
• Kerberos (with Aaron D. Jaggard, Andre Scedrov, and Joe-Kai Tsay)
• OEKE, One Encrypted Key Exchange

References of papers that use CryptoVerif

Publications on this topic

[1]

David Cadé and Bruno Blanchet. From Computationally-Proved Protocol Specifications to Implementations and Application to SSH. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), 4(1):4-31, March 2013. Special issue ARES'12.

[2]

David Cadé and Bruno Blanchet. Proved Generation of Implementations from Computationally-Secure Protocol Specifications. In David Basin and John Mitchell, editors, 2nd Conference on Principles of Security and Trust (POST 2013), volume 7796 of Lecture Notes in Computer Science, pages 63-82, Rome, Italy, March 2013. Springer.

[3]

David Cadé and Bruno Blanchet. From Computationally-proved Protocol Specifications to Implementations. In 7th International Conference on Availability, Reliability and Security (AReS 2012), pages 65-74, Prague, Czech Republic, August 2012. IEEE.

[4]

Bruno Blanchet. Automatically Verified Mechanized Proof of One-Encryption Key Exchange. In 25th IEEE Computer Security Foundations Symposium (CSF'12), pages 325-339, Cambridge, MA, USA, June 2012. IEEE.

[5]

Bruno Blanchet. Mechanizing Game-Based Proofs of Security Protocols. In Tobias Nipkow, Olga Grumberg, and Benedikt Hauptmann, editors, Software Safety and Security - Tools for Analysis and Verification, volume 33 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 1-25. IOS Press, May 2012. Proceedings of the summer school MOD 2011.

[6]

Bruno Blanchet. Automatically verified mechanized proof of one-encryption key exchange. Cryptology ePrint Archive, Report 2012/173, April 2012. Available at http://eprint.iacr.org/2012/173.

[7]

Bruno Blanchet. A second look at Shoup's lemma. In Workshop on Formal and Computational Cryptography (FCC 2011), Paris, France, June 2011.

[8]

Bruno Blanchet and David Pointcheval. The computational and decisional Diffie-Hellman assumptions in CryptoVerif. In Workshop on Formal and Computational Cryptography (FCC 2010), Edimburgh, United Kingdom, July 2010.

[9]

Bruno Blanchet, Aaron D. Jaggard, Jesse Rao, Andre Scedrov, and Joe-Kai Tsay. Refining Computationally Sound Mechanized Proofs for Kerberos. In Workshop on Formal and Computational Cryptography (FCC 2009), Port Jefferson, NY, July 2009.

[10]

Martín Abadi (invited speaker), Bruno Blanchet, and Hubert Comon-Lundh. Models and Proofs of Protocol Security: A Progress Report. In Ahmed Bouajjani and Oded Maler, editors, 21st International Conference on Computer Aided Verification (CAV'09), volume 5643 of Lecture Notes in Computer Science, pages 35-49, Grenoble, France, June 2009. Springer.

[11]

Bruno Blanchet. Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire. Automatic verification of security protocols: formal model and computational model. Mémoire d'habilitation à diriger des recherches, Université Paris-Dauphine, November 2008. En français avec publications en anglais en annexe. In French with publications in English in appendix.

[12]

Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, and Joe-Kai Tsay. Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos. In ACM Symposium on Information, Computer and Communications Security (ASIACCS'08), pages 87-99, Tokyo, Japan, March 2008. ACM.

[13]

Bruno Blanchet. A Computationally Sound Mechanized Prover for Security Protocols. IEEE Transactions on Dependable and Secure Computing, 5(4):193-207, October-December 2008. Special issue IEEE Symposium on Security and Privacy 2006. Electronic version available at http://doi.ieeecomputersociety.org/10.1109/TDSC.2007.1005.

[14]

Bruno Blanchet. CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols. In Dagstuhl seminar Formal Protocol Verification Applied, October 2007.

[15]

Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, and Joe-Kai Tsay. Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos. In Dagstuhl seminar Formal Protocol Verification Applied, October 2007.

[16]

Bruno Blanchet. Computationally Sound Mechanized Proofs of Correspondence Assertions. In 20th IEEE Computer Security Foundations Symposium (CSF'07), pages 97-111, Venice, Italy, July 2007. IEEE.

[17]

Bruno Blanchet. Computationally sound mechanized proofs of correspondence assertions. Cryptology ePrint Archive, Report 2007/128, April 2007. Available at http://eprint.iacr.org/2007/128.

[18]

Bruno Blanchet and David Pointcheval. Automated Security Proofs with Sequences of Games. In Cynthia Dwork, editor, CRYPTO'06, volume 4117 of Lecture Notes in Computer Science, pages 537-554, Santa Barbara, CA, August 2006. Springer.

[19]

Bruno Blanchet. A Computationally Sound Mechanized Prover for Security Protocols. In IEEE Symposium on Security and Privacy, pages 140-154, Oakland, California, May 2006.

[20]

Bruno Blanchet and David Pointcheval. Automated security proofs with sequences of games. Cryptology ePrint Archive, Report 2006/069, February 2006. Available at http://eprint.iacr.org/2006/069.

[21]

Bruno Blanchet. A computationally sound mechanized prover for security protocols. Cryptology ePrint Archive, Report 2005/401, November 2005. Available at http://eprint.iacr.org/2005/401.

[22]

Bruno Blanchet. A Computationally Sound Automatic Prover for Cryptographic Protocols. In Workshop on the link between formal and computational models, Paris, France, June 2005.

Support of the CryptoVerif project