Séminaire SoSySec

Sécurité des logiciels et des systèmes

Accueil     Présentation     Archives

Antoine Delignat-Lavaud (Microsoft Research Cambridge)

A Verified Implementation and Security Proof of the TLS 1.3 Record Layer

The new 1.3 revision of the Transport Layer Security protocol used to encrypt most traffic on the Internet is built on top of an updated modular AEAD construction (replacing dangerous modes such as MAC-pad-encrypt) that differs from previous TLS versions in its use of padding, associated data and nonces. It encrypts the content-type used to multiplex between sub-protocols such as Handshake, Alert and Application Data. New protocol features such as early application data (0-RTT and 0.5-RTT) and late handshake messages require additional keys and a more general model of stateful encryption.

We prove the cryptographic security of the TLS 1.3 record layer based on a security-verified implementation written in F*, which enables us to write code-based game-playing proofs, following the well-established approach of Bellare and Rogaway, applied directly to the F* implementation rather than to hand-written pseudo-code. More precisely, we reduce the security of the record layer to the security of the underlying block cipher, modelled as a PRF, and the parameters of the field used for the Wegman-Carter-Shoup MAC construction; we also provide concrete security bounds for cipher suites such as AES-GCM and ChaCha20-Poly1305. Most of the perfect reduction steps are verified by typing on the reference implementation, while some steps that incur a security loss must be justified on paper. The resulting secure implementation is useable as part of our verified TLS 1.3 library and can interoperate with experimental versions of Chrome and Firefox with TLS 1.3 support.