Publications

Copyright / Droits d'auteur.

Journals/Journaux

[1]

Bruno Blanchet and Ben Smyth. Automated reasoning for equivalences in the applied pi calculus with barriers. Journal of Computer Security, 26(3):367-422, 2018.

[2]

Martín Abadi, Bruno Blanchet, and Cédric Fournet. The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. Journal of the ACM, 65(1):1:1-1:41, October 2017.

[3]

Bruno Blanchet. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security, 1(1-2):1-135, October 2016.

[4]

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

[5]

Miriam Paiola and Bruno Blanchet. Verification of Security Protocols with Lists: from Length One to Unbounded Length. Journal of Computer Security, 21(6):781-816, December 2013. Special issue POST'12.

[6]

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.

[7]

Bruno Blanchet. Automatic Verification of Correspondences for Security Protocols. Journal of Computer Security, 17(4):363-434, July 2009.

[8]

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.

[9]

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.

[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 and Andreas Podelski. Verification of Cryptographic Protocols: Tagging Enforces Termination. Theoretical Computer Science, 333(1-2):67-90, March 2005. Special issue FoSSaCS'03.

[14]

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.

[15]

Bruno Blanchet. Escape Analysis for Java(TM). Theory and Practice. ACM Transactions on Programming Languages and Systems, 25(6):713-775, November 2003.

[16]

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

Chapters in books/Chapitres de livres

[1]

Bruno Blanchet. Automatic Verification of Security Protocols in the Symbolic Model: the Verifier ProVerif. In Alessandro Aldini, Javier Lopez, and Fabio Martinelli, editors, Foundations of Security Analysis and Design VII, FOSAD Tutorial Lectures, volume 8604 of Lecture Notes in Computer Science, pages 54-87. Springer, 2014.

[2]

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.

[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, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software, invited chapter. In T. Mogensen, D. A. Schmidt, and I. H. Sudborough, editors, The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, volume 2566 of Lecture Notes in Computer Science, pages 85-108. Springer, December 2002.

Invited Conferences/Conférences invitées

[1]

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), volume 7215 of Lecture Notes in Computer Science, pages 3-29, Tallinn, Estonia, March 2012. Springer.

[2]

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.

[3]

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.

[4]

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 in Computer Science, pages 433-436, Paris, France, July 2001. Springer.

Conferences/Conférences

[1]

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

[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), pages 279-294, Enschede, The Netherlands, July 2024. IEEE.

[3]

Bruno Blanchet and Charlie Jacomme. Post-quantum sound CryptoVerif and verification of hybrid TLS and SSH key-exchanges. In Proceedings of the 37th IEEE Computer Security Foundations Symposium (CSF'24), pages 543-556, Enschede, The Netherlands, July 2024. IEEE.

[4]

Bruno Blanchet, Vincent Cheval, and Véronique Cortier. ProVerif with lemmas, induction, fast subsumption, and much more. In IEEE Symposium on Security and Privacy (S&P'22), pages 205-222, San Francisco, CA, May 2022. IEEE Computer Society.

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

Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. SoK: Computer-Aided Cryptography. In IEEE Symposium on Security and Privacy (S&P'21), pages 777-795. IEEE Computer Society, May 2021.

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

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.

[9]

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.

[10]

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.

[11]

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.

[12]

Bruno Blanchet and Ben Smyth. Automated reasoning for equivalences in the applied pi calculus with barriers. In 29th IEEE Computer Security Foundations Symposium (CSF'16), pages 310-324, Lisboa, Portugal, June 2016. IEEE.

[13]

Bruno Blanchet and Miriam Paiola. Automatic Verification of Protocols with Lists of Unbounded Length. In ACM Conference on Computer and Communications Security (CCS'13), pages 573-584, Berlin, Germany, November 2013. ACM.

[14]

Vincent Cheval and Bruno Blanchet. Proving More Observational Equivalences with ProVerif. 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 226-246, Rome, Italy, March 2013. Springer.

[15]

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.

[16]

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.

[17]

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.

[18]

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), volume 7215 of Lecture Notes in Computer Science, pages 69-88, Tallinn, Estonia, March 2012. Springer.

[19]

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.

[20]

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.

[21]

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.

[22]

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.

[23]

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.

[24]

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

[25]

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.

[26]

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.

[27]

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

[28]

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 in Computer Science, pages 340-354, Barcelona, Spain, March 2004. Springer.

[29]

Bruno Blanchet and Benjamin Aziz. A Calculus for Secure Mobility. In Vijay Saraswat, editor, Eighth Asian Computing Science Conference (ASIAN'03), volume 2896 of Lecture Notes in Computer Science, pages 188-204, Mumbai, India, December 2003. Springer.

[30]

Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. A Static Analyzer for Large Safety-Critical Software. In ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI'03), pages 196-207, San Diego, California, June 2003. ACM.

[31]

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 in Computer Science, pages 316-335, San Diego, California, June 2003. Springer.

[32]

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 in Computer Science, pages 136-152, Warsaw, Poland, April 2003. Springer.

[33]

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 in Computer Science, pages 342-359, Madrid, Spain, September 2002. Springer.

[34]

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.

[35]

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. This paper received a test of time award at the CSF'23 conference.

[36]

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 in Computer Science, pages 25-41, Genova, Italy, April 2001. Springer.

[37]

Bruno Blanchet. Escape Analysis for Object Oriented Languages. Application to Java(TM). In Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'99), pages 20-34, Denver, Colorado, November 1999.

[38]

Bruno Blanchet. Escape Analysis: Correctness Proof, Implementation and Experimental Results. In 25th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'98), pages 25-37, San Diego, California, January 1998. ACM Press.

Workshops

[1]

Bruno Blanchet. The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm. In Geoffrey W. Hamilton, Temesghen Kahsai, and Maurizio Proietti, editors, 9th Workshop on Horn Clauses for Verification and Synthesis (HCVS), volume 373 of EPTCS, pages 14-22. Open Publishing Association, November 2022.

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

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.

[6]

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

[7]

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

[8]

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

[9]

Bruno Blanchet and Benjamin Aziz. A Calculus for Locations, Mobility, and Cryptography. In Dagstuhl seminar Reasoning about Shape, March 2003.

[10]

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

Theses/Mémoires et thèse

[1]

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.

[2]

Bruno Blanchet. Analyse d'échappement. Applications à ML et Java(TM). Escape Analysis. Applications to ML and Java(TM). PhD thesis, École Polytechnique, 7 December 2000. En anglais. In English. Prix de thèse de l'École Polytechnique. Thesis prize of Ecole Polytechnique.

[3]

Bruno Blanchet. Rapport de magistère MMFAI. Master's thesis, ENS, October 1997. En français.

[4]

Bruno Blanchet. Garbage Collection statique. Rapport de DEA, INRIA, Rocquencourt, September 1996. En français.

Reports/Rapports

[1]

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.

[2]

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.

[3]

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.

[4]

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.

[5]

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.

[6]

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.

[7]

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.

[8]

Martín Abadi, Bruno Blanchet, and Cédric Fournet. The applied pi calculus: Mobile values, new names, and secure communication. Report arXiv:1609.03003, September 2016. Revised July 2017. Available at http://arxiv.org/abs/1609.03003.

[9]

Bruno Blanchet and Ben Smyth. Automated reasoning for equivalences in the applied pi calculus with barriers. Research report RR-8906, Inria, April 2016. Available at https://hal.inria.fr/hal-01306440.

[10]

Miriam Paiola and Bruno Blanchet. From the Applied Pi Calculus to Horn Clauses for Protocols with Lists. Research Report RR-8823, Inria, December 2015.
[ http | .pdf ]

[11]

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.

[12]

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

[13]

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.

[14]

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.

[15]

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.

[16]

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.