default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBruno Blanchet
Person information
- affiliation: ENS Paris, France
SPARQL queries 
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[c44]Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub:
CV2EC: Getting the Best of Both Worlds. CSF 2024: 279-294- [c43]Bruno Blanchet:
Dealing with Dynamic Key Compromise in Crypto Verif. CSF 2024: 495-510 - [c42]Bruno Blanchet, Charlie Jacomme:
Post-Quantum Sound CryptoVerif and Verification of Hybrid TLS and SSH Key-Exchanges. CSF 2024: 543-556 - 2023
- [i10]Bruno Blanchet:
CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels). CoRR abs/2310.14658 (2023) - 2022
- [c41]Bruno Blanchet, Vincent Cheval, Véronique Cortier:
ProVerif with Lemmas, Induction, Fast Subsumption, and Much More. SP 2022: 69-86 - [c40]Bruno Blanchet
:
The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm. HCVS/VPT@ETAPS 2022: 14-22 - [d3]Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, Doreen Riepel:
Analysing the HPKE Standard - Supplementary Material. Version v3.0. Zenodo, 2022 [all versions]
- 2021
- [c39]Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, Doreen Riepel:
Analysing the HPKE Standard. EUROCRYPT (1) 2021: 87-116 - [c38]Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno:
SoK: Computer-Aided Cryptography. SP 2021: 777-795 - [d2]Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, Doreen Riepel:
Analysing the HPKE Standard - Supplementary Material. Version v2.0. Zenodo, 2021 [all versions] - 2020
- [d1]Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, Doreen Riepel:
Analysing the HPKE Standard - Supplementary Material. Version v1.0. Zenodo, 2020 [all versions] - [i9]Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, Doreen Riepel:
Analysing the HPKE Standard. IACR Cryptol. ePrint Arch. 2020: 1499 (2020)
2010 – 2019
- 2019
- [c37]Benjamin Lipp, Bruno Blanchet, Karthikeyan Bhargavan:
A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. EuroS&P 2019: 231-246 - [i8]Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno:
SoK: Computer-Aided Cryptography. IACR Cryptol. ePrint Arch. 2019: 1393 (2019) - 2018
- [j16]Martín Abadi, Bruno Blanchet, Cédric Fournet:
The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. J. ACM 65(1): 1:1-1:41 (2018) - [j15]Bruno Blanchet, Ben Smyth:
Automated reasoning for equivalences in the applied pi calculus with barriers. J. Comput. Secur. 26(3): 367-422 (2018) - [c36]Bruno Blanchet:
Composition Theorems for CryptoVerif and Application to TLS 1.3. CSF 2018: 16-30 - 2017
- [c35]Bruno Blanchet:
Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols. CSF 2017: 68-82 - [c34]Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet:
Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. EuroS&P 2017: 435-450 - [c33]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: 483-502 - 2016
- [j14]Bruno Blanchet:
Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Found. Trends Priv. Secur. 1(1-2): 1-135 (2016) - [c32]Bruno Blanchet, Ben Smyth:
Automated Reasoning for Equivalences in the Applied Pi Calculus with Barriers. CSF 2016: 310-324 - [i7]Martín Abadi, Bruno Blanchet, Cédric Fournet:
The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. CoRR abs/1609.03003 (2016) - 2015
- [j13]David Cadé, Bruno Blanchet:
Proved generation of implementations from computationally secure protocol specifications. J. Comput. Secur. 23(3): 331-402 (2015) - 2013
- [j12]Miriam Paiola, Bruno Blanchet:
Verification of security protocols with lists: From length one to unbounded length. J. Comput. Secur. 21(6): 781-816 (2013) - [j11]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): 4-31 (2013) - [c31]Bruno Blanchet, Miriam Paiola:
Automatic verification of protocols with lists of unbounded length. CCS 2013: 573-584 - [c30]Bruno Blanchet:
Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif. FOSAD 2013: 54-87 - [c29]David Cadé, Bruno Blanchet:
Proved Generation of Implementations from Computationally Secure Protocol Specifications. POST 2013: 63-82 - [c28]Vincent Cheval, Bruno Blanchet:
Proving More Observational Equivalences with ProVerif. POST 2013: 226-246 - 2012
- [c27]David Cadé, Bruno Blanchet:
From Computationally-proved Protocol Specifications to Implementations. ARES 2012: 65-74 - [c26]Bruno Blanchet:
Automatically Verified Mechanized Proof of One-Encryption Key Exchange. CSF 2012: 325-339 - [c25]Bruno Blanchet:
Security Protocol Verification: Symbolic and Computational Models. POST 2012: 3-29 - [c24]Miriam Paiola, Bruno Blanchet:
Verification of Security Protocols with Lists: From Length One to Unbounded Length. POST 2012: 69-88 - [p2]Bruno Blanchet:
Mechanizing Game-Based Proofs of Security Protocols. Software Safety and Security 2012: 1-25 - [i6]Bruno Blanchet:
Automatically Verified Mechanized Proof of One-Encryption Key Exchange. IACR Cryptol. ePrint Arch. 2012: 173 (2012) - 2011
- [p1]Bruno Blanchet:
Using Horn Clauses for Analyzing Security Protocols. Formal Models and Techniques for Analyzing Security Protocols 2011: 86-111
2000 – 2009
- 2009
- [j10]Bruno Blanchet:
Automatic verification of correspondences for security protocols. J. Comput. Secur. 17(4): 363-434 (2009) - [c23]Martín Abadi, Bruno Blanchet, Hubert Comon-Lundh:
Models and Proofs of Protocol Security: A Progress Report. CAV 2009: 35-49 - 2008
- [j9]Bruno Blanchet, Martín Abadi, Cédric Fournet:
Automated verification of selected equivalences for security protocols. J. Log. Algebraic Methods Program. 75(1): 3-51 (2008) - [j8]Bruno Blanchet:
A Computationally Sound Mechanized Prover for Security Protocols. IEEE Trans. Dependable Secur. Comput. 5(4): 193-207 (2008) - [c22]Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, Joe-Kai Tsay:
Computationally sound mechanized proofs for basic and public-key Kerberos. AsiaCCS 2008: 87-99 - [c21]Bruno Blanchet, Avik Chaudhuri:
Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage. SP 2008: 417-431 - [i5]Bruno Blanchet:
Automatic Verification of Correspondences for Security Protocols. CoRR abs/0802.3444 (2008) - 2007
- [j7]Martín Abadi, Bruno Blanchet, Cédric Fournet:
Just fast keying in the pi calculus. ACM Trans. Inf. Syst. Secur. 10(3): 9 (2007) - [c20]Bruno Blanchet:
Computationally Sound Mechanized Proofs of Correspondence Assertions. CSF 2007: 97-111 - [i4]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 abs/cs/0701193 (2007) - [i3]Bruno Blanchet:
Computationally Sound Mechanized Proofs of Correspondence Assertions. IACR Cryptol. ePrint Arch. 2007: 128 (2007) - 2006
- [c19]Bruno Blanchet, David Pointcheval:
Automated Security Proofs with Sequences of Games. CRYPTO 2006: 537-554 - [c18]Bruno Blanchet:
A Computationally Sound Mechanized Prover for Security Protocols. S&P 2006: 140-154 - [i2]Bruno Blanchet, David Pointcheval:
Automated Security Proofs with Sequences of Games. IACR Cryptol. ePrint Arch. 2006: 69 (2006) - 2005
- [j6]Bruno Blanchet:
Security protocols: from linear to classical logic by abstract interpretation. Inf. Process. Lett. 95(5): 473-479 (2005) - [j5]Martín Abadi, Bruno Blanchet:
Analyzing security protocols with secrecy types and logic programs. J. ACM 52(1): 102-146 (2005) - [j4]Martín Abadi, Bruno Blanchet:
Computer-assisted verification of a protocol for certified email. Sci. Comput. Program. 58(1-2): 3-27 (2005) - [j3]Bruno Blanchet, Andreas Podelski:
Verification of cryptographic protocols: tagging enforces termination. Theor. Comput. Sci. 333(1-2): 67-90 (2005) - [c17]Xavier Allamigeon, Bruno Blanchet:
Reconstruction of Attacks against Cryptographic Protocols. CSFW 2005: 140-154 - [c16]Bruno Blanchet, Martín Abadi, Cédric Fournet:
Automated Verification of Selected Equivalences for Security Protocols. LICS 2005: 331-340 - [i1]Bruno Blanchet:
A Computationally Sound Mechanized Prover for Security Protocols. IACR Cryptol. ePrint Arch. 2005: 401 (2005) - 2004
- [c15]Martín Abadi, Bruno Blanchet, Cédric Fournet:
Just Fast Keying in the Pi Calculus. ESOP 2004: 340-354 - [c14]Bruno Blanchet:
Automatic Proof of Strong Secrecy for Security Protocols. S&P 2004: 86- - 2003
- [j2]Martín Abadi, Bruno Blanchet:
Secrecy types for asymmetric communication. Theor. Comput. Sci. 298(3): 387-415 (2003) - [j1]Bruno Blanchet:
Escape analysis for JavaTM: Theory and practice. ACM Trans. Program. Lang. Syst. 25(6): 713-775 (2003) - [c13]Bruno Blanchet, Benjamin Aziz:
A Calculus for Secure Mobility. ASIAN 2003: 188-204 - [c12]Bruno Blanchet, Andreas Podelski:
Verification of Cryptographic Protocols: Tagging Enforces Termination. FoSSaCS 2003: 136-152 - [c11]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: 196-207 - [c10]Bruno Blanchet:
Automatic verification of cryptographic protocols: a logic programming approach. PPDP 2003: 1-3 - [c9]Martín Abadi, Bruno Blanchet:
Computer-Assisted Verification of a Protocol for Certified Email. SAS 2003: 316-335 - 2002
- [c8]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: 85-108 - [c7]Martín Abadi, Bruno Blanchet:
Analyzing security protocols with secrecy types and logic programs. POPL 2002: 33-44 - [c6]Bruno Blanchet:
From Secrecy to Authenticity in Security Protocols. SAS 2002: 342-359 - 2001
- [c5]Bruno Blanchet:
An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. CSFW 2001: 82-96 - [c4]Martín Abadi, Bruno Blanchet:
Secrecy Types for Asymmetric Communication. FoSSaCS 2001: 25-41 - [c3]Bruno Blanchet:
Abstracting Cryptographic Protocols by Prolog Rules. SAS 2001: 433-436
1990 – 1999
- 1999
- [c2]Bruno Blanchet:
Escape Analysis for Object-Oriented Languages: Application to Java. OOPSLA 1999: 20-34 - 1998
- [c1]Bruno Blanchet:
Escape Analysis: Correctness Proof, Implementation and Experimental Results. POPL 1998: 25-37
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-12 21:59 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
