I am a researcher at Inria and LORIA, member of the PESTO team.
My research interests mainly focus on formal methods for security and privacy. I design new verification techniques, algorithms, and tools to analyze formal security properties. I generally enjoy research projects that combine both foundational contributions and practical applications, including analyzing real-world cryptographic protocols. More recently, I also took a great interest in fuzz testing techniques.
I did my PhD at Ecole Normale Supérieure de Cachan jointly advised by Stéphanie Delaune and David Baelde and a postdoc at ETH Zurich in the David Basin’s Information Security Group.
Download my CV (PDF)
I am honored to have received the CNIL - Inria Data Protection 2023 Award with Alexandre Debant for our work on analyzing the security of the e-voting protocol used for the 2022 French legislative election (see below).
New paper accepted at Usenix Security'24 where we propose a new protocol that turns OpenID into a mechanism that delivers transferable proofs of eligibility in e-voting. Using zk-SNARK proofs, we show that this can be done without revealing any sensitive information.
New paper accepted at IEEE Security & Privacy'24 where we propose a new fuzzing technique (Dolev-Yao model-guided Fuzzing). We provide a full-fledged implementation of such a DY fuzzer in Rust with our tool tlspuffin, which found four new CVEs on WolfSSL, including one critical and two high CVEs.
New paper accepted at Usenix'23 and presented at Real World Crypto (contributed talk) on the e-voting protocol used during the 2022 French legislative election, which was the largest ever political election using e-voting in the world. We reversed the protocol, found 6 verifiability and privacy attacks on the protocol, and proposed fixes, most of them have been deployed. We also presented this work at Real World Crypto'23. Media coverage: here, there, and there.
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-). 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 29th 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 external scientific experts for the ANR (French National Agency for Research) Generic Call 2019-2020. I have reviewed papers for CCS, CSF, Euro S&P, ACM TOPS, JCS, etc.
I am the PI of the ProtoFuzz project (2023-2027) funded by ANR JCJ (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), joint project between Huawei Technologies Singapore Research Center and ETH Zurich on 5G protocols (2018-2019). I have participated to the following projects: ANR Chair of research and teaching in artificial intelligence (ASAP), ERC Consolidator Grant SPOOC, ERC Starting Grant POPSTAR, various ANR projects.
We developed with Max Ammann (main developer, security engineer at Trail of Bits), Tom Gouville (PhD student), and Michael Mera (research engineer) a fuzzer implementing a novel model-guided kind of fuzzer. The novel idea is to use the security-related domain-specific Dolev-Yao formal model to guide the fuzzer towards finding logical attacks in security protocols. Research conducted with 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.
I have developed and implemented Partial Order Reduction techniques for a class of security protocols (those that are action-deterministic) in the tool Apte, dramatically improving its practical impact. I also have implemented a preliminary version of those techniques in the tool SPEC (more details).