International Cryptology Conference

CRYPTO 2014: Advances in Cryptology – CRYPTO 2014 pp 235-255 | Cite as

Proving the TLS Handshake Secure (As It Is)

  • Karthikeyan Bhargavan
  • Cédric Fournet
  • Markulf Kohlweiss
  • Alfredo Pironti
  • Pierre-Yves Strub
  • Santiago Zanella-Béguelin
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8617)

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.

References

  1. 1.
    Acar, T., Belenkiy, M., Bellare, M., Cash, D.: Cryptographic agility and its reation to circular encryption. In: Gilbert, H. (ed.) EUROCRYPT 2010. LNCS, vol. 6110, pp. 403–422. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  2. 2.
    Barthe, G., Grégoire, B., Heraud, S., Zanella-Béguelin, S.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71–90. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  3. 3.
    Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol. 773, pp. 232–249. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  4. 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. 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
  6. 6.
    Bleichenbacher, D.: Chosen ciphertext attacks against protocols based on RSA encryption standard PKCS #1. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol. 1462, pp. 1–12. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  7. 7.
    Canetti, R., Krawczyk, H., Nielsen, J.B.: Relaxing chosen-ciphertext security. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 565–582. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Cramer, R., Shoup, V.: Design and analysis of practical public-key encryption schemes secure against adaptive chosen ciphertext attack. SIAM J. Computing 33(1), 167–226 (2003)MathSciNetCrossRefMATHGoogle Scholar
  9. 9.
    Dierks, T., Rescorla, E.: The Transport Layer Security (TLS) Protocol Version 1.2 (2008)Google Scholar
  10. 10.
    Fournet, C., Kohlweiss, M., Strub, P.-Y.: Modular code-based cryptographic verification. In: ACM CCS 2011 (2011)Google Scholar
  11. 11.
    Giesen, F., Kohlar, F., Stebila, D.: On the security of TLS renegotiation. In: ACM CCS 2013 (2013)Google Scholar
  12. 12.
    Haber, S., Pinkas, B.: Securely combining public-key cryptosystems. In: ACM CCS 2001 (2001)Google Scholar
  13. 13.
    Jager, T., Kohlar, F., Schäge, S., Schwenk, J.: On the security of TLS-DHE in the standard model. In: Safavi-Naini, R., Canetti, R. (eds.) CRYPTO 2012. LNCS, vol. 7417, pp. 273–293. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  14. 14.
    Jonsson, J., Kaliski Jr., B.S.: On the security of RSA encryption in TLS. In: Yung, M. (ed.) CRYPTO 2002. LNCS, vol. 2442, pp. 127–142. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  15. 15.
    Klíma, V., Pokorný, O., Rosa, T.: Attacking RSA-based sessions in SSL/TLS. In: Walter, C.D., Koç, Ç.K., Paar, C. (eds.) CHES 2003. LNCS, vol. 2779, pp. 426–440. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  16. 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
  17. 17.
    Krawczyk, H., Paterson, K.G., Wee, H.: On the security of the TLS protocol: A systematic analysis. In: Canetti, R., Garay, J.A. (eds.) CRYPTO 2013, Part I. LNCS, vol. 8042, pp. 429–448. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  18. 18.
    Langley, A.: Unfortunate current practices for HTTP over TLS (2011), http://www.ietf.org/mail-archive/web/tls/current/msg07281.html
  19. 19.
    Modadugu, N., Langley, A., Moeller, B.: Transport Layer Security (TLS) False Start. Internet Draft (2010)Google Scholar
  20. 20.
    Mavrogiannopoulos, N., Vercauteren, F., Velichkov, V., Preneel, B.: A cross-protocol attack on the TLS protocol. In: ACM CCS 2012 (2012)Google Scholar
  21. 21.
    Morrissey, P., Smart, N.P., Warinschi, B.: A modular security analysis of the TLS handshake protocol. In: Pieprzyk, J. (ed.) ASIACRYPT 2008. LNCS, vol. 5350, pp. 55–73. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  22. 22.
    Naccache, D., Shparlinski, I.E.: Divisibility, Smoothness and Cryptographic Applications. ArXiv e-prints (October 2008)Google Scholar
  23. 23.
    Paterson, K.G., Ristenpart, T., Shrimpton, T.: Tag size does matter: Attacks and proofs for the TLS record protocol. In: Lee, D.H., Wang, X. (eds.) ASIACRYPT 2011. LNCS, vol. 7073, pp. 372–389. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  24. 24.
    Qualys SSL labs. SSL server test, https://www.ssllabs.com/ssltest/analyze.html
  25. 25.
    Ray, M.: Authentication gap in TLS renegotiation (2009), http://extendedsubset.com/Renegotiating_TLS.pdf
  26. 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. 27.
    Wagner, D., Schneier, B.: Analysis of the SSL 3.0 protocol. In: 2nd USENIX Workshop on Electronic Commerce, WOEC 1996 (1996)Google Scholar

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