miTLS is a verified reference implementation of the TLS protocol. Our code fully supports its wire formats, ciphersuites, sessions and connections, re-handshakes and resumptions, alerts and errors, and data fragmentation, as prescribed in the RFCs; it interoperates with mainstream web browsers and servers. At the same time, our code is carefully structured to enable its modular, automated verification, from its main API down to computational assumptions on its cryptographic algorithms.

The stable version of miTLS including the new 0.9 release are written in F# and specified in F7. We present security specifications for its main components, such as authenticated stream encryption for the record layer and key establishment for the handshake. We describe their verification using the F7 refinement typechecker. To this end, we equip each cryptographic primitive and construction of TLS with a new typed interface that captures its security properties, and we gradually replace concrete implementations with ideal functionalities. We finally typecheck the protocol state machine, and thus obtain precise security theorems for TLS, as it is implemented and deployed. We also revisit classic attacks and report a few new ones.

See miTLS in action!

The development version is written and verified in F*, a ML-like functional programming language aimed at program verification.


TLS is possibly the most used secure communications protocol, with a long history of flaws and fixes, ranging from its protocol logic to its cryptographic design, and from the Internet standard to its diverse implementations.

Microsoft, Inria, and the Joint Centre

This work is the result of the long-term collaboration between Microsoft Research and Inria, the two partners in the Joint Centre.


18 Nov 2015 to 19 Nov 2015

miTLS and flexTLS github release. Presented at Paris Open Source Summit. Visit us on github.

5 August 2015

Awarded pwnie in Las Vegas at the BlackHat USA security conference. See the publications page.

18-20 May 2015

A Messy State of the Union: Taming the Composite State Machines of TLS won Distinguished Paper Award at IEEE Symposium on Security and Privacy. See the publications page.

3 October 2014

miTLS 0.8.1 released. See the download page.

20 August 2014

miTLS 0.7.0 released. See the download page.

4 March 2014

Announcement of the triple handshake attack.

21 November 2013

miTLS 0.1.3 released. See the download page.

19 March 2013

miTLS 0.1.2 released. See the download page.

5 March 2013

Our paper on TLS security has been accepted at the IEEE Symposium on Security & Privacy. A draft technical report of this work is available from the download page.

11 February 2013

miTLS 0.1.1 released. See the download page.