We systematically study the provable security of the TLS handshake, as it is implemented and deployed. To capture the details of the standard and its main extensions, we rely on miTLS, a verified reference implementation of the protocol. miTLS inter-operates with mainstream browsers and servers for many protocol versions, configurations, and ciphersuites; and it provides application-level, provable security for some.
We propose new agile security definitions and assumptions for the signatures, key encapsulation mechanisms, and key derivation algorithms used by the TLS handshake. By necessity, our definitions are stronger than those expected with simple modern protocols.
To validate our model of key encapsulation, we prove that RSA ciphersuites satisfy the security assumption needed for our proof of the handshake. Specifically, we formalize the use of PKCS#1v1.5 encryption in TLS, including recommended countermeasures against Bleichenbacher attacks, and build a 3,000-line EasyCrypt proof of its security against replayable chosen-ciphertext attacks under the assumption that ciphertexts are hard to re-randomize.
Based on our new agile definitions, we construct a modular proof of security for the miTLS reference implementation of the handshake, including ciphersuite negotiation, key exchange, renegotiation, and resumption, treated as a detailed 3,600-line executable model.
We present our main definitions, constructions, and proofs for an abstract model of the protocol, featuring series of related runs of the handshake with different ciphersuites. We also describe its refinement to account for the whole reference implementation, based on automated verification tools.Category / Keywords: cryptographic protocols / TLS protocol, handshake, key exchange, cryptographic agility, provable Date: received 7 Mar 2014, last revised 7 Mar 2014 Contact author: markulf at microsoft com Available format(s): PDF | BibTeX Citation Version: 20140309:201546 (All versions of this report) Discussion forum: Show discussion | Start new discussion