@inproceedings{delignat-lavaud2016towards,
author = {Delignat-Lavaud, Antoine and Fournet, Cédric and Kohlweiss, Markulf and Protzenko, Jonathan and Swamy, Nikhil and Zanella-Béguelin, Santiago},
title = {Towards a Provably Secure Implementation of TLS 1.3},
booktitle = {TRON Workshop},
year = {2016},
month = {July},
abstract = {We report ongoing work towards a verified reference
implementation of TLS 1.3 in the F* programming language. Our
code supports selected ciphersuites for all versions of TLS from
1.0 to 1.3. It is being developed on http://github.com/mitls as the
next version of MITLS, written in F? instead of F#. We intend to
prove a strong, joint cryptographic security theorem for TLS 1.3
clients and servers, even when they run alongside older versions
of the protocol with weaker security. Our verification approach
adapts and extends that of MITLS in several ways: (1) we adopt
an idiomatic stateful style that promises higher performance than
the pure functional style of MITLS; (2) we seek to prove stronger
security properties with fewer ad hoc assumptions; (3) we rely on
advanced F? type inference to substantially reduce both the code
base and the typed proof annotations. This paper describes our
implementation architecture, our new composite state machine
for TLS 1.0–1.3, and our target security theorem. By the time of
the TRON workshop, we will present concrete verification results
for our implementation. As far as we are aware, these will be
the first cryptographic proofs for an implementation of TLS 1.3,
and a fortiori for an implementation that is backward compatible
with older versions of the protocol. We anticipate that our effort
will identify early problems and offer implementation guidelines
for other TLS libraries.},
url = {http://approjects.co.za/?big=en-us/research/publication/towards-provably-secure-implementation-tls-1-3/},
edition = {TRON Workshop},
}