Bruno Blanchet

According to our database, Bruno Blanchet authored at least 56 papers between 1998 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2024

Post-Quantum Sound CryptoVerif and Verification of Hybrid TLS and SSH Key-Exchanges.

Bruno Blanchet, Charlie Jacomme

Proceedings of the 37th IEEE Computer Security Foundations Symposium, 2024

CV2EC: Getting the Best of Both Worlds.

Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub

Proceedings of the 37th IEEE Computer Security Foundations Symposium, 2024

Dealing with Dynamic Key Compromise in Crypto Verif.

Bruno Blanchet

Proceedings of the 37th IEEE Computer Security Foundations Symposium, 2024

2023

CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels).

Bruno Blanchet

CoRR, 2023

2022

Analysing the HPKE Standard - Supplementary Material.

Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, Doreen Riepel

Dataset, August, 2022

The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm.

Bruno Blanchet

Proceedings of the Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation, 2022

ProVerif with Lemmas, Induction, Fast Subsumption, and Much More.

Bruno Blanchet, Vincent Cheval, Véronique Cortier

Proceedings of the 43rd IEEE Symposium on Security and Privacy, 2022

2021

Analysing the HPKE Standard - Supplementary Material.

Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, Doreen Riepel

Dataset, September, 2021

SoK: Computer-Aided Cryptography.

Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno

Proceedings of the 42nd IEEE Symposium on Security and Privacy, 2021

Analysing the HPKE Standard.

Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, Doreen Riepel

Proceedings of the Advances in Cryptology - EUROCRYPT 2021, 2021

2020

Analysing the HPKE Standard - Supplementary Material.

Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, Doreen Riepel

Dataset, November, 2020

2019

A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol.

Benjamin Lipp, Bruno Blanchet, Karthikeyan Bhargavan

Proceedings of the IEEE European Symposium on Security and Privacy, 2019

2018

The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication.

Martín Abadi, Bruno Blanchet, Cédric Fournet

J. ACM, 2018

Composition Theorems for CryptoVerif and Application to TLS 1.3.

Bruno Blanchet

Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

2017

Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate.

Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi

Proceedings of the 2017 IEEE Symposium on Security and Privacy, 2017

Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach.

Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet

Proceedings of the 2017 IEEE European Symposium on Security and Privacy, 2017

Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols.

Bruno Blanchet

Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

2016

Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif.

Bruno Blanchet

Found. Trends Priv. Secur., 2016

Automated Reasoning for Equivalences in the Applied Pi Calculus with Barriers.

Bruno Blanchet, Ben Smyth

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

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

Proving More Observational Equivalences with ProVerif.

Vincent Cheval, Bruno Blanchet

Proceedings of the Principles of Security and Trust - Second International Conference, 2013

Proved Generation of Implementations from Computationally Secure Protocol Specifications.

David Cadé, Bruno Blanchet

Proceedings of the Principles of Security and Trust - Second International Conference, 2013

Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif.

Bruno Blanchet

Proceedings of the Foundations of Security Analysis and Design VII, 2013

Automatic verification of protocols with lists of unbounded length.

Bruno Blanchet, Miriam Paiola

Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

2012

Mechanizing Game-Based Proofs of Security Protocols.

Bruno Blanchet

Proceedings of the Software Safety and Security - Tools for Analysis and Verification, 2012

Verification of Security Protocols with Lists: From Length One to Unbounded Length.

Miriam Paiola, Bruno Blanchet

Proceedings of the Principles of Security and Trust - First International Conference, 2012

Security Protocol Verification: Symbolic and Computational Models.

Bruno Blanchet

Proceedings of the Principles of Security and Trust - First International Conference, 2012

Automatically Verified Mechanized Proof of One-Encryption Key Exchange.

Bruno Blanchet

Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

From Computationally-proved Protocol Specifications to Implementations.

David Cadé, Bruno Blanchet

Proceedings of the Seventh International Conference on Availability, 2012

2011

