Year

Venue

Title

2025

journals/tches

Let's DOIT: Using Intel's Extended HW/SW Contract for Secure Compilation of Crypto Code.

Santiago Arranz-Olmos Gilles Barthe Benjamin Grégoire Jan Jancar Vincent Laporte Tiago Oliveira Peter Schwabe

2024

journals/tches

High-assurance zeroization.

Santiago Arranz-Olmos Gilles Barthe Ruben Gonzalez Benjamin Grégoire Vincent Laporte Jean-Christophe Léchenet Tiago Oliveira Peter Schwabe

2024

journals/joc

Masking the GLP Lattice-Based Signature Scheme at Any Order.

Gilles Barthe Sonia Belaïd Thomas Espitau Pierre-Alain Fouque Benjamin Grégoire Mélissa Rossi Mehdi Tibouchi

2024

conf/crypto

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

2023

journals/tches

Formally verifying Kyber Episode 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

2023

conf/crypto

Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $.

Manuel Barbosa François Dupressoir Benjamin Grégoire Andreas Hülsing Matthias Meijers Pierre-Yves Strub

2023

conf/crypto

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

2023

conf/sp

Typing High-Speed Cryptography against Spectre v1.

Basavesh Ammanaghatta Shivakumar Gilles Barthe Benjamin Grégoire Vincent Laporte Tiago Oliveira Swarn Priya Peter Schwabe Lucas Tabary-Maujean

2022

conf/ccs

Enforcing Fine-grained Constant-time Policies.

Basavesh Ammanaghatta Shivakumar Gilles Barthe Benjamin Grégoire Vincent Laporte Swarn Priya

2021

journals/tches

Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification.

Gilles Barthe Marc Gourjon Benjamin Grégoire Maximilian Orlt Clara Paglialonga Lars Porth

2021

conf/ccs

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

2021

conf/ccs

Mechanized Proofs of Adversarial Complexity and Application to Universal Composability.

Manuel Barbosa Gilles Barthe Benjamin Grégoire Adrien Koutsos Pierre-Yves Strub

2021

conf/ccs

Structured Leakage and Applications to Cryptographic Constant-Time and Cost.

Gilles Barthe Benjamin Grégoire Vincent Laporte Swarn Priya

2021

conf/sp

High-Assurance Cryptography in the Spectre Era.

Gilles Barthe Sunjay Cauligi Benjamin Grégoire Adrien Koutsos Kevin Liao Tiago Oliveira Swarn Priya Tamara Rezk Peter Schwabe

2020

conf/sp

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 Pierre-Yves Strub

2019

conf/ccs

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 Pierre-Yves Strub

2019

conf/ccs

A Machine-Checked Proof of Security for AWS Key Management Service.

José Bacelar Almeida Manuel Barbosa Gilles Barthe Matthew Campagna Ernie Cohen Benjamin Grégoire Vitor Pereira Bernardo Portela Pierre-Yves Strub Serdar Tasiran

2019

conf/esorics

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 François-Xavier Standaert

2018

conf/ccs

Symbolic Proofs for Lattice-Based Cryptography.

Gilles Barthe Xiong Fan Joshua Gancher Benjamin Grégoire Charlie Jacomme Elaine Shi

2018

conf/eurocrypt

Masking the GLP Lattice-Based Signature Scheme at Any Order.

Gilles Barthe Sonia Belaïd Thomas Espitau Pierre-Alain Fouque Benjamin Grégoire Mélissa Rossi Mehdi Tibouchi

2017

conf/ccs

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

2017

conf/ccs

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 Pierre-Yves Strub

2017

conf/eurocrypt

Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model.

Gilles Barthe François Dupressoir Sebastian Faust Benjamin Grégoire François-Xavier Standaert Pierre-Yves Strub

2016

conf/ccs

Advanced Probabilistic Couplings for Differential Privacy.

Gilles Barthe Noémie Fong Marco Gaboardi Benjamin Grégoire Justin Hsu Pierre-Yves Strub

2016

conf/ccs

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 Rébecca Zucchini