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.

[BibT_eX]

[DOI]

Dataset, September, 2021

2020

Analysing the HPKE Standard - Supplementary Material.

[BibT_eX]

[DOI]

Dataset, November, 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

A Computationally Sound Mechanized Prover for Security Protocols.

[BibT_eX]

[DOI]

IEEE Trans. Dependable Secur. Comput., 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

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]