SpringerLink
Log in

Key-Schedule Security for the TLS 1.3 Standard

  • Conference paper
  • First Online:
Advances in Cryptology – ASIACRYPT 2022 (ASIACRYPT 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13791))

Abstract

Transport Layer Security (TLS) is the cryptographic backbone of secure communication on the Internet. In its latest version 1.3, the standardization process has taken formal analysis into account both due to the importance of the protocol and the experience with conceptual attacks against previous versions. To manage the complexity of TLS (the specification exceeds 100 pages), prior reduction-based analyses have focused on some protocol features and omitted others, e.g., included session resumption and omitted agile algorithms or vice versa.

This article is a major step towards analysing the TLS 1.3 key establishment protocol as specified at the end of its rigorous standardization process. Namely, we provide a full proof of the TLS key schedule, a core protocol component which produces output keys and internal keys of the key exchange protocol. In particular, our model supports all key derivations featured in the standard, including its negotiated modes and algorithms that combine an optional Diffie-Hellman exchange for forward secrecy with optional pre-shared keys supplied by the application or recursively established in prior sessions.

Technically, we rely on state-separating proofs (Asiacrypt ’18) and introduce techniques to model large and complex derivation graphs. Our key schedule analysis techniques have been used subsequently to analyse the key schedule of Draft 11 of the MLS protocol (S &P ’22) and to propose improvements.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 96.29
Price includes VAT (Germany)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 128.39
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    These two oracles in particular are necessary for composition: Note that the main oracles the adversary interacts with are subscripted by a name n and a level \(\ell \) while the \(\textsf{Q}\) and \(\textsf{UNQ}\) oracles only take the name n as subscript. We will share the same \(\textsf{Q}\) and \(\textsf{UNQ}\) oracles between many instances of \(\texttt{Gxpd}^b_{ n ,\ell }\) and therefore need to allow reductions access to these oracles.

