Publications

Conferences

• Preservation of Speculative Constant-Time by Compilation (Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte) [POPL, 2025]
  

• Protecting Cryptographic Code Against Spectre-RSB (Santiago Arranz Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang) [ASPLOS, 2025]
  

• Leakage-Free Probabilistic Jasmin Programs (José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh) [CPP, ‘25]
  

• X-Wing The Hybrid KEM You’ve Been Looking For (Manuel Barbosa, Deirdre Connolly, João Diogo Duarte, Aaron Kaiser, Peter Schwabe, Karolin Varner, Bas Westerbaan) [Communications in Cryptology, vol. 1, no. 1, 2024]
  

• Testing Side-channel Security of Cryptographic Implementations against Future Microarchitectures (Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, Yuval Yarom) [CCS, ‘24]
  

• SwooSh: Efficient Lattice-Based Non-Interactive Key Exchange (Phillip Gajland, Bor de Kock, Miguel Quaresma, Giulio Malavolta, and Peter Schwabe) [SEC, 2024]
  

• Machine-Checked Proofs of Accountability: How to sElect Who is to Blame (Constantin Cătălin Drăgan, François Dupressoir, Kristian Gjøsteen, Thomas Haines, Peter B. Rønne, Morten Rotvold Solberg) [ESORICS, 2024]
  

• Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs (Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, Gabriele Vanoni) [PACMPL, ‘24]
  

• Formally Verifying Kyber Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt (José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub) [CRYPTO, 2024]
  

• A Tight Security Proof for SPHINCS\(^{+}\), Formally Verified (Manuel Barbosa, François Dupressoir, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub) [ASIACRYPT, 2024]
  

• Zero-Knowledge in EasyCrypt (Denis Firsov and Dominique Unruh) [CSF, 2023]
  

• Spectre Declassified: Reading from the Right Place at the Wrong Time (Basavesh Ammanaghatta Shivakumar, Jack Barnes, Gilles Barthe, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Sioli O’Connell, Peter Schwabe, Rui Qi Sim, Yuval Yarom) [S&P, 2023]
  

• Rogue key and impersonation attacks on FIDO2: From theory to practice (Manuel Barbosa, André Cirne, Luís Esquível) [ARES, ‘23]
  

• Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with Coq-Elpi (Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi) [CPP, ‘23]
  

• Machine-checked proofs of privacy against malicious boards for Selene & Co (Constantin Cătălin Drăgan, François Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y.A. Ryan, Peter B. Rønne, Morten Rotvold Solberg) [JCS, 2023]
  

• Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS⁺ (Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub) [CRYPTO, 2023]
  

• Typing High-Speed Cryptography against Spectre v1 (Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, and Lucas Tabary-Maujean) [S&P, 2023]
  

• High-assurance zeroization (Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe) [IACR, 2023]
  

• Formally verifying Kyber Part IV: Implementation Correctness (José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub) [TCHES, 2023]
  

• Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium (Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu) [CRYPTO, 2023]
  

• Execution Time Program Verification with Tight Bounds (Ana Carolina Silva, Manuel Barbosa, Mário Florido) [PADL, 2023]
  

• Verified Password Generation from Password Composition Policies (Miguel Grilo, João Campos, João F. Ferreira, José Bacelar Almeida, Alexandra Mendes) [IFM, 2022]
  

• SoK: Practical Foundations for Software Spectre Defenses (Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan) [S&P, 2022]
  

• Formal Verification of Saber’s Public-Key Encryption Scheme in EasyCrypt (Andreas Hülsing, Matthias Meijers, and Pierre-Yves Strub) [CRYPTO, 2022]
  

• Enforcing fine-grained constant-time policies (Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya) [CCS, 2022]
  

• Bringing State-Separating Proofs to EasyCrypt A Security Proof for Cryptobox (François Dupressoir, Konrad Kohbrok, Sabine Oechsner) [CSF, 2022]
  

• A formal treatment of the role of verified compilers in secure computation (José Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela) [JLAMP, 2022]
  

• SoK: Computer-Aided Cryptography (Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno) [S&P, 2021]
  

• Provable Security Analysis of FIDO2 (Manuel Barbosa, Alexandra Boldyreva, Shan Chen, Bogdan Warinschi) [CRYPTO, 2021]
  

• Mechanized Proofs of Adversarial Complexity and Application to Universal Composability (Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub) [CCS, ‘21]
  

• Mechanised Models and Proofs for Distance-Bounding (Ioana Boureanu, Constantin Cătălin Drăgan, François Dupressoir, David Gérault, Pascal Lafourcade) [CSF, 2021]
  

• Machine-Checking Unforgeability Proofs for Signature Schemes with Tight Reductions to the Computational Diffie-Hellman Problem (François Dupressoir, Sara Zain) [CSF, 2021]
  

• Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head (José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira) [CCS, ‘21]
  

• EasyPQC: Verifying Post-Quantum Cryptography (Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou) [CCS, ‘21]
  

• Structured Leakage and Applications to Cryptographic Constant-Time and Cost (Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya) [CCS, 2020]
  

• Security Analysis of ElGamal Implementations (Mohamad El Laz, Benjamin Grégoire, Tamara Rezk) [ICETE, 2020]
  

• High-Assurance Cryptography in the Spectre Era (Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, and Peter Schwabe) [S&P, 2020]
  

• Formal verification of a constant-time preserving C compiler (Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu) [PACMPL, ‘20]
  

