Bruno Blanchet

Publication Activity (10 Years)

Years Active: 1998-2023
Publications (10 Years): 17

Top Topics

Capsule Endoscopy

Automated Verification

Security Protocols

Top Venues

IEEE Symposium on Security and Privacy

J. Comput. Secur.

Publications

Bruno Blanchet
CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels). CoRR (2023)
Bruno Blanchet
The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm. HCVS/VPT@ETAPS (2022)
Bruno Blanchet, Vincent Cheval, Véronique Cortier
ProVerif with Lemmas, Induction, Fast Subsumption, and Much More. IEEE Symposium on Security and Privacy (2022)
Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, Doreen Riepel
Analysing the HPKE Standard. EUROCRYPT (1) (2021)
Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno
SoK: Computer-Aided Cryptography. IEEE Symposium on Security and Privacy (2021)
Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, Doreen Riepel
Analysing the HPKE Standard. IACR Cryptol. ePrint Arch. 2020 (2020)
Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno
SoK: Computer-Aided Cryptography. IACR Cryptol. ePrint Arch. 2019 (2019)
Benjamin Lipp, Bruno Blanchet, Karthikeyan Bhargavan
A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. EuroS&P (2019)
Bruno Blanchet
Composition Theorems for CryptoVerif and Application to TLS 1.3. CSF (2018)
Bruno Blanchet, Ben Smyth
Automated reasoning for equivalences in the applied pi calculus with barriers. J. Comput. Secur. 26 (3) (2018)
Martín Abadi, Bruno Blanchet, Cédric Fournet
The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. J. ACM 65 (1) (2018)
Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi
Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. IEEE Symposium on Security and Privacy (2017)
Bruno Blanchet
Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols. CSF (2017)
Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet
Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. EuroS&P (2017)
Bruno Blanchet, Ben Smyth
Automated Reasoning for Equivalences in the Applied Pi Calculus with Barriers. CSF (2016)
Bruno Blanchet
Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Found. Trends Priv. Secur. 1 (1-2) (2016)
Martín Abadi, Bruno Blanchet, Cédric Fournet
The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. CoRR (2016)
David Cadé, Bruno Blanchet
Proved generation of implementations from computationally secure protocol specifications. J. Comput. Secur. 23 (3) (2015)
Bruno Blanchet, Miriam Paiola
Automatic verification of protocols with lists of unbounded length. CCS (2013)
David Cadé, Bruno Blanchet
Proved Generation of Implementations from Computationally Secure Protocol Specifications. POST (2013)
Bruno Blanchet
Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif. FOSAD (2013)
Vincent Cheval, Bruno Blanchet
Proving More Observational Equivalences with ProVerif. POST (2013)
Miriam Paiola, Bruno Blanchet
Verification of security protocols with lists: From length one to unbounded length. J. Comput. Secur. 21 (6) (2013)
David Cadé, Bruno Blanchet
From Computationally-Proved Protocol Specifications to Implementations and Application to SSH. J. Wirel. Mob. Networks Ubiquitous Comput. Dependable Appl. 4 (1) (2013)
Bruno Blanchet
Automatically Verified Mechanized Proof of One-Encryption Key Exchange. CSF (2012)
Bruno Blanchet
Security Protocol Verification: Symbolic and Computational Models. POST (2012)
David Cadé, Bruno Blanchet
From Computationally-proved Protocol Specifications to Implementations. ARES (2012)
Miriam Paiola, Bruno Blanchet
Verification of Security Protocols with Lists: From Length One to Unbounded Length. POST (2012)
Bruno Blanchet
Automatically Verified Mechanized Proof of One-Encryption Key Exchange. IACR Cryptol. ePrint Arch. 2012 (2012)
Martín Abadi, Bruno Blanchet, Hubert Comon-Lundh
Models and Proofs of Protocol Security: A Progress Report. CAV (2009)
Bruno Blanchet
Automatic verification of correspondences for security protocols. J. Comput. Secur. 17 (4) (2009)
Bruno Blanchet
Automatic Verification of Correspondences for Security Protocols CoRR (2008)
Bruno Blanchet, Avik Chaudhuri
Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage. IEEE Symposium on Security and Privacy (2008)
Bruno Blanchet
A Computationally Sound Mechanized Prover for Security Protocols. IEEE Trans. Dependable Secur. Comput. 5 (4) (2008)
Bruno Blanchet, Martín Abadi, Cédric Fournet
Automated verification of selected equivalences for security protocols. J. Log. Algebraic Methods Program. 75 (1) (2008)
Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, Joe-Kai Tsay
Computationally sound mechanized proofs for basic and public-key Kerberos. AsiaCCS (2008)
Bruno Blanchet
Computationally Sound Mechanized Proofs of Correspondence Assertions. IACR Cryptol. ePrint Arch. 2007 (2007)
Martín Abadi, Bruno Blanchet, Cédric Fournet
Just fast keying in the pi calculus. ACM Trans. Inf. Syst. Secur. 10 (3) (2007)
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
A Static Analyzer for Large Safety-Critical Software CoRR (2007)
Bruno Blanchet
Computationally Sound Mechanized Proofs of Correspondence Assertions. CSF (2007)
Bruno Blanchet
A Computationally Sound Mechanized Prover for Security Protocols. IEEE Symposium on Security and Privacy (2006)
Bruno Blanchet, David Pointcheval
Automated Security Proofs with Sequences of Games. CRYPTO (2006)
Bruno Blanchet, David Pointcheval
Automated Security Proofs with Sequences of Games. IACR Cryptol. ePrint Arch. 2006 (2006)
Xavier Allamigeon, Bruno Blanchet
Reconstruction of Attacks against Cryptographic Protocols. CSFW (2005)
Martín Abadi, Bruno Blanchet
Computer-assisted verification of a protocol for certified email. Sci. Comput. Program. 58 (1-2) (2005)
Bruno Blanchet, Andreas Podelski
Verification of cryptographic protocols: tagging enforces termination. Theor. Comput. Sci. 333 (1-2) (2005)
Bruno Blanchet
A Computationally Sound Mechanized Prover for Security Protocols. IACR Cryptol. ePrint Arch. 2005 (2005)
Bruno Blanchet
Security protocols: from linear to classical logic by abstract interpretation. Inf. Process. Lett. 95 (5) (2005)
Bruno Blanchet, Martín Abadi, Cédric Fournet
Automated Verification of Selected Equivalences for Security Protocols. LICS (2005)
Martín Abadi, Bruno Blanchet
Analyzing security protocols with secrecy types and logic programs. J. ACM 52 (1) (2005)
Bruno Blanchet
Automatic Proof of Strong Secrecy for Security Protocols. IEEE Symposium on Security and Privacy (2004)
Martín Abadi, Bruno Blanchet, Cédric Fournet
Just Fast Keying in the Pi Calculus. ESOP (2004)
Bruno Blanchet, Andreas Podelski
Verification of Cryptographic Protocols: Tagging Enforces Termination. FoSSaCS (2003)
Martín Abadi, Bruno Blanchet
Secrecy types for asymmetric communication. Theor. Comput. Sci. 298 (3) (2003)
Bruno Blanchet
Automatic verification of cryptographic protocols: a logic programming approach. PPDP (2003)
Martín Abadi, Bruno Blanchet
Computer-Assisted Verification of a Protocol for Certified Email. SAS (2003)
Bruno Blanchet
: Theory and practice. ACM Trans. Program. Lang. Syst. 25 (6) (2003)
Bruno Blanchet, Benjamin Aziz
A Calculus for Secure Mobility. ASIAN (2003)
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
A static analyzer for large safety-critical software. PLDI (2003)
Bruno Blanchet
From Secrecy to Authenticity in Security Protocols. SAS (2002)
Martín Abadi, Bruno Blanchet
Analyzing security protocols with secrecy types and logic programs. POPL (2002)
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software. The Essence of Computation (2002)
Bruno Blanchet
An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. CSFW (2001)
Martín Abadi, Bruno Blanchet
Secrecy Types for Asymmetric Communication. FoSSaCS (2001)
Bruno Blanchet
Abstracting Cryptographic Protocols by Prolog Rules. SAS (2001)
Bruno Blanchet
Escape Analysis for Object-Oriented Languages: Application to Java. OOPSLA (1999)
Bruno Blanchet
Escape Analysis: Correctness Proof, Implementation and Experimental Results. POPL (1998)