DY* Unchained: Now with Composable Security Proofs and Precise Compromise Scenarios
to appear at IEEE S&P 2026.
A Verification Framework for Secure Group Messaging
Thesis manuscript.
[hal]
[pdf]
TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security
IEEE S&P 2025.
[doi]
[eprint]
Comparse: Provably Secure Formats for Cryptographic Protocols
ACM CCS 2023.
[doi]
[eprint]
TreeSync: Authenticated Group Management for Messaging Layer Security
USENIX Security '23.
[USENIX]
[eprint]
This paper won the Internet Defense Prize and received a Distinguished Paper Award.
The Messaging Layer Security (MLS) Protocol
IETF RFC (contributor).
[datatracker]
[rfc]
I am an active participant in the IETF MLS working group, where I authored several key improvements such as the disambiguation of signatures and the strengthening of group membership agreement.
Co-winner of the 2023 Internet Defense Prize.
Distinguished Paper Award at USENIX Security ‘23.
Sub-reviewer:
Artifact Evaluation Committee:
Systèmes numériques at ENS Paris (Sept. 2024 - Jan 2025)
Systèmes numériques at ENS Paris (Sept. 2023 - Jan 2024)
Systèmes numériques at ENS Paris (Sept. 2022 - Jan 2023)
Systèmes numériques at ENS Paris (Sept. 2021 - Jan 2022)
Proofs of Security Protocols in Lean
at Google Seattle.
[slides]
[recording]
1-hour talk discussing Bob DyLean, an ongoing project to enable symbolic analysis of cryptographic protocols using Lean. The target audience is people familiar with program verification but unfamiliar with cryptographic protocols, such as Lean developers.
TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security
at IEEE S&P 2025.
[slides]
8-minutes talk for the eponymous paper, given at IEEE S&P 2025.
Formally analyzing a cryptographic protocol standard (or: how MLS kept this PhD student busy for three years)
at Real World Crypto 2025.
[slides]
[recording]
20-minutes talk giving an overview on my work on formally verifying MLS, and lessons learned throughout this journey.
Comparse: Provably Secure Formats for Cryptographic Protocols
at ACM CCS 2023.
[slides]
12-minutes talk for the eponymous paper, given at ACM CCS 2023.
"Don't roll your own crypto": les méthodes formelles au service de la sécurité
at Devfest Toulouse (in french).
[recording]
[slides]
I gave a short talk at Devfest Toulouse 2019, giving a brief overview of what formal methods can be used for (aimed at developers who never heard of this).
End-to-End Encrypted Group Chats with MLS: Design, Implementation and Verification
at Microsoft Research (08/2023) ; Cornell Tech (08/2023) ; IRISA (01/2024) ; NYU (03/2024) ; MIT (04/2024).
[slides]
[slides v2]
This is the long version (45 to 60 minutes) of the talk for the paper “TreeSync: Authenticated Group Management for Messaging Layer Security”, given at various places.
The second version of the slides include a digression on the paper “Comparse: Provably Secure Formats for Cryptographic Protocols”, to explain more deeply what happened behind the signature ambiguity attack.
TreeSync: Authenticated Group Management for Messaging Layer Security
at USENIX Security '23.
[slides]
[recording]
12-minutes talk for the eponymous paper, given at USENIX Security ‘23.
Applications de Brainfuck, langage minimaliste mais Turing-complet
at Devfest Toulouse (in french).
[recording]
[slides]
I gave a short talk at Devfest Toulouse 2019, explaining how it was humanly possible to write useful Brainfuck programs. After explaining the syntax of the language, I explained some useful code patterns such as conditions or array management, which allow to write complex programs.
Des tuyaux pour se qualifier au baseball
at Informatique pour Tous (in french).
[recording]
[slides]
I gave a talk that was aimed to explain a computer science notion for high-school student. I decided to explain the max-flow min-cut theorem and the Ford-Fulkerson algorithm, applied on a problem of deciding whether a baseball team can still qualify or not. I definitely lacked a lot of presentation skills (you can count the “euuuuh”), however I think I found the simplest explanations for the max-flow alogrithm.
A verification framework for secure machine learning
Internship for 2nd year of Master's Degree at INRIA, Paris.
With
[PDF]
[slides]
I worked five months in the Prosecco team at INRIA. I wrote a global and local specifications for the online phase of the SPDZ2k protocol, and proved that they computed the same thing.
Faster CakeML compilation with a verified linear scan register allocator
Internship for 1st year of Master's Degree at Chalmers, Göteborg (Sweden).
With
[PDF]
[slides]
I worked five months in the CakeML team to implement a verified linear-scan register allocator. The motivation was that the register allocation was the slowest part of the compilation process, hence a faster algorithm could drastically reduce compilation time.
Détection automatique des adresses exploitables d'un algorithme de cryptographie par timing du cache processeur
Internship for 3rd year of Bachelor's Degree at Secure-IC, Paris.
With
[PDF]
[slides]
I worked two months on cache timing attacks (before Spectre or Meltdown were known). I found a procedure to analyse a cryptographic library and automatically find parts of the code which break secret independance, and might leak a private key to an attacker running on the same computer.