Skip to Main content Skip to Navigation


hal-00939187v1  Journal articles
Miriam PaiolaBruno Blanchet. Verification of Security Protocols with Lists: from Length One to Unbounded Length
Journal of Computer Security, IOS Press, 2013, 21 (6), pp.781--816
...
hal-00863387v1  Conference papers
Miriam PaiolaBruno Blanchet. Verification of Security Protocols with Lists: from Length One to Unbounded Length
First Conference on Principles of Security and Trust (POST'12), 2012, Tallinn, Estonia. pp.69--88
...
hal-01575920v2  Conference papers
Karthikeyan BhargavanBruno BlanchetNadim Kobeissi. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate
38th IEEE Symposium on Security and Privacy, May 2017, San Jose, United States. pp.483 - 502, ⟨10.1109/SP.2017.26⟩
...
hal-01423760v1  Journal articles
Bruno Blanchet. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif
Foundations and Trends® in Privacy and Security , Now publishers inc, 2016, 1 (1-2), pp.1 - 135. ⟨10.1561/3300000004⟩
hal-01102136v1  Book sections
Bruno Blanchet. Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif
Alessandro Aldini; Javier Lopez; Fabio Martinelli. Foundations of Security Analysis and Design VII, 8604, Springer, pp.54-87, 2014, Lecture Notes in Computer Science, 978-3-319-10081-4. ⟨10.1007/978-3-319-10082-1_3⟩
...
hal-01764527v1  Reports
Bruno Blanchet. Composition Theorems for CryptoVerif and Application to TLS 1.3
[Research Report] RR-9171, Inria Paris. 2018, pp.67
hal-01110443v1  Conference papers
Bruno Blanchet. A second look at {S}houp's lemma
FCC 2011 - Seventh Workshop on Formal and Computational Cryptography, Jun 2011, Paris, France
...
hal-02396640v1  Conference papers
Benjamin LippBruno BlanchetKarthikeyan Bhargavan. A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol
4th IEEE European Symposium on Security and Privacy, Jun 2019, Stockholm, Sweden. pp.231-246
hal-00863377v1  Conference papers
Vincent ChevalBruno Blanchet. Proving More Observational Equivalences with ProVerif
POST 2013 - 2nd Conference on Principles of Security and Trust, Mar 2013, Rome, Italy. pp.226-246, ⟨10.1007/978-3-642-36830-1_12⟩
...
hal-01947972v1  Journal articles
Bruno BlanchetBen Smyth. Automated reasoning for equivalences in the applied pi calculus with barriers
Journal of Computer Security, IOS Press, 2018, 26 (3), pp.367 - 422. ⟨10.3233/JCS-171013⟩
...
hal-01947959v1  Conference papers
Bruno Blanchet. Composition Theorems for CryptoVerif and Application to TLS 1.3
31st IEEE Computer Security Foundations Symposium (CSF'18), Jul 2018, Oxford, United Kingdom. ⟨10.1109/CSF.2018.00009⟩
...
hal-00863382v1  Conference papers
David CadéBruno Blanchet. From Computationally-proved Protocol Specifications to Implementations
7th International Conference on Availability, Reliability and Security (AReS 2012), 2012, Prague, Czech Republic. pp.65--74
...
hal-03113251v2  Reports
Joël AlwenBruno BlanchetEduard HauckEike KiltzBenjamin Lipp et al.  Analysing the HPKE Standard
[Research Report] IACR Cryptology ePrint Archive. 2020
hal-01110425v1  Book sections
Bruno Blanchet. Using Horn Clauses for Analyzing Security Protocols
Véronique Cortier; Steve Kremer. Formal Models and Techniques for Analyzing Security Protocols, 5, IOS Press, pp.86 - 111, 2011, Cryptology and Information Security Series, 978-1-60750-713-0. ⟨10.3233/978-1-60750-714-7-86⟩
hal-00918849v1  Conference papers
Bruno BlanchetMiriam Paiola. Automatic Verification of Protocols with Lists of Unbounded Length
CCS'13 - ACM Conference on Computer and Communications Security, ACM SIGSAC, Nov 2013, Berlin, Germany. pp.573--584, ⟨10.1145/2508859.2516679⟩
...
hal-00863388v1  Conference papers
Bruno Blanchet. Security Protocol Verification: Symbolic and Computational Models
First Conference on Principles of Security and Trust (POST'12), 2012, Tallinn, Estonia. pp.3--29
...
hal-03366962v1  Conference papers
Bruno BlanchetVincent ChevalVéronique Cortier. ProVerif with Lemmas, Induction, Fast Subsumption, and Much More
S&P'22 - 43rd IEEE Symposium on Security and Privacy, May 2022, San Francisco, United States
hal-01102382v1  Journal articles
David CadéBruno Blanchet. Proved Generation of Implementations from Computationally Secure Protocol Specifications
Journal of Computer Security, IOS Press, 2015, 23 (3), pp.331-402
...
hal-03046757v1  Conference papers
Manuel BarbosaGilles BartheKarthik BhargavanBruno BlanchetCas Cremers et al.  SoK: Computer-Aided Cryptography
SP 2021 - 42nd IEEE Symposium on Security and Privacy, May 2021, Virtual Conference, United States
...
hal-01575861v1  Conference papers
Bruno Blanchet. Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols
30th IEEE Computer Security Foundations Symposium, Aug 2017, Santa Barbara, United States. pp.68-82, ⟨10.1109/CSF.2017.7⟩
...
hal-01423742v1  Conference papers
Bruno BlanchetBen Smyth. Automated Reasoning for Equivalences in the Applied Pi Calculus with Barriers
29th IEEE Computer Security Foundations Symposium (CSF'16), Jun 2016, Lisboa, Portugal. pp.310 - 324, ⟨10.1109/CSF.2016.29⟩
...
hal-00863389v1  Book sections
Bruno Blanchet. Mechanizing Game-Based Proofs of Security Protocols
Tobias Nipkow and Olga Grumberg and Benedikt Hauptmann. Software Safety and Security - Tools for Analysis and Verification, 33, IOS Press, pp.1--25, 2012, NATO Science for Peace and Security Series ― D: Information and Communication Security
...
hal-03471218v1  Conference papers
Joël AlwenBruno BlanchetEduard HauckEike KiltzBenjamin Lipp et al.  Analysing the HPKE Standard
Eurocrypt 2021 - 40th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Oct 2021, Zagreb, Croatia. pp.87-116, ⟨10.1007/978-3-030-77870-5_4⟩