Bruno Blanchet

72 papers A* 11A 13B 6C 1Journal 26Unranked 13

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