Proving the TLS Handshake Secure (As It Is)
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.
Unable to display preview. Download preview PDF.
- 4.Bhargavan, K., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.-Y.: Implementing TLS with verified cryptograhic security. In: IEEE Symposium on Security and Privacy (2013)Google Scholar
- 5.Bhargavan, K., Delignat-Lavaut, A., Fournet, C., Pironti, A., Strub, P.-Y.: Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS. In: IEEE Symposium on Security and Privacy (2014)Google Scholar
- 9.Dierks, T., Rescorla, E.: The Transport Layer Security (TLS) Protocol Version 1.2 (2008)Google Scholar
- 10.Fournet, C., Kohlweiss, M., Strub, P.-Y.: Modular code-based cryptographic verification. In: ACM CCS 2011 (2011)Google Scholar
- 11.Giesen, F., Kohlar, F., Stebila, D.: On the security of TLS renegotiation. In: ACM CCS 2013 (2013)Google Scholar
- 12.Haber, S., Pinkas, B.: Securely combining public-key cryptosystems. In: ACM CCS 2001 (2001)Google Scholar
- 16.Kohlar, F., Schäge, S., Schwenk, J.: On the security of TLS-DH and TLS-RSA in the standard model. Cryptology ePrint Archive, Report 2013/367 (2013)Google Scholar
- 18.Langley, A.: Unfortunate current practices for HTTP over TLS (2011), http://www.ietf.org/mail-archive/web/tls/current/msg07281.html
- 19.Modadugu, N., Langley, A., Moeller, B.: Transport Layer Security (TLS) False Start. Internet Draft (2010)Google Scholar
- 20.Mavrogiannopoulos, N., Vercauteren, F., Velichkov, V., Preneel, B.: A cross-protocol attack on the TLS protocol. In: ACM CCS 2012 (2012)Google Scholar
- 22.Naccache, D., Shparlinski, I.E.: Divisibility, Smoothness and Cryptographic Applications. ArXiv e-prints (October 2008)Google Scholar
- 24.Qualys SSL labs. SSL server test, https://www.ssllabs.com/ssltest/analyze.html
- 25.Ray, M.: Authentication gap in TLS renegotiation (2009), http://extendedsubset.com/Renegotiating_TLS.pdf
- 26.Stevens, M., Sotirov, A., Appelbaum, J., Lenstra, A., Molnar, D., Osvik, D.A., de Weger, B.: Short chosen-prefix collisions for MD5 and the creation of a rogue CA certificate. Cryptology ePrint Archive, Report 2009/111 (2009)Google Scholar
- 27.Wagner, D., Schneier, B.: Analysis of the SSL 3.0 protocol. In: 2nd USENIX Workshop on Electronic Commerce, WOEC 1996 (1996)Google Scholar