Bruno Blanchet

CoRR, 2023

2022

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

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Vincent Cheval

Véronique Cortier

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

2020

Analysing the HPKE Standard.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2020

2019

SoK: Computer-Aided Cryptography.

[BibT_eX]

[DOI]

Manuel Barbosa

Gilles Barthe

IACR Cryptol. ePrint Arch., 2019

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

[BibT_eX]

[DOI]

Benjamin Lipp

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

2018

Automated reasoning for equivalences in the applied pi calculus with barriers.

[BibT_eX]

[DOI]

Ben Smyth

J. Comput. Secur., 2018

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

[BibT_eX]

[DOI]

Cédric Fournet

J. ACM, 2018

Composition Theorems for CryptoVerif and Application to TLS 1.3.

[BibT_eX]

[DOI]

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

2017

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

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Nadim Kobeissi

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

Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols.

[BibT_eX]

[DOI]

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

2016

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

[BibT_eX]

[DOI]

Found. Trends Priv. Secur., 2016

2015

Proved generation of implementations from computationally secure protocol specifications.

[BibT_eX]

[DOI]

David Cadé

J. Comput. Secur., 2015

2013

From Computationally-Proved Protocol Specifications to Implementations and Application to SSH.

[BibT_eX]

[DOI]

David Cadé

J. Wirel. Mob. Networks Ubiquitous Comput. Dependable Appl., 2013

Verification of security protocols with lists: From length one to unbounded length.

[BibT_eX]

[DOI]

Miriam Paiola

J. Comput. Secur., 2013

Proving More Observational Equivalences with ProVerif.

[BibT_eX]

[DOI]

Vincent Cheval

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

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

[BibT_eX]

[DOI]

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

Automatic verification of protocols with lists of unbounded length.

[BibT_eX]

[DOI]

Miriam Paiola

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

2012

Mechanizing Game-Based Proofs of Security Protocols.

[BibT_eX]

[DOI]

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

Automatically Verified Mechanized Proof of One-Encryption Key Exchange.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2012

Security Protocol Verification: Symbolic and Computational Models.

[BibT_eX]

[DOI]

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

From Computationally-proved Protocol Specifications to Implementations.

[BibT_eX]

[DOI]

David Cadé

Proceedings of the Seventh International Conference on Availability, 2012

2011

Using Horn Clauses for Analyzing Security Protocols.

[BibT_eX]

[DOI]

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

2009

Automatic verification of correspondences for security protocols.

[BibT_eX]

[DOI]

J. Comput. Secur., 2009

Models and Proofs of Protocol Security: A Progress Report.

[BibT_eX]

[DOI]

Hubert Comon-Lundh

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

2008

Automated verification of selected equivalences for security protocols.

[BibT_eX]

[DOI]

Cédric Fournet

J. Log. Algebraic Methods Program., 2008

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

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

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

2007

Just fast keying in the pi calculus.

[BibT_eX]

[DOI]

Cédric Fournet

ACM Trans. Inf. Syst. Secur., 2007

Computationally Sound Mechanized Proofs of Correspondence Assertions.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2007

2006

Automated Security Proofs with Sequences of Games.

[BibT_eX]

[DOI]

David Pointcheval

IACR Cryptol. ePrint Arch., 2006

2005

Verification of cryptographic protocols: tagging enforces termination.

[BibT_eX]

[DOI]

Andreas Podelski

Theor. Comput. Sci., 2005

Computer-assisted verification of a protocol for certified email.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2005

Analyzing security protocols with secrecy types and logic programs.

[BibT_eX]

[DOI]

J. ACM, 2005

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

[BibT_eX]

[DOI]

Inf. Process. Lett., 2005

A Computationally Sound Mechanized Prover for Security Protocols.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2005

Reconstruction of Attacks against Cryptographic Protocols.

[BibT_eX]

[DOI]

Xavier Allamigeon

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

2004

Automatic Proof of Strong Secrecy for Security Protocols.

[BibT_eX]

[DOI]

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

2003

Escape analysis for Java<sup>TM</sup>: Theory and practice.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2003

Secrecy types for asymmetric communication.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2003

Automatic verification of cryptographic protocols: a logic programming approach.

[BibT_eX]

[DOI]

Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2003

A static analyzer for large safety-critical software.

[BibT_eX]

[DOI]

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

A Calculus for Secure Mobility.

[BibT_eX]

[DOI]

Benjamin Aziz

Proceedings of the Advances in Computing Science, 2003

2002

From Secrecy to Authenticity in Security Protocols.

[BibT_eX]

[DOI]

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

Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software.

[BibT_eX]

[DOI]

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

2001

Abstracting Cryptographic Protocols by Prolog Rules.

[BibT_eX]

[DOI]

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

An Efficient Cryptographic Protocol Verifier Based on Prolog Rules.

[BibT_eX]

[DOI]

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

1999

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

[BibT_eX]

[DOI]

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

1998

Escape Analysis: Correctness Proof, Implementation and Experimental Results.

[BibT_eX]

[DOI]