Using Horn Clauses for Analyzing Security Protocols.

Bruno Blanchet

Proceedings of the Formal Models and Techniques for Analyzing Security Protocols, 2011

2009

Automatic verification of correspondences for security protocols.

Bruno Blanchet

J. Comput. Secur., 2009

Models and Proofs of Protocol Security: A Progress Report.

Martín Abadi, Bruno Blanchet, Hubert Comon-Lundh

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008

Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage.

Bruno Blanchet, Avik Chaudhuri

Proceedings of the 2008 IEEE Symposium on Security and Privacy (SP 2008), 2008

Computationally sound mechanized proofs for basic and public-key Kerberos.

Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, Joe-Kai Tsay

Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security, 2008

2007

Computationally Sound Mechanized Proofs of Correspondence Assertions.

Bruno Blanchet

Proceedings of the 20th IEEE Computer Security Foundations Symposium, 2007

2006

A Computationally Sound Mechanized Prover for Security Protocols.

Bruno Blanchet

Proceedings of the 2006 IEEE Symposium on Security and Privacy (S&P 2006), 2006

Automated Security Proofs with Sequences of Games.

Bruno Blanchet, David Pointcheval

Proceedings of the Advances in Cryptology, 2006

2005

Security protocols: from linear to classical logic by abstract interpretation.

Bruno Blanchet

Inf. Process. Lett., 2005

Automated Verification of Selected Equivalences for Security Protocols.

Bruno Blanchet, Martín Abadi, Cédric Fournet

Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

Reconstruction of Attacks against Cryptographic Protocols.

Xavier Allamigeon, Bruno Blanchet

Proceedings of the 18th IEEE Computer Security Foundations Workshop, 2005

2004

Automatic Proof of Strong Secrecy for Security Protocols.

Bruno Blanchet

Proceedings of the 2004 IEEE Symposium on Security and Privacy (S&P 2004), 2004

Just Fast Keying in the Pi Calculus.

Martín Abadi, Bruno Blanchet, Cédric Fournet

Proceedings of the Programming Languages and Systems, 2004

2003

Escape analysis for Java^TM: Theory and practice.

Bruno Blanchet

ACM Trans. Program. Lang. Syst., 2003

Computer-Assisted Verification of a Protocol for Certified Email.

Martín Abadi, Bruno Blanchet

Proceedings of the Static Analysis, 10th International Symposium, 2003

Automatic verification of cryptographic protocols: a logic programming approach.

Bruno Blanchet

Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 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

Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, 2003

Verification of Cryptographic Protocols: Tagging Enforces Termination.

Bruno Blanchet, Andreas Podelski

Proceedings of the Foundations of Software Science and Computational Structures, 2003

A Calculus for Secure Mobility.

Bruno Blanchet, Benjamin Aziz

Proceedings of the Advances in Computing Science, 2003

2002

From Secrecy to Authenticity in Security Protocols.

Bruno Blanchet

Proceedings of the Static Analysis, 9th International Symposium, 2002

Analyzing security protocols with secrecy types and logic programs.

Martín Abadi, Bruno Blanchet

Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

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

Proceedings of the Essence of Computation, Complexity, Analysis, 2002

2001

Abstracting Cryptographic Protocols by Prolog Rules.

Bruno Blanchet

Proceedings of the Static Analysis, 8th International Symposium, 2001

Secrecy Types for Asymmetric Communication.

Martín Abadi, Bruno Blanchet

Proceedings of the Foundations of Software Science and Computation Structures, 2001

An Efficient Cryptographic Protocol Verifier Based on Prolog Rules.

Bruno Blanchet

Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 2001

1999

Escape Analysis for Object-Oriented Languages: Application to Java.

Bruno Blanchet

Proceedings of the 1999 ACM SIGPLAN Conference on Object-Oriented Programming Systems, 1999

1998

Escape Analysis: Correctness Proof, Implementation and Experimental Results.

Bruno Blanchet

Proceedings of the POPL '98, 1998