Vérification de protocoles cryptographiques dans le modèle formel

• Il est fondé sur le modèle formel des protocoles : on suppose des primitives cryptographiques parfaites (par exemple, on ne peut déchiffrer un message que si on a la clé correspondante). Les messages sont des termes sur ces primitives cryptographiques, et l'attaquant est restreint à n'appliquer que ces primitives. Moyennant cette hypothèse, on peut prouver des propriétés du protocole.
• Il peut traiter beaucoup de primitives cryptographiques, définies par des règles de réécriture ou des équations, dont la cryptographie à clé partagée et publique (chiffrement et signatures), les fonctions de hachage, mise en accord de clés de Diffie-Hellman, etc.
• Il peut traiter un nombre non-borné de sessions (même en parallèle) et un espace de messages non-borné. Ce résultat a été obtenu grâce à des approximations bien choisies, c'est-à-dire que ce vérificateur peut donner de fausses attaques, mais que s'il affirme qu'une propriété de sécurité est vraie, alors elle est vraie.
• Il peut prouver les propriétés suivantes:
  • secret (l'attaquant ne peut pas obtenir une certaine donnée, CSFW'01)
  • authenticité (SAS'02), et plus généralement propriétés de correspondances entre événements (SAS'03, en collaboration avec Martín Abadi; JCS)
  • secret fort (l'attaquant ne voit pas la différence si la valeur du secret change, Oakland'04)
  • équivalences de processus qui ne diffèrent que par des termes (LICS'05 et JLAP, avec Martín Abadi et Cédric Fournet)
• J'ai testé ce vérificateur sur des protocoles de la littérature avec des résultats très encourageants: beaucoup d'exemples de protocoles peuvent être vérifiés par cet outil avec très peu de ressources. (Les protocoles de la littérature sont typiquement vérifiés en moins de 1 s.)
• Avec Andreas Podelski, j'ai montré que l'algorithme de résolution utilisé termine sur une large classe de protocoles (protocoles dits "taggés", FoSSaCS'03 et TCS).
• Xavier Allamigeon a conçu un algorithme de reconstruction d'attaques lors d'un stage sous ma direction (CSFW'05).
• J'ai aussi effectué des études de cas plus ambitieuses, avec Martín Abadi et Cédric Fournet sur le protocole JFK (ESOP'04), avec Avik Chaudhuri sur le système de fichiers PLutus (Oakland'08).

En collaboration avec Martín Abadi, j'ai aussi étudié des méthodes de vérification fondée sur le typage (FoSSaCS'01 et TCS'03). Ces deux approches ont été comparées dans notre article à POPL'2002 avec Martín Abadi. Nous montrons que notre système de types de FoSSaCS peut être étendu pour traiter davantage de primitives cryptographiques de façon plus flexible, et que ce nouveau système de types est équivalent au vérificateur de protocoles pour le secret. Les deux techniques prouvent exactement les mêmes propriétés de secret, même si elles semblent complètement différentes a priori.

Publications sur ce sujet

[1]

Miriam Paiola and Bruno Blanchet. Verification of security protocols with lists: from length one to unbounded length. In Pierpaolo Degano and Joshua Guttman, editors, First Conference on Principles of Security and Trust (POST'12), Lecture Notes on Computer Science, Tallinn, Estonia, March 2012. Springer Verlag. To appear. Available at http://www.di.ens.fr/~paiola/publications/PaiolaBlanchetPOST12.html.

[2]

Bruno Blanchet. Security Protocol Verification: Symbolic and Computational Models. In Pierpaolo Degano and Joshua Guttman, editors, First Conference on Principles of Security and Trust (POST'12), Lecture Notes on Computer Science, Tallinn, Estonia, March 2012. Springer Verlag. To appear.

[3]

Bruno Blanchet. Using Horn Clauses for Analyzing Security Protocols. In Véronique Cortier and Steve Kremer, editors, Formal Models and Techniques for Analyzing Security Protocols, volume 5 of Cryptology and Information Security Series, pages 86-111. IOS Press, March 2011.

[4]

Bruno Blanchet. Automatic Verification of Correspondences for Security Protocols. Journal of Computer Security, 17(4):363-434, 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 and Avik Chaudhuri. Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage. In IEEE Symposium on Security and Privacy, pages 417-431, Oakland, CA, May 2008. IEEE.

[8]

Bruno Blanchet. Automatic verification of correspondences for security protocols. Report arXiv:0802.3444v1, February 2008. Available at http://arxiv.org/abs/0802.3444v1.

[9]

Bruno Blanchet, Martín Abadi, and Cédric Fournet. Automated Verification of Selected Equivalences for Security Protocols. Journal of Logic and Algebraic Programming, 75(1):3-51, February-March 2008.

[10]

Martín Abadi, Bruno Blanchet, and Cédric Fournet. Just Fast Keying in the Pi Calculus. ACM Transactions on Information and System Security (TISSEC), 10(3):1-59, July 2007.

[11]

Martín Abadi and Bruno Blanchet. Computer-Assisted Verification of a Protocol for Certified Email. Science of Computer Programming, 58(1-2):3-27, October 2005. Special issue SAS'03.

[12]

Bruno Blanchet. Security Protocols: From Linear to Classical Logic by Abstract Interpretation. Information Processing Letters, 95(5):473-479, September 2005.

[13]

Bruno Blanchet. An Automatic Security Protocol Verifier based on Resolution Theorem Proving (invited tutorial). In 20th International Conference on Automated Deduction (CADE-20), Tallinn, Estonia, July 2005.

[14]

Bruno Blanchet, Martín Abadi, and Cédric Fournet. Automated Verification of Selected Equivalences for Security Protocols. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), pages 331-340, Chicago, IL, June 2005. IEEE Computer Society.

[15]

Xavier Allamigeon and Bruno Blanchet. Reconstruction of Attacks against Cryptographic Protocols. In 18th IEEE Computer Security Foundations Workshop (CSFW-18), pages 140-154, Aix-en-Provence, France, June 2005. IEEE Computer Society.

[16]

Bruno Blanchet and Andreas Podelski. Verification of Cryptographic Protocols: Tagging Enforces Termination. Theoretical Computer Science, 333(1-2):67-90, March 2005. Special issue FoSSaCS'03.

[17]

Martín Abadi and Bruno Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. Journal of the ACM, 52(1):102-146, January 2005.

[18]

Bruno Blanchet. Automatic Proof of Strong Secrecy for Security Protocols. Technical Report MPI-I-2004-NWG1-001, Max-Planck-Institut für Informatik, Saarbrücken, Germany, July 2004.

[19]

Bruno Blanchet. Automatic Proof of Strong Secrecy for Security Protocols. In IEEE Symposium on Security and Privacy, pages 86-100, Oakland, California, May 2004.

[20]

Martín Abadi, Bruno Blanchet, and Cédric Fournet. Just Fast Keying in the Pi Calculus. In David Schmidt, editor, Programming Languages and Systems: Proceedings of the 13th European Symposium on Programming (ESOP'04), volume 2986 of Lecture Notes on Computer Science, pages 340-354, Barcelona, Spain, March 2004. Springer Verlag.

[21]

Bruno Blanchet. Automatic Proof of Strong Secrecy for Security Protocols. In Dagstuhl seminar Language-Based Security, October 2003.

[22]

Bruno Blanchet. Automatic Verification of Cryptographic Protocols: A Logic Programming Approach (invited talk). In 5th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'03), pages 1-3, Uppsala, Sweden, August 2003. ACM.

[23]

Martín Abadi and Bruno Blanchet. Computer-Assisted Verification of a Protocol for Certified Email. In Radhia Cousot, editor, Static Analysis, 10th International Symposium (SAS'03), volume 2694 of Lecture Notes on Computer Science, pages 316-335, San Diego, California, June 2003. Springer Verlag.

[24]

Martín Abadi and Bruno Blanchet. Secrecy Types for Asymmetric Communication. Theoretical Computer Science, 298(3):387-415, April 2003. Special issue FoSSaCS'01.

[25]

Bruno Blanchet and Andreas Podelski. Verification of Cryptographic Protocols: Tagging Enforces Termination. In Andrew Gordon, editor, Foundations of Software Science and Computation Structures (FoSSaCS'03), volume 2620 of Lecture Notes on Computer Science, pages 136-152, Warsaw, Poland, April 2003. Springer Verlag.

[26]

Bruno Blanchet. From Secrecy to Authenticity in Security Protocols. In Manuel Hermenegildo and Germán Puebla, editors, 9th International Static Analysis Symposium (SAS'02), volume 2477 of Lecture Notes on Computer Science, pages 342-359, Madrid, Spain, September 2002. Springer Verlag.

[27]

Martín Abadi and Bruno Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. In 29th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL 2002), pages 33-44, Portland, Oregon, January 2002. ACM Press.

[28]

Bruno Blanchet. Abstracting Cryptographic Protocols by Prolog Rules (invited talk). In Patrick Cousot, editor, 8th International Static Analysis Symposium (SAS'2001), volume 2126 of Lecture Notes on Computer Science, pages 433-436, Paris, France, July 2001. Springer Verlag.

[29]

Bruno Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82-96, Cape Breton, Nova Scotia, Canada, June 2001. IEEE Computer Society.

[30]

Martín Abadi and Bruno Blanchet. Secrecy Types for Asymmetric Communication. In F. Honsell and M. Miculan, editors, Foundations of Software Science and Computation Structures (FoSSaCS 2001), volume 2030 of Lecture Notes on Computer Science, pages 25-41, Genova, Italy, April 2001. Springer Verlag.

[31]

Martín Abadi and Bruno Blanchet. Secrecy Types for Asymmetric Communication. In Dagstuhl seminar Security through Analysis and Verification, December 2000.

Logiciel: ProVerif