I am on leave from Inria, working as co-founder and chief research scientist at Cryspen.

In my academic life, 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), at the Chennai Mathematical Institute, and at IIT Delhi.

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, Hybrid Public Key Encryption, and Messaging Layer Security at the IETF.

Recruitment: At Cryspen, we are looking for both crypto and proof engineers who are excited about building high-assurance cryptographic software using formal analysis techniques. At Inria, we are always on the lookout for excellent Ph.D. students and Post-Docs to work on a variety of topics, including cryptographic protocol design, analysis, and implementation.

Current Projects: Cryspen, HACL*, DY*, hacspec, F*

Past Projects: Project Everest, miTLS, SMACK-TLS,

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

News: