Escape Analysis: Correctness Proof, Implementation and Experimental Results. - Bruno Blanchet (POPL, 1998)

Escape Analysis for Object-Oriented Languages: Application to Java. - Bruno Blanchet (OOPSLA, 1999)

An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. - Bruno Blanchet (CSFW, 2001)

Abstracting Cryptographic Protocols by Prolog Rules. - Bruno Blanchet (SAS, 2001)

Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software. - Bruno Blanchet; Patrick Cousot; Radhia Cousot; Jérôme Feret; Laurent Mauborgne; Antoine Miné; David Monniaux; Xavier Rival (The Essence of Computation, 2002)

From Secrecy to Authenticity in Security Protocols. - Bruno Blanchet (SAS, 2002)

A Calculus for Secure Mobility. - Bruno Blanchet; Benjamin Aziz (ASIAN, 2003)

A static analyzer for large safety-critical software. - Bruno Blanchet; Patrick Cousot; Radhia Cousot; Jérôme Feret; Laurent Mauborgne; Antoine Miné; David Monniaux; Xavier Rival (PLDI, 2003)

Automatic verification of cryptographic protocols: a logic programming approach. - Bruno Blanchet (PPDP, 2003)

Secrecy types for asymmetric communication. - Martín Abadi; Bruno Blanchet (Theor. Comput. Sci., 2003)

Escape analysis for JavaTM: Theory and practice. - Bruno Blanchet (ACM Trans. Program. Lang. Syst., 2003)

Automatic Proof of Strong Secrecy for Security Protocols. - Bruno Blanchet (S&P, 2004)

Reconstruction of Attacks against Cryptographic Protocols. - Xavier Allamigeon; Bruno Blanchet (CSFW, 2005)

Security protocols: from linear to classical logic by abstract interpretation. - Bruno Blanchet (Inf. Process. Lett., 2005)

Analyzing security protocols with secrecy types and logic programs. - Martín Abadi; Bruno Blanchet (J. ACM, 2005)

Computer-assisted verification of a protocol for certified email. - Martín Abadi; Bruno Blanchet (Sci. Comput. Program., 2005)

Verification of cryptographic protocols: tagging enforces termination. - Bruno Blanchet; Andreas Podelski (Theor. Comput. Sci., 2005)

Automated Security Proofs with Sequences of Games. - Bruno Blanchet; David Pointcheval (IACR Cryptol. ePrint Arch., 2006)

Computationally Sound Mechanized Proofs of Correspondence Assertions. - Bruno Blanchet (IACR Cryptol. ePrint Arch., 2007)

Just fast keying in the pi calculus. - Martín Abadi; Bruno Blanchet; Cédric Fournet (ACM Trans. Inf. Syst. Secur., 2007)

Computationally sound mechanized proofs for basic and public-key Kerberos. - Bruno Blanchet; Aaron D. Jaggard; Andre Scedrov; Joe-Kai Tsay (AsiaCCS, 2008)

Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage. - Bruno Blanchet; Avik Chaudhuri (SP, 2008)

Automated verification of selected equivalences for security protocols. - Bruno Blanchet; Martín Abadi; Cédric Fournet (J. Log. Algebraic Methods Program., 2008)

A Computationally Sound Mechanized Prover for Security Protocols. - Bruno Blanchet (IEEE Trans. Dependable Secur. Comput., 2008)

Models and Proofs of Protocol Security: A Progress Report. - Martín Abadi; Bruno Blanchet; Hubert Comon-Lundh (CAV, 2009)

Automatic verification of correspondences for security protocols. - Bruno Blanchet (J. Comput. Secur., 2009)

Using Horn Clauses for Analyzing Security Protocols. - Bruno Blanchet (Formal Models and Techniques for Analyzing Security Protocols, 2011)

From Computationally-proved Protocol Specifications to Implementations. - David Cadé; Bruno Blanchet (ARES, 2012)

Security Protocol Verification: Symbolic and Computational Models. - Bruno Blanchet (POST, 2012)

