Analyse de protocoles cryptographiques dans le modèle calculatoire

• CryptoVerif produit des preuves par jeux, comme celles des cryptographes.
• Il produit des preuves valides pour un nombre de sessions polynomial dans le paramètre de sécurité, en présence d'un attaquant actif.
• Il fournit un mécanisme générique pour spécifier des primitives cryptographiques variées, qui traite en particulier chiffrement à clé partagée, codes d'authentification de messages, chiffrement à clé publique, signatures, fonctions de hachage, hypothèse de Diffie-Hellman calculatoire.
• Il peut prouver :
  • Le secret (Oakland'06, TDSC).
  • Les correspondances, qui incluent en particulier l'authentification (CSF'07).
• Il peut aussi borner la probabilité d'une attaque en fonction du nombre de sessions de la probabilité de casser chaque primitive (sécurité exacte).

Publications sur ce sujet

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

Logiciel: CryptoVerif