I am a researcher at Inria and LORIA, member of the PESTO team.
I develop and apply formal methods and testing techniques to secure real-world cryptographic protocols, along three lines:
I did my PhD at Ecole Normale Supérieure de Paris-Saclay jointly advised by Stéphanie Delaune and David Baelde and a postdoc at ETH Zurich in David Basin’s Information Security Group.
Download my CV (PDF): full · short (1 page)
I will defend my habilitation (HDR) on Monday, November 2, 2026, at 2:00 PM at LORIA (Nancy). Everyone is welcome, on site or remotely: see the HDR defense page for the committee, abstract, and practical information.
New paper accepted at IEEE Security & Privacy 2027: DDYF: Differential Dolev-Yao Fuzzing of Cryptographic Protocols, with Tom Gouville and Steve Kremer.
New fully funded open positions for a postdoc, a PhD candidate, and a Master's intern.
My ProtoFuzz project (2023-2027) was funded by the ANR (280k euros) as a JCJC project (individual research projects coordinated by young researchers). I am looking for students (research interns, PhD students), postdocs, and engineers to join this research effort. In case you are interested, contact me via email.
Preprint Real World Crypto Talk Media Coverage CNIL - Inria Data Protection 2023 Award
Preprint PDF DOI Black-Hat USA'17 talk Media coverage Video of PoC Models
I serve in the program committee of Usenix Security (2025-), where I received a Distinguished Reviewer Award in 2026 (and was a Notable Reviewer in 2025). I have previously served in the program committee of the European Symposium on Research in Computer Security (ESORICS) (2024), ACM ASIACCS symposium (2023), the Computer Security track at the ACM Symposium on Applied Computing (SEC@SAC) (2019-2022), and the HotSpot workshop (affiliated with IEEE European Symposium on Security and Privacy) (2021). I have been an external scientific expert for the ANR (French National Agency for Research) Generic Call in 2019 and 2020, and for the Flanders Innovation & Entrepreneurship agency VLAIO (Flemish Government) in 2025. I have reviewed papers for CCS, CSF, Euro S&P, ACM TOPS, JCS, etc.
I serve as the president of the jury (2025-) of the best PhD artifact award of the GDR Sécurité. I am also in the program committee (2024-) of the Gilles Kahn Thesis Award of the Société Informatique de France (SIF) (annual award for the best French thesis in computer science). I am a local member of the Legal and Ethical Risk Assessment Committee (COERLE) of Inria. I co-organized the GDR Sécurité summer school Cyber in Nancy 2022. I was a member of the 2025 jury grading the “Info A” entrance exam of the French “Grandes Écoles” ENS.
I am the PI of the ProtoFuzz project (2023-2027) funded by ANR JCJC (280k euros). I am or was a member of the France 2030 ANR PEPR Cybersécurité (SVP) (2022-2026) and ANR Chair IA ASAP project (2020-2024). I was co-coordinator of a joint project between Huawei Technologies Singapore Research Center and ETH Zurich on 5G protocols (2018-2019). I have participated in the following projects: ANR Chair of research and teaching in artificial intelligence (ASAP), ERC Consolidator Grant SPOOC, ERC Starting Grant POPSTAR, ANR project Sequoia, ANR project ProSe, ANR JCJC project VIP.
We designed and developed a new kind of model-guided fuzzer. The novel idea is to use the security-related Dolev-Yao formal model to guide the fuzzer towards finding logical attacks in security protocol implementations. Developed with Max Ammann (master's intern and then security engineer at Trail of Bits), Tom Gouville (PhD student), Nataël Baffou, Olivier Demengeon, and Michael Mera (research engineers). Research conducted with T. Gouville, M. Ammann, and S. Kremer.
Porridge is a standalone OCaml library implementing Partial Order Reduction techniques for checking trace equivalence of security protocols. It is not restricted to the limited class of action-deterministic protocols as in prior works. It has been successfully integrated into two state-of-the-art verifiers DeepSec and Apte, bringing significant speedups. Theory and practical results are described in our ESORICS’18 paper.
UKano is a tool that enables the automatic formal verification of unlinkability and anonymity for a large class of 2-agents protocols that was previously out of scope. It has been notably used to discover new attacks on ePassport protocols. I have written this tool by leveraging our new verification method proposed in our S&P’16 paper.