References

  1. Abdalla, M., Bellare, M., Rogaway, P.: The oracle diffie-hellman assumptions and an analysis of DHIES. In: Naccache, D. (ed.) CT-RSA 2001. LNCS, vol. 2020, pp. 143–158. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45353-9_12

    Chapter  Google Scholar 

  2. Adrian, D., et al.: Imperfect forward secrecy: how Diffie-Hellman fails in practice. In: ACM CCS 2015, pp. 5–17. ACM Press (2015). https://doi.org/10.1145/2810103.2813707

  3. AlFardan, N.J., Paterson, K.G.: Lucky thirteen: breaking the TLS and DTLS record protocols. In: 2013 S &P, pp. 526–540. IEEE (2013). https://doi.org/10.1109/SP.2013.42

  4. Arfaoui, G., Bultel, X., Fouque, P.A., Nedelcu, A., Onete, C.: The privacy of the TLS 1.3 protocol. PoPETs 2019(4), 190–210 (2019). https://doi.org/10.2478/popets-2019-0065

  5. Aviram, N., et al.: DROWN: breaking TLS using SSLv2. In: USENIX Security 2016, pp. 689–706. USENIX (2016)

    Google Scholar 

  6. Badertscher, C., Matt, C., Maurer, U., Rogaway, P., Tackmann, B.: Augmented secure channels and the goal of the TLS 1.3 record layer. In: Au, M.-H., Miyaji, A. (eds.) ProvSec 2015. LNCS, vol. 9451, pp. 85–104. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26059-4_5

    Chapter  Google Scholar 

  7. Bellare, M.: New proofs for NMAC and HMAC: security without collision resistance. J. Cryptol. 28(4), 844–878 (2014). https://doi.org/10.1007/s00145-014-9185-x

    Article  MATH  Google Scholar 

  8. 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). https://doi.org/10.1007/3-540-48329-2_21

    Chapter  Google Scholar 

  9. Beurdouche, B., et al.: A messy state of the union: taming the composite state machines of TLS. In: 2015 S &P, pp. 535–552. IEEE (2015). https://doi.org/10.1109/SP.2015.39

  10. Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: 2017 S &P, pp. 483–502. IEEE (2017). https://doi.org/10.1109/SP.2017.26

  11. Bhargavan, K., Brzuska, C., Fournet, C., Green, M., Kohlweiss, M., Zanella-Béguelin, S.: Downgrade resilience in key-exchange protocols. In: 2016 S &P, pp. 506–525. IEEE (2016). https://doi.org/10.1109/SP.2016.37

  12. Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Pironti, A., Strub, P.Y.: Triple handshakes and cookie cutters: Breaking and fixing authentication over tls. In: IEEE Symposium on Security & Privacy (Oakland) (2014). pubs/triple-handshakes-and-cookie-cutters-sp14.pdf

    Google Scholar 

  13. Bhargavan, K., Delignat-Lavaud, A., Pironti, A.: Verified contributive channel bindings for compound authentication. In: NDSS 2015. ISOC (2015)

    Google Scholar 

  14. Bhargavan, K., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.-Y., Zanella-Béguelin, S.: Proving the TLS handshake secure (as it is). In: Garay, J.A., Gennaro, R. (eds.) CRYPTO 2014. LNCS, vol. 8617, pp. 235–255. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44381-1_14

    Chapter  Google Scholar 

  15. Bhargavan, K., Leurent, G.: Transcript collision attacks: breaking authentication in TLS, IKE and SSH. In: NDSS 2016. ISOC (2016)

    Google Scholar 

  16. Blanchet, B.: CryptoVerif: computationally sound mechanized prover for cryptographic protocols. In: Formal Protocol Verification, vol. 117, p. 156 (2007)

    Google Scholar 

  17. Blanchet, B.: Composition theorems for CryptoVerif and application to TLS 1.3. In: CSF, pp. 16–30 (2018). https://doi.org/10.1109/CSF.2018.00009

  18. Blanchet, B., Smyth, B., Cheval, V., Sylvestre, M.: ProVerif 2.00: automatic cryptographic protocol verifier. User Manual (2018)

    Google Scholar 

  19. Böck, H., Somorovsky, J., Young, C.: Return of bleichenbacher’s oracle threat (ROBOT). In: USENIX Security 2018, pp. 817–849. USENIX (2018)

    Google Scholar 

  20. Brendel, J., Fischlin, M., Günther, F., Janson, C.: PRF-ODH: relations, instantiations, and impossibility results. In: Katz, J., Shacham, H. (eds.) CRYPTO 2017. LNCS, vol. 10403, pp. 651–681. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63697-9_22

    Chapter  Google Scholar 

  21. Bricout, R., Murphy, S., Paterson, K.G., van der Merwe, T.: Analysing and exploiting the mantin biases in RC4. Cryptology ePrint Archive, Report 2016/063 (2016). http://eprint.iacr.org/2016/063

  22. Brzuska, C., Cornelissen, E., Kohbrok, K.: Security analysis of the mls key derivation. In: 2022 IEEE Symposium on Security and Privacy, pp. 595–613. IEEE Computer Society, Los Alamitos (2022). https://doi.org/10.1109/SP46214.2022.00035

  23. Brzuska, C., Delignat-Lavaud, A., Egger, C., Fournet, C., Kohbrok, K., Kohlweiss, M.: Key-schedule security for the TLS 1.3 standard. Cryptology ePrint Archive, Report 2021/467 (2021). https://eprint.iacr.org/2021/467

  24. Brzuska, C., Delignat-Lavaud, A., Fournet, C., Kohbrok, K., Kohlweiss, M.: State separation for code-based game-playing proofs. In: ASIACRYPT 2018, Part III. LNCS, vol. 11274, pp. 222–249. Springer, Heidelberg (Dec 2018). https://doi.org/10.1007/978-3-030-03332-3_9

  25. Brzuska, C., Egger, C.: Key exchange to key schedule reduction for TLS 1.3 (2022). preprint

    Google Scholar 

  26. Canetti, R., Krawczyk, H.: Universally composable notions of key exchange and secure channels. In: Knudsen, L.R. (ed.) EUROCRYPT 2002. LNCS, vol. 2332, pp. 337–351. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46035-7_22

    Chapter  Google Scholar 

  27. Chen, S., Jero, S., Jagielski, M., Boldyreva, A., Nita-Rotaru, C.: Secure communication channel establishment: TLS 1.3 (over TCP Fast Open) vs. QUIC. In: Sako, K., Schneider, S., Ryan, P.Y.A. (eds.) ESORICS 2019. LNCS, vol. 11735, pp. 404–426. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29959-0_20

    Chapter  Google Scholar 

  28. Cornelissen, E.: Pull request 453: Use the GroupContext to derive the joiner_secret. https://github.com/mlswg/mls-protocol/pull/453

  29. Cremers, C., Horvat, M., Hoyland, J., Scott, S., van der Merwe, T.: A comprehensive symbolic analysis of TLS 1.3. In: ACM CCS 2017, pp. 1773–1788. ACM Press (2017)

    Google Scholar 

  30. Cremers, C., Horvat, M., Scott, S., van der Merwe, T.: Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication. In: 2016 S &P, pp. 470–485. IEEE (2016). https://doi.org/10.1109/SP.2016.35

  31. Davis, H., Günther, F.: Tighter proofs for the SIGMA and TLS 1.3 key exchange protocols. In: Sako, K., Tippenhauer, N.O. (eds.) ACNS 2021. LNCS, vol. 12727, pp. 448–479. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-78375-4_18

    Chapter  MATH  Google Scholar 

  32. Delignat-Lavaud, A., et al.: Implementing and proving the TLS 1.3 record layer. In: IEEE Security & Privacy. IEEE (2017)

    Google Scholar 

  33. Diemert, D., Jager, T.: On the tight security of TLS 1.3: theoretically sound cryptographic parameters for real-world deployments. J. Cryptol. 34(3), 1–57 (2021). https://doi.org/10.1007/s00145-021-09388-x

    Article  MATH  Google Scholar 

  34. Dowling, B., Fischlin, M., Günther, F., Stebila, D.: A cryptographic analysis of the TLS 1.3 handshake protocol candidates. In: ACM CCS 2015, pp. 1197–1210. ACM Press (2015). https://doi.org/10.1145/2810103.2813653

  35. Dowling, B., Fischlin, M., Günther, F., Stebila, D.: A cryptographic analysis of the TLS 1.3 draft-10 full and pre-shared key handshake protocol. Cryptology ePrint Archive, Report 2016/081 (2016). http://eprint.iacr.org/2016/081

  36. Dowling, B., Fischlin, M., Günther, F., Stebila, D.: A cryptographic analysis of the TLS 1.3 handshake protocol. J. Cryptol. 34(4), 1–69 (2021). https://doi.org/10.1007/s00145-021-09384-1

    Article  MATH  Google Scholar 

  37. Drucker, N., Gueron, S.: Selfie: reflections on TLS 1.3 with PSK. J. Cryptol. 34(3), 1–18 (2021). https://doi.org/10.1007/s00145-021-09387-y

    Article  Google Scholar 

  38. Duong, T., Rizzo, J.: Here come the \(\oplus \) ninjas (2011). http://nerdoholic.org/uploads/dergln/beast_part2/ssl_jun21.pdf

  39. Fischlin, M., Günther, F.: Replay attacks on zero round-trip time: the case of the TLS 1.3 handshake candidates. In: 2017 IEEE European Symposium on Security and Privacy (EuroS &P), pp. 60–75. IEEE (2017)

    Google Scholar 

  40. Fischlin, M., Günther, F., Marson, G.A., Paterson, K.G.: Data is a stream: security of stream-based channels. In: Gennaro, R., Robshaw, M. (eds.) CRYPTO 2015. LNCS, vol. 9216, pp. 545–564. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48000-7_27

    Chapter  Google Scholar 

  41. Fischlin, M., Günther, F., Schmidt, B., Warinschi, B.: Key confirmation in key exchange: a formal treatment and implications for TLS 1.3. In: 2016 S &P, pp. 452–469. IEEE (2016). https://doi.org/10.1109/SP.2016.34

  42. Iyengar, J., Thomson, M.: QUIC. IETF draft (2019)

    Google Scholar 

  43. Jager, T., Kohlar, F., Schäge, S., Schwenk, J.: Authenticated confidential channel establishment and the security of TLS-DHE. J. Cryptol. 30(4), 1276–1324 (2017). https://doi.org/10.1007/s00145-016-9248-2

    Article  MATH  Google Scholar 

  44. Krawczyk, H.: SIGMA: the “SIGn-and-MAc’’ approach to authenticated diffie-hellman and its use in the IKE protocols. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 400–425. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45146-4_24

    Chapter  Google Scholar 

  45. Krawczyk, H.: Cryptographic extraction and key derivation: the HKDF scheme. In: Rabin, T. (ed.) CRYPTO 2010. LNCS, vol. 6223, pp. 631–648. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14623-7_34

    Chapter  Google Scholar 

  46. Krawczyk, H.: A unilateral-to-mutual authentication compiler for key exchange (with applications to client authentication in TLS 1.3). In: ACM CCS 2016, pp. 1438–1450. ACM Press (2016). https://doi.org/10.1145/2976749.2978325

  47. Krawczyk, H., Wee, H.: The OPTLS protocol and TLS 1.3. Cryptology ePrint Archive, Report 2015/978 (2015). http://eprint.iacr.org/2015/978

  48. Li, X., Xu, J., Zhang, Z., Feng, D., Hu, H.: Multiple handshakes security of TLS 1.3 candidates. In: 2016 S &P, pp. 486–505. IEEE (2016). https://doi.org/10.1109/SP.2016.36

  49. Mavrogiannopoulos, N., Vercauteren, F., Velichkov, V., Preneel, B.: A cross-protocol attack on the TLS protocol. In: ACM CCS 2012, pp. 62–72. ACM Press (2012). https://doi.org/10.1145/2382196.2382206

  50. Möller, B., Duong, T., Kotowicz, K.: This poodle bites: exploiting the SSL 3.0 fallback (2014). https://www.openssl.org/~bodo/ssl-poodle.pdf

  51. Paterson, K.G., van der Merwe, T.: Reactive and proactive standardisation of TLS. In: Security Standardisation Research, pp. 160–186 (2016)

    Google Scholar 

  52. Patton, C., Shrimpton, T.: Partially specified channels: the TLS 1.3 record layer without elision. Cryptology ePrint Archive, Report 2018/634 (2018)

    Google Scholar 

  53. Rescorla, E.: The Transport Layer Security (TLS) Protocol Version 1.3 (2018). https://tools.ietf.org/html/rfc8446

