Conferences

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