• Constant-time foundations for the new spectre era (Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe) [PLDI, 2020]
  

• Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification (José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira) [INDOCRYPT, 2020]
  

• maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults (Gilles Barthe, Sonia Belaïd, Gaëtan Cassiers, Pierre-Alain Fouque, Benjamin Grégoire, Francois-Xavier Standaert) [ESORICS, 2019]
  

• Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3 (José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, and Pierre-Yves Strub) [CCS, 2019]
  

• The Last Mile: High-Assurance and High-Speed Cryptographic Implementations (José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, and Pierre-Yves Strub) [S&P, 2019]
  

• FaCT: a DSL for timing-sensitive computation (Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan) [PLDI, 2019]
  

• EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security (Ran Canetti, Alley Stoughton, Mayank Varia) [CSF, 2019]
  

• A Machine-Checked Proof of Security for AWS Key Management Service (José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Gregoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran) [CCS, ‘19]
  

• Proving expected sensitivity of probabilistic programs (Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub) [PACMPL, ‘18]
  

• Formal Security Proof of CMAC and Its Variants (Cecile Baritel-Ruet, Francois Dupressoir, Pierre-Alain Fouque, Benjamin Gregoire) [CSF, 2018]
  

• Mechanizing the Proof of Adaptive, Information-Theoretic Security of Cryptographic Protocols in the Random Oracle Model (Alley Stoughton, Mayank Varia) [CSF, 2017]
  

• Jasmin: High-assurance and high-speed cryptography (José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub) [CCS, 2017]
  

• A Fast and Verified Software Stack for Secure Function Evaluation (José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, and Vitor Pereira) [CCS, 2017]
  

• Coupling proofs are probabilistic product programs (Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub) [POPL, 2017]
  

• A Fast and Verified Software Stack for Secure Function Evaluation (José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira) [CCS, ‘17]
  

• Verifying constant-time implementations (José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi) [SEC, 2016]
  

• Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC (José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir) [FSE, 2016]
  

• Strong Non-Interference and Type-Directed Higher-Order Masking (Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, and Rébecca Zucchini) [CCS, 2016]
  

• Proving Differential Privacy via Probabilistic Couplings (Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub) [LICS, 2016]
  

• Computer-Aided Verification for Mechanism Design (Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub) [WINE, 2016]
  

• Advanced Probabilistic Couplings for Differential Privacy (Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub) [CCS, ‘16]
  

• Relational Reasoning via Probabilistic Coupling (Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub) [LPAR, 2015]
  

• Automated Proofs of Pairing-Based Cryptography (Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt) [CCS, ‘15]
  

• Synthesis of Fault Attacks on Cryptographic Implementations (Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz) [CCS, ‘14]
  

• Proving the TLS Handshake Secure (As It Is) (Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin) [CRYPTO, 2014]
  

• Proving Differential Privacy in Hoare Logic (Gilles Barthe, Marco Gaboardi, Emilio Jesus Gallego Arias, Justin Hsu, Cesar Kunz, Pierre-Yves Strub) [CSF, 2014]
  

• Probabilistic relational verification for cryptographic implementations (Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin) [POPL, 2014]
  

• Making RSA–PSS Provably Secure against Non-random Faults (Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz) [CAiSE, 2014]
  

• EasyCrypt: A Tutorial (Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub) [FOSAD, 2014]
  

• Certified Synthesis of Efficient Batch Verifiers (Joseph A. Akinyele, Gilles Barthe, Benjamin Gregoire, Benedikt Schmidt, Pierre-Yves Strub) [CSF, 2014]
  

• Verified Computational Differential Privacy with Applications to Smart Metering (Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, and Santiago Zanella-Beguelin) [CSF, 2013]
  

• Fully automated analysis of padding-based encryption in the computational model (Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella-Béguelin) [CCS, ‘13]
  

• Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations (José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir) [CCS, ‘13]
  

• Verified Security of Merkle-Damgård (Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Gregoire, Cesar Kunz, Malte Skoruppa, Santiago Zanella Beguelin) [CSF, 2012]
  

• Verified Indifferentiable Hashing into Elliptic Curves (Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin) [POST, 2012]
  

• Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs (Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin) [MPC, 2012]
  

• Computer-Aided Cryptographic Proofs (Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin) [ITP, 2012]
  

• Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs (Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin) [CPP, 2012]
  

• Computer-Aided Security Proofs for the Working Cryptographer (Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin) [CRYPTO, 2011]
  

Theses

• Formally computer-verified protections against timing-based side-channel attacks (Swarn Priya) [2023]
  

• High-speed and High-assurance Cryptographic Software (Tiago Oliveira) [2022]
  

• Formal Security Proofs of Cryptographic Standards (Cécile Baritel-Ruet) [2020]
  

Preprints

• Transparent Decompilation for Timing Side-Channel Analyses (Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Sören van der Wall, Zhiyuan Zhang) [arXiv, 2025]
  

• Agile, Post-quantum Secure Cryptography in Avionics (Karolin Varner, Wanja Zaeske, Sven Friedrich, Aaron Kaiser, Alice Bowman) [IACR, 2024]
  

• Schnorr Protocol in Jasmin (Josè Bacelar Almeida, Denis Firsov, Tiago Oliveira, and Dominique Unruh) [IACR, 2023]
  

• A Note on ‘Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity’ (Gilles Barthe, François Dupressoir, Benjamin Grégoire) [IACR, 2017]