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]
  

• Zero-Knowledge in EasyCrypt (Denis Firsov and Dominique Unruh) [CSF, 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]
  

• 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]
  

• Structured Leakage and Applications to Cryptographic Constant-Time and Cost (Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya) [CCS, 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]
  

• 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]
  

• 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]
  

• 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, 2019]
  

• 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]
  

• 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

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