Automatically Verified Mechanized Proof of One-Encryption Key Exchange. - Bruno Blanchet (IACR Cryptol. ePrint Arch., 2012)

Mechanizing Game-Based Proofs of Security Protocols. - Bruno Blanchet (Software Safety and Security, 2012)

Automatic verification of protocols with lists of unbounded length. - Bruno Blanchet; Miriam Paiola (CCS, 2013)

Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif. - Bruno Blanchet (FOSAD, 2013)

Proving More Observational Equivalences with ProVerif. - Vincent Cheval; Bruno Blanchet (POST, 2013)

Verification of security protocols with lists: From length one to unbounded length. - Miriam Paiola; Bruno Blanchet (J. Comput. Secur., 2013)

From Computationally-Proved Protocol Specifications to Implementations and Application to SSH. - David Cadé; Bruno Blanchet (J. Wirel. Mob. Networks Ubiquitous Comput. Dependable Appl., 2013)

Proved generation of implementations from computationally secure protocol specifications. - David Cadé; Bruno Blanchet (J. Comput. Secur., 2015)

Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. - Bruno Blanchet (Found. Trends Priv. Secur., 2016)

Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols. - Bruno Blanchet (CSF, 2017)

Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. - Nadim Kobeissi; Karthikeyan Bhargavan; Bruno Blanchet (EuroS&P, 2017)

Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. - Karthikeyan Bhargavan; Bruno Blanchet; Nadim Kobeissi (IEEE Symposium on Security and Privacy, 2017)

Composition Theorems for CryptoVerif and Application to TLS 1.3. - Bruno Blanchet (CSF, 2018)

The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. - Martín Abadi; Bruno Blanchet; Cédric Fournet (J. ACM, 2018)

Automated reasoning for equivalences in the applied pi calculus with barriers. - Bruno Blanchet; Ben Smyth (J. Comput. Secur., 2018)

A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. - Benjamin Lipp 001; Bruno Blanchet; Karthikeyan Bhargavan (EuroS&P, 2019)

SoK: Computer-Aided Cryptography. - Manuel Barbosa; Gilles Barthe; Karthikeyan Bhargavan; Bruno Blanchet; Cas Cremers; Kevin Liao; Bryan Parno (IACR Cryptol. ePrint Arch., 2019)

Analysing the HPKE Standard. - Joël Alwen; Bruno Blanchet; Eduard Hauck; Eike Kiltz; Benjamin Lipp 001; Doreen Riepel (IACR Cryptol. ePrint Arch., 2020)

Analysing the HPKE Standard - Supplementary Material. - Joël Alwen; Bruno Blanchet; Eduard Hauck; Eike Kiltz; Benjamin Lipp 001; Doreen Riepel (Zenodo, 2020)

Analysing the HPKE Standard - Supplementary Material. - Joël Alwen; Bruno Blanchet; Eduard Hauck; Eike Kiltz; Benjamin Lipp 001; Doreen Riepel (Zenodo, 2021)

ProVerif with Lemmas, Induction, Fast Subsumption, and Much More. - Bruno Blanchet; Vincent Cheval; Véronique Cortier (SP, 2022)

The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm. - Bruno Blanchet (HCVS/VPT@ETAPS, 2022)

Analysing the HPKE Standard - Supplementary Material. - Joël Alwen; Bruno Blanchet; Eduard Hauck; Eike Kiltz; Benjamin Lipp 001; Doreen Riepel (Zenodo, 2022)

CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels). - Bruno Blanchet (CoRR, 2023)

Dealing with Dynamic Key Compromise in Crypto Verif. - Bruno Blanchet (CSF, 2024)

CV2EC: Getting the Best of Both Worlds. - Bruno Blanchet; Pierre Boutry; Christian Doczkal; Benjamin Grégoire; Pierre-Yves Strub (CSF, 2024)

Post-Quantum Sound CryptoVerif and Verification of Hybrid TLS and SSH Key-Exchanges. - Bruno Blanchet; Charlie Jacomme (CSF, 2024)