I am a researcher (directeur de recherche) at Inria, where I lead the Prosecco project ("Programming Securely with Cryptography") at INRIA Paris. I am a fellow (chaire) at the Prairie research institute. I also teach part-time at the Master Parisien de Recherche en Informatique (MPRI).

My research concerns the design and implementation of new program verification techniques that would enable formal analyses of real-world security applications. My recent work focuses on using dependent type systems, such as F*. to investigate the (in)security of cryptographic protocols, such as TLS, and to build verified cryptographic libraries, such as HACL*. A full list of my publications is available from my publications page.

I have recently been involved in the design, analysis, and standardization of TLS 1.3 and Messaging Layer Security at the IETF.

My work is primarily funded by an ERC Consolidator Grant, titled "CIRCUS: Certified Implementations of Robust, Cryptographically Secure Components". I also receive some funds from the ANR SafeTLS grant. I contribute to the Microsoft Everest Expedition.

Projects: HACL*, Project Everest, miTLS, F*, RefTLS, SMACK-TLS,

Program Committees: Real World Crypto 2020, IEEE S&P 2020, ACM CCS 2020, IEEE CSF 2016,2020, Applied Cryptography and Network Security 2020

Current PhD Students: Benjamin Beurdouche, Marina Polubelova, Natalia Kulatova, Denis Merigoux, Benjamin Lipp
Past PhD Students: Evmorfia-Iro Bartzia, Antoine Delignat-Lavaud, Jean Karim Zinzdohoue, Nadim Kobeissi

Positions: We are always on the lookout for outstanding interns, PhD candidates, and Post-Doctoral researchers. To apply, send me an email with your CV and a short research statement.
mailing address: INRIA, 2 rue Simone Iff, Paris 75012, France
email: <firstName>.<lastName>@inria.fr

News: