International Cryptology Conference

CRYPTO 2014: Advances in Cryptology – CRYPTO 2014 pp 235-255

Proving the TLS Handshake Secure (As It Is)

  • Karthikeyan Bhargavan
  • Cédric Fournet
  • Markulf Kohlweiss
  • Alfredo Pironti
  • Pierre-Yves Strub
  • Santiago Zanella-Béguelin
Conference paper

DOI: 10.1007/978-3-662-44381-1_14

Part of the Lecture Notes in Computer Science book series (LNCS, volume 8617)
Cite this paper as:
Bhargavan K., Fournet C., Kohlweiss M., Pironti A., Strub PY., Zanella-Béguelin S. (2014) Proving the TLS Handshake Secure (As It Is). In: Garay J.A., Gennaro R. (eds) Advances in Cryptology – CRYPTO 2014. CRYPTO 2014. Lecture Notes in Computer Science, vol 8617. Springer, Berlin, Heidelberg

Abstract

The TLS Internet Standard features a mixed bag of cryptographic algorithms and constructions, letting clients and servers negotiate their use for each run of the handshake. Although many ciphersuites are now well-understood in isolation, their composition remains problematic, and yet it is critical to obtain practical security guarantees for TLS, as all mainstream implementations support multiple related runs of the handshake and share keys between algorithms.

We 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. We propose new agile security definitions and assumptions for the signatures, key encapsulation mechanisms (KEM), and key derivation algorithms used by the TLS handshake. To validate our model of key encapsulation, we prove that both RSA and Diffie-Hellman ciphersuites satisfy our definition for the KEM. In particular, we formalize the use of PKCS#1v1.5 and build a 3,000-line EasyCrypt proof of the security of the resulting KEM 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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© International Association for Cryptologic Research 2014

Authors and Affiliations

  • Karthikeyan Bhargavan
    • 1
  • Cédric Fournet
    • 2
  • Markulf Kohlweiss
    • 2
  • Alfredo Pironti
    • 1
  • Pierre-Yves Strub
    • 3
  • Santiago Zanella-Béguelin
    • 1
    • 2
  1. 1.INRIAParisFrance
  2. 2.Microsoft ResearchCambridgeUK
  3. 3.IMDEA Software InstituteMadridSpain

Personalised recommendations