Abstract

Joint work with Karthik Bhargavan, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub

We develop a reference implementation of the TLS 1 .2 Internet Standard. Our code fully supports binary wire formats, multiple ciphersuites, sessions and connections with re-handshakes and resumptions, alerts, message fragmentation, ... as prescribed by the standard; it interoperates with other implementations, notably existing web browsers and servers. At the same time, our code is carefully structured to enable its automated, modular verification, from its main API down to computational security assumptions on its underlying cryptographic algorithms.

In the talk, I will review our modular cryptographic verification method, which is based on F7, a refinement type checker coupled with an SMT -solver, with a theory formalized in Coq. Using F7, we verify constructions and protocols coded in F# by typing them against new cryptographic interfaces that capture their authenticity and secrecy properties. We relate their ideal functionalities and concrete implementations, using game-based program transformations behind typed interfaces, so that we can easily compose them.

I will also outline our TLS implementations, coded in F# and specified in F7. I will present its main typed interfaces, which can be read as specifications of “giant” ideal functionalities for its main components, such as authenticated encryption for the record layer and key establishment for the handshake. I will finally describe our main security results, as well as some new attacks we found in the process.