Analysis of cryptographic protocols in the computational model

• CryptoVerif produces proofs by sequences of games, as used by cryptographers.
• It produces proofs valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary.
• It provides a generic mechanism for specifying the security assumptions on cryptographic primitives, which can handle in particular symmetric encryption, message authentication codes, public-key encryption, signatures, hash functions, the computational Diffie-Hellman assumption.
• can prove:
  • secrecy (Oakland'06, TDSC).
  • correspondences (CSF'07), which include in particular authentication.
• It 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).

Publications on this topic

[1]

Bruno Blanchet. Mechanizing Game-Based Proofs of Security Protocols. In Olga Grumberg, Tobias Nipkow, and Javier Esparza, editors, Tools for Analysis and Verification of Software Safety and Security. IOS Press, 2012. Proceedings of the 2011 MOD summer school. To appear.

[2]

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

[3]

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.

[4]

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.

[5]

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 on Computer Science, pages 35-49, Grenoble, France, June 2009. Springer Verlag.

[6]

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.

[7]

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.

[8]

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.

[9]

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

[10]

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.

[11]

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.

[12]

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.

[13]

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

[14]

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

[15]

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.

[16]

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.

[17]

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

Software: CryptoVerif