CryptoVerif: Cryptographic protocol verifier in the computational model

.

Project leader:

Bruno Blanchet

Project participants:

Charlie Jacomme, Benjamin Lipp

Former participant:

David Cadé

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

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).

It also provides translations of protocol models to OCaml for generating implementations and to F* for generating implementations and reasoning about them, and a translation of assumptions on primitives to EasyCrypt for proving them from lower-level or more standard assumptions.

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

Detailed description of CryptoVerif (semantics of the language, security properties, game transformations).

Tutorial

Another tutorial, by Marc Hafner

Another tutorial, by Charlie Jacomme and Benjamin Lipp

Downloads

• Source: CryptoVerif version 2.08pl1, sources under the CeCILL-B license (gzipped tar file)
• Binary: CryptoVerif version 2.08pl1 for Windows, binaries under the CeCILL-B license (zip file)
• Reference manual

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) or use this web form.
• 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
• SSH (with David Cadé; scripts in subdirectory implementation/ssh of the CryptoVerif distribution)
• Signal (a.k.a. TextSecure, with Nadim Kobeissi and Karthikeyan Bhargavan)
• TLS 1.3 Draft 18 (with Karthikeyan Bhargavan and Nadim Kobeissi)
• ARINC 823 avionic protocols
• WireGuard VPN protocol (with Benjamin Lipp and Karthikeyan Bhargavan)
• Dynamic key compromise
• Translation of CryptoVerif assumptions to EasyCrypt (with Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub)

References of papers that use CryptoVerif

Publications on this topic

[1]

Bruno Blanchet. Dealing with Dynamic Key Compromise in CryptoVerif. In Proceedings of the 37th IEEE Computer Security Foundations Symposium (CSF'24), Enschede, The Netherlands, July 2024. IEEE. To appear.

[2]

Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, and Pierre-Yves Strub. CV2EC: Getting the Best of Both Worlds. In Proceedings of the 37th IEEE Computer Security Foundations Symposium (CSF'24), Enschede, The Netherlands, July 2024. IEEE. To appear.

[3]

Bruno Blanchet. Cryptoverif: a computationally-sound security protocol verifier (initial version with communication on channels). Research report RR-9525, Inria, October 2023. Available at https://inria.hal.science/hal-04246199.

[4]

Bruno Blanchet and Charlie Jacomme. Cryptoverif: a computationally-sound security protocol verifier. Research report RR-9526, Inria, October 2023. Available at https://inria.hal.science/hal-04253820.

[5]

Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and Francois-Xavier Standaert, editors, Eurocrypt 2021, volume 12696 of Lecture Notes in Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.

[6]

Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, and Doreen Riepel. Analysing the HPKE standard. Cryptology ePrint Archive, Report 2020/1499, November 2020. Available at https://eprint.iacr.org/2020/1499.

[7]

Benjamin Lipp, Bruno Blanchet, and Karthikeyan Bhargavan. A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. In IEEE European Symposium on Security and Privacy (EuroS&P'19), pages 231-246, Stockholm, Sweden, June 2019. IEEE Computer Society.

[8]

Benjamin Lipp, Bruno Blanchet, and Karthikeyan Bhargavan. A mechanised cryptographic proof of the WireGuard virtual private network protocol. Research report RR-9269, Inria, April 2019. Available at https://hal.inria.fr/hal-02100345.

[9]

Bruno Blanchet. Composition Theorems for CryptoVerif and Application to TLS 1.3. In 31st IEEE Computer Security Foundations Symposium (CSF'18), pages 16-30, Oxford, UK, July 2018. IEEE Computer Society.

[10]

Bruno Blanchet. Composition theorems for CryptoVerif and application to TLS 1.3. Research Report RR-9171, Inria, April 2018. Available at https://hal.inria.fr/hal-01764527.

[11]

Bruno Blanchet. Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols. In 30th IEEE Computer Security Foundations Symposium (CSF'17), pages 68-82, Santa Barbara, CA, USA, August 2017. IEEE.

[12]

Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. In IEEE Symposium on Security and Privacy (S&P'17), pages 483-503, San Jose, CA, May 2017. IEEE. Distinguished paper award.

[13]

Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. Verified models and reference implementations for the TLS 1.3 standard candidate. Research Report RR-9040, Inria, May 2017. Available at https://hal.inria.fr/hal-01528752.

[14]

Bruno Blanchet. Symbolic and computational mechanized verification of the ARINC823 avionic protocols. Research Report RR-9072, Inria, May 2017. Available at https://hal.inria.fr/hal-01527671.

[15]

Nadim Kobeissi, Karthikeyan Bhargavan, and Bruno Blanchet. Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach. In 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17), pages 435-450, Paris, France, April 2017. IEEE.

[16]

David Cadé and Bruno Blanchet. Proved Generation of Implementations from Computationally Secure Protocol Specifications. Journal of Computer Security, 23(3):331-402, 2015.

[17]

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.

[18]

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.

[19]

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.

[20]

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.

[21]

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.

[22]

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.

[23]

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

[24]

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.

[25]

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.

[26]

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.

[27]

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.

[28]

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.

[29]

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.

[30]

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.

[31]

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

[32]

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.

[33]

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.

[34]

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.

[35]

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

[36]

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.

[37]

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.

[38]

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