"I love miTLS, Triple Handshake, SMACK, FREAK, Logjam, and SLOTH"

2022-06-12 18:12:51

miTLS Publications Attacks Code FlexTLS People miTLS: A Verified Reference Implementation of TLSmiTLS is a verified reference implementation ofthe TLSprotocol. Our code fully supports its wire formats, ciphersuites,sessions and connections, re-handshakes and resumptions, alerts anderrors, and data fragmentation, as prescribed in the RFCs; itinteroperates with mainstream web browsers and servers. At the sametime, our code is carefully structured to enable its modular,automated verification, from its main API down to computationalassumptions on its cryptographic algorithms.The stable version of miTLS including the new 0.9 release arewritten in F# andspecified inF7. We present security specifications for its main components,such as authenticated stream encryption for the record layer and keyestablishment for the handshake. We describe their verification usingthe F7 refinement typechecker. To this end, we equip eachcryptographic primitive and construction of TLS with a new typedinterface that captures its security properties, and we graduallyreplace concrete implementations with ideal functionalities. Wefinally typecheck the protocol state machine, and thus obtain precisesecurity theorems for TLS, as it is implemented and deployed. We alsorevisit classic attacks and report a few new ones.The development version is written and verifiedin F*, aML-like functional programming language aimed at programverification. You can learn more about F* on itsproject homepage.The TLS ProtocolTLS is possibly the most used secure communications protocol, with a long history of flaws and fixes, ranging from its protocol logic toits cryptographic design, and from the Internet standard to itsdiverse implementations.Microsoft, Inria, and the Joint CentreThis work is the result of the long-term collaboration between Microsoft Research and Inria, the two partners in the Microsoft-Inria Joint Centre.