I am a researcher (directeur de recherche) at Inria, where I lead the Prosecco project ("Programming Securely with Cryptography") at INRIA Paris. I also teach part-time at Ecole Polytechnique and 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 large security-critical applications. My recent work focuses on using dependent type systems, such as F*. to investigate the (in)security of cryptographic protocols, such as TLS. A full list of my publications is available from my publications page.
- Paper@ICFP, September 2017
Our paper on generating C code from verified F* programs appears at ICFP 2017.
- Award@Oakland, May 2017
Our paper on verifying TLS 1.3 using ProVerif and CryptoVerif was awarded the Distinguished Paper award at IEEE S&P (Oakland 2017).
- Papers@Oakland, May 2017
We had two papers on TLS 1.3 at IEEE S\&P (Oakland) 2017.
- Invited Talk@ACNS, July 2017
I gave an invited talk on High Assurance Cryptographic Software at ACNS 2016
- Impact@NIST, July 2017
NIST deprecated 3DES, partly due to our Sweet32 paper at CCS 2016.
- Papers@EuroS&P, April 2017
We had two papers at Euro S&P 2017, which was organized by my group in Paris.
- Award@France, November 2016
I was awarded the Prix Jeune Chercheur Inria – Academie des sciences 2016.
- Award@MSR, July 2016
I was given one of the Microsoft Research Outstanding Collaborator Awards
- Invited Talk@EUROCRYPT, May 2016
I gave an invited talk on protecting TLS against legacy crypto at EUROCRYPT 2016
- Paper@S&P, May 2016
Our paper on downgrade resilience in TLS, SSH, and IPsec appeared at IEEE S&P (Oakland) 2016
- Award@NDSS, February 2016
Our SLOTH paper on weak hash functions wins a Best Paper award at ISOC NDSS 2016
- Levchin Prize, January 2016
The miTLS project wins the Levchin Prize for significant contributions to real-world cryptography
- Sloth Attack, January 2016
We disclosed Sloth, a new attack on many TLS clients and servers, triggering security updates to many TLS libraries and web servers.
Some press: Register, Ars Technica
- Award@CCS, October 2015
Our Logjam paper on weak Diffie-Hellman groups wins a Best Paper award at ACM CCS 2015
- Paper@POPL 2016
Our paper on the new F* was accepted at POPL 2016
- Grant@Mozilla, October 2015
Mozilla Corporation has awarded our team a research grant to support our research on verifying TLS 1.3.
- Standard@IETF, September 2015
RFC 7627 our proposal to prevent the Triple Handshake attacks on TLS becomes an Internet standard.
- Song@CRYTPO, August 2015
Cryptographers sing "500 bits - Implementor's Lament": a concise summary of our recent attacks, Freak and Logjam, at the CRYPTO rump session.
- Award@WOOT, August 2015
Our paper on FlexTLS: a tool for testing TLS implementations won the Best Paper award at WOOT 2015
- Award@BlackHat, August 2015
Our paper on Logjam won a Pwnie award for Most Innovative Research at BlackHat 2015
- Award@S&P, May 2015
Our paper on state machine flaws in TLS implementations won the Distinguished Paper award at IEEE S&P (Oakland) 2015
- Logjam Attack, May 2015
We disclosed Logjam, a new attack on many TLS clients and servers, triggering security updates to many web browsers.
Security updates for Logjam: OpenSSL, Firefox, Windows, IBM
Some press: Wall Street Journal, Ars Technica, ZDnet
- Paper@WWW, May 2015
Our paper on origin confusion attacks on web servers appeared at WWW 2015
- FREAK Attack, March 2015
We disclosed FREAK, a new attack on TLS clients and servers, resulting in security updates to mainstream web browsers and TLS libraries.
Security updates for FREAK: OpenSSL, Windows, Apple
Some press: Washington Post, BBC, Figaro, New York Times, Guardian
- Paper@NDSS, February 2015
Our paper on analysing channel bindings in TLS, SSH, and IPsec appeared at NDSS 2015
- Talk@BlackHat, August 2014
Antoine Delignat-Lavaud presented our various new attacks on TLS and HTTPS at BlackHat USA 2014
- Paper@CRYPTO, July 2014
Our paper on proving security for an implementation of the TLS Handshake appeared at CRYPTO 2014
- Paper@S&P, May 2014
Our paper on triple handshake and cookie cutter attacks on TLS appeared at Oakland (IEEE S&P) 2014.
- Triple Handshake Attack, March 2014
We presented Triple Handshake attacks on authentication over TLS to the TLS working group at IETF'89.
Security updates (CVEs) for triple handshake attacks: Google Chrome, Mozilla NSS, Apple Safari/SecureTransport.
Some press: [1, 2, 3, 4, 5, 6, 7]
- Paper@POPL, January 2014
- Cookie Cutter Attack, October 2013
Security updates (CVEs) for cookie cutter attacks: Google Chrome, Apple Safari/CFNetwork
Positions: We are always on the lookout for outstanding masters interns, PhD candidates, and Post-Doctoral researchers. To apply, send me an email with your CV and a short research statement. mailing address: INRIA, 23 avenue d'Italie, Paris 75013, France