Download references

Author information

Authors and Affiliations

  1. Aalto University, Espoo, Finland

    Chris Brzuska & Konrad Kohbrok

  2. Microsoft Research Cambridge, Cambridge, UK

    Antoine Delignat-Lavaud & Cédric Fournet

  3. IRIF, Université Paris Cité, Paris, France

    Christoph Egger

  4. University of Edinburgh, Edinburgh, UK

    Markulf Kohlweiss

Authors
  1. Chris Brzuska
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Antoine Delignat-Lavaud
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christoph Egger
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Cédric Fournet
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Konrad Kohbrok
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Markulf Kohlweiss
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Chris Brzuska .

Editor information

Editors and Affiliations

  1. Indian Institute of Technology Madras, Chennai, India

    Shweta Agrawal

  2. Chinese Academy of Sciences, Bei**g, China

    Dongdai Lin

Rights and permissions

Reprints and permissions

Copyright information

© 2022 International Association for Cryptologic Research

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Brzuska, C., Delignat-Lavaud, A., Egger, C., Fournet, C., Kohbrok, K., Kohlweiss, M. (2022). Key-Schedule Security for the TLS 1.3 Standard. In: Agrawal, S., Lin, D. (eds) Advances in Cryptology – ASIACRYPT 2022. ASIACRYPT 2022. Lecture Notes in Computer Science, vol 13791. Springer, Cham. https://doi.org/10.1007/978-3-031-22963-3_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-22963-3_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-22962-6

  • Online ISBN: 978-3-031-22963-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation