research-article

Public Access

A Comprehensive Symbolic Analysis of TLS 1.3

Authors:

Jonathan Hoyland,

Thyla van der MerweAuthors Info & Claims

CCS '17: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security

October 2017

Pages 1773 - 1788

https://doi.org/10.1145/3133956.3134063

Published: 30 October 2017 Publication History

Abstract

The TLS protocol is intended to enable secure end-to-end communication over insecure networks, including the Internet. Unfortunately, this goal has been thwarted a number of times throughout the protocol's tumultuous lifetime, resulting in the need for a new version of the protocol, namely TLS 1.3. Over the past three years, in an unprecedented joint design effort with the academic community, the TLS Working Group has been working tirelessly to enhance the security of TLS.

We further this effort by constructing the most comprehensive, faithful, and modular symbolic model of the TLS~1.3 draft 21 release candidate, and use the TAMARIN prover to verify the claimed TLS~1.3 security requirements, as laid out in draft 21 of the specification. In particular, our model covers all handshake modes of TLS 1.3.

Our analysis reveals an unexpected behaviour, which we expect will inhibit strong authentication guarantees in some implementations of the protocol. In contrast to previous models, we provide a novel way of making the relation between the TLS specification and our model explicit: we provide a fully annotated version of the specification that clarifies what protocol elements we modelled, and precisely how we modelled these elements. We anticipate this model artifact to be of great benefit to the academic community and the TLS Working Group alike.

References

[1]

David Adrian, Karthikeyan Bhargavan, Zakir Durumeric, Pierrick Gaudry, Matthew Green, J. Alex Halderman, Nadia Heninger, Drew Springall, Emmanuel Thomé, Luke Valenta, Benjamin VanderSloot, Eric Wustrow, Santiago Zanella-Béguelin, and Paul Zimmermann 2015. Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice. (2015), pages 13 pages. https://doi.org/10.1145/2810103.2813707

Digital Library

[2]

Nadhem J. AlFardan and Kenneth G. Paterson 2012. Plaintext-Recovery Attacks Against Datagram TLS 19th Annual Network and Distributed System Security Symposium, NDSS 2012, San Diego, California, USA, February 5-8, 2012. http://www.internetsociety.org/plain-text-recovery-attacks-against-datagram-tls

[3]

Nadhem J. AlFardan and Kenneth G. Paterson 2013. Lucky Thirteen: Breaking the TLS and DTLS Record Protocols 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19--22, 2013. 526--540. http://dx.doi.org/10.1109/SP.2013.42

Digital Library

[4]

Kenichi Arai and Shin'ichiro Matsuo 2016. Formal Verification of TLS 1.3 Full Handshake Protocol Using ProVerif. TLS mailing list post. (February 2016). https://www.ietf.org/mail-archive/web/tls/current/msg19339.html

[5]

Nimrod Aviram, Sebastian Schinzel, Juraj Somorovsky, Nadia Heninger, Maik Dankel, Jens Steube, Luke Valenta, David Adrian, J. Alex Halderman, Viktor Dukhovni, Emilia Käsper, Shaanan Cohney, Susanne Engels, Christof Paar, and Yuval Shavitt 2016. DROWN: Breaking TLS with SSLv2. In 5th USENIX Security Symposium. 689--706.

[6]

Gregory V. Bard. 2004. The Vulnerability of SSL to Chosen Plaintext Attack. IACR Cryptology ePrint Archive Vol. 2004 (2004), 111. http://eprint.iacr.org/2004/111

[7]

Gregory V. Bard. 2006. A Challenging but Feasible Blockwise-Adaptive Chosen-Plaintext Attack on SSL. In SECRYPT 2006, Proceedings of the International Conference on Security and Cryptography, Setúbal, Portugal, August 7--10, 2006, SECRYPT is part of ICETE - The International Joint Conference on e-Business and Telecommunications. 99--109.

[8]

Mihir Bellare and Phillip Rogaway 1993. Entity authentication and key distribution. In Annual International Cryptology Conference. Springer, 232--249.

[9]

Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, and Jean Karim Zinzindohoue 2015. A Messy State of the Union: Taming the Composite State Machines of TLS 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015. 535--552. http://dx.doi.org/10.1109/SP.2015.39

Digital Library

[10]

Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. 2017. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. Technical Report. INRIA.

[11]

Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, and Santiago Zanella-Béguelin. 2016. Downgrade resilience in key-exchange protocols. In Security and Privacy (SP), 2016 IEEE Symposium on. IEEE, 506--525.

[12]

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, and Jean Karim Zinzindohoué. 2016. Implementing and Proving the TLS 1.3 Record Layer. Technical Report. INRIA. shownotehttp://eprint.iacr.org/2016/1178.

[13]

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, and Pierre-Yves Strub 2014. Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS 2014 IEEE Symposium on Security and Privacy, SP 2014, Berkeley, CA, USA, May 18-21, 2014. 98--113. http://dx.doi.org/10.1109/SP.2014.14

Digital Library

[14]

K. Bhargavan, N. Kobeissi, and B. Blanchet. 2016. ProScript TLS: Building a TLS 1.3 Implementation with a Verifiable Protocol Model. (2016). Presented at TRON 1.0, San Diego, CA, USA, February 21.

[15]

Karthikeyan Bhargavan and Gaëtan Leurent 2016. On the Practical (In-)Security of 64-bit Block Ciphers: Collision Attacks on HTTP over TLS and OpenVPN. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS '16). ACM, New York, NY, USA, 456--467. https://doi.org/10.1145/2976749.2978423

Digital Library

[16]

Karthikeyan Bhargavan and Gaëtan Leurent 2016. Transcript collision attacks: Breaking authentication in TLS, IKE, and SSH Network and Distributed System Security Symposium--NDSS 2016.

[17]

Bruno Blanchet, Ben Smyth, Vincent Cheval, and Marc Sylvestre 2016. Proverif 1.96: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial List of Figures. (2016). http://prosecco.gforge.inria.fr/personal/bblanche/proverif/manual.pdf

[18]

Daniel Bleichenbacher. 1998. Chosen Ciphertext Attacks Against Protocols Based on the RSA Encryption Standard PKCS #1. In Advances in Cryptology - CRYPTO '98, 18th Annual International Cryptology Conference, Santa Barbara, California, USA, August 23-27, 1998, Proceedings. 1--12. http://dx.doi.org/10.1007/BFb0055716

[19]

Ran Canetti and Hugo Krawczyk 2001. Analysis of Key-Exchange Protocols and Their Use for Building Secure Channels Advances in Cryptology - EUROCRYPT 2001, International Conference on the Theory and Application of Cryptographic Techniques, Innsbruck, Austria, May 6-10, 2001, Proceeding. 453--474. http://dx.doi.org/10.1007/3-540-44987--6_28

[20]

Brice Canvel, Alain P. Hiltgen, Serge Vaudenay, and Martin Vuagnoux 2003. Password Interception in a SSL/TLS Channel. Advances in Cryptology - CRYPTO 2003, 23rd Annual International Cryptology Conference, Santa Barbara, California, USA, August 17-21, 2003, Proceedings. 583--599. http://dx.doi.org/10.1007/978-3-540-45146-4_34

[21]

Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017. Source files and annotated RFC for TLS 1.3 analysis. (2017). https://tls13tamarin.github.io/TLS13Tamarin/.

[22]

Cas Cremers, Marko Horvat, Sam Scott, and Thyla van der Merwe 2016. Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication Security and Privacy (SP), 2016 IEEE Symposium on. IEEE, 470--485.

[23]

Danny Dolev and Andrew Yao 1983. On the security of public key protocols. IEEE Transactions on information theory Vol. 29, 2 (1983), 198--208.

Digital Library

[24]

Benjamin Dowling, Marc Fischlin, Felix Günther, and Douglas Stebila 2015. A Cryptographic Analysis of the TLS 1.3 Handshake Protocol Candidates Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, Denver, CO, USA, October 12-6, 2015. 1197--1210. http://doi.acm.org/10.1145/2810103.2813653

[25]

Benjamin Dowling, Marc Fischlin, Felix Günther, and Douglas Stebila 2016. A Cryptographic Analysis of the TLS 1.3 draft-10 Full and Pre-shared Key Handshake Protocol. Cryptology ePrint Archive, Report 2016/081. (2016). shownotehttp://eprint.iacr.org/.

[26]

Thai Duong and Juliano Rizzo 2011. Here Come the øplus Ninjas. Unpublished manuscript. (May 2011).

[27]

Thai Duong and Juliano Rizzo 2012. The CRIME Attack. Ekoparty Security Conference presentation. (2012).

[28]

Marc Fischlin, Felix Günther, Benedikt Schmidt, and Bogdan Warinschi 2016. Key Confirmation in Key Exchange: A Formal Treatment and Implications for TLS 1.3 2016 IEEE Symposium on Security and Privacy, SP 2016, San Jose, CA, USA, May 23--25, 2016.

[29]

Christina Garman, Kenneth G Paterson, and Thyla Van der Merwe 2015. Attacks Only Get Better: Password Recovery Attacks Against RC4 in TLS. USENIX Security. 113--128.

[30]

Marko Horvat. 2016. Formal Analysis of Modern Security Protocols in Current Standards. Ph.D. Dissertation. University of Oxford.

[31]

Tibor Jager, Jörg Schwenk, and Juraj Somorovsky. 2015. On the Security of TLS 1.3 and QUIC Against Weaknesses in PKCS#1 v1.5 Encryption Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, Denver, CO, USA, October 12-6, 2015. 1185--1196. http://doi.acm.org/10.1145/2810103.2813657

[32]

Vlastimil Klíma, Ondrej Pokorný, and Tomás Rosa 2003. Attacking RSA-Based Sessions in SSL/TLS. Cryptographic Hardware and Embedded Systems - CHES 2003, 5th International Workshop, Cologne, Germany, September 8-10, 2003, Proceedings. 426--440. http://dx.doi.org/10.1007/978-3-540-45238-6_33

[33]

Markulf Kohlweiss, Ueli Maurer, Cristina Onete, Björn Tackmann, and Daniele Venturi. 2014. (De-)Constructing TLS. IACR Cryptology ePrint Archive Vol. 2014 (2014), 20. http://eprint.iacr.org/2014/020

[34]

Hugo Krawczyk. 2010. Cryptographic Extraction and Key Derivation: The HKDF Scheme Advances in Cryptology - CRYPTO 2010, 30th Annual Cryptology Conference, Santa Barbara, CA, USA, August 15-19, 2010. Proceedings. 631--648. http://dx.doi.org/10.1007/978-3-642-14623-7_34

[35]

Hugo Krawczyk and Hoeteck Wee 2015. The OPTLS Protocol and TLS 1.3. IACR Cryptology ePrint Archive Vol. 2015 (2015), 978. http://eprint.iacr.org/2015/978

[36]

Brian A. LaMacchia, Kristin E. Lauter, and Anton Mityagin. 2007. Stronger Security of Authenticated Key Exchange. Provable Security, First International Conference, ProvSec 2007, Wollongong, Australia, November 1-2, 2007, Proceedings. 1--16. http://dx.doi.org/10.1007/978-3-540-75670-5_1

[37]

A. Langley and W. Chang 2013. QUIC Crypto. (June 2013). Available at https://docs.google.com/document/d/1g5nIXAIkN_Y-7XJW5K45IblHd_L2f5LTaDUDwvZ5L6g/.

[38]

Yong Li, Sven Schäge, Zheng Yang, Florian Kohlar, and Jörg Schwenk. 2014. On the Security of the Pre-shared Key Ciphersuites of TLS Public-Key Cryptography - PKC 2014 - 17th International Conference on Practice and Theory in Public-Key Cryptography, Buenos Aires, Argentina, March 26-28, 2014. Proceedings. 669--684. http://dx.doi.org/10.1007/978-3-642-54631-0_38

Digital Library

[39]

Gavin Lowe. 1997. A Hierarchy of Authentication Specifications. In Proceedings of the 10th IEEE Workshop on Computer Security Foundations (CSFW '97). IEEE Computer Society, Washington, DC, USA, 31--. http://dl.acm.org/citation.cfm?id=794197.795075

[40]

Colm MacCárthaigh. 2017. Security review of TLS1.3 0-RTT. TLS mailing list post. (May 2017). https://www.ietf.org/mail-archive/web/tls/current/msg23051. Available at https://www.ietf.org/mail-archive/web/tls/current/msg23051.html.

[41]

Itsik Mantin. 2015. Attacking SSL when using RC4. White Paper. (March 2015). https://www.imperva.com/docs/HII_Attacking_SSL_when_using_RC4.pdf

[42]

Nikos Mavrogiannopoulos, Frederik Vercauteren, Vesselin Velichkov, and Bart Preneel 2012. A cross-protocol attack on the TLS protocol. the ACM Conference on Computer and Communications Security, CCS'12, Raleigh, NC, USA, October 16-18, 2012. 62--72. http://doi.acm.org/10.1145/2382196.2382206

Digital Library

[43]

Bodo Moeller. 2004. Security of CBC Ciphersuites in SSL/TLS: Problems and Countermeasures. Unpublished manuscript. (May 2004). http://www.openssl.org/ bodo/tls-cbc.txt.

[44]

Bodo Möller, Thai Duong, and Krzysztof Kotowicz. 2014. This POODLE bites: Exploiting The SSL 3.0 Fallback. Security Advisory. (September 2014). https://www.openssl.org/ bodo/ssl-poodle.pdf

[45]

Kenneth G. Paterson and Thyla van der Merwe 2016. Reactive and Proactive Standardisation of TLS. Security Standardisation Research - Third International Conference, SSR 2016, Gaithersburg, MD, USA, December 5-6, 2016, Proceedings. 160--186.

[46]

E. Rescorla. 2015. The Transport Layer Security (TLS) Protocol Version 1.3 (draft, revision 10). (October 2015). https://tools.ietf.org/html/draft-ietf-tls-tls13--10 Available at https://tools.ietf.org/html/draft-ietf-tls-tls13-10.

[47]

Eric Rescorla and Brian Korver 2003. Guidelines for writing RFC text on security considerations. RFC 3552 (Informational). (July 2003). https://tools.ietf.org/html/rfc3552

[48]

Benedikt Schmidt, Simon Meier, Cas Cremers, and David Basin. 2012. Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012, Stephen Chong (Ed.). IEEE, 78--94.

[49]

Serge Vaudenay. 2002. Security Flaws Induced by CBC Padding - Applications to SSL, IPSEC, WTLS ... Advances in Cryptology - EUROCRYPT 2002, International Conference on the Theory and Applications of Cryptographic Techniques, Amsterdam, The Netherlands, April 28 - May 2, 2002, Proceedings. 534--546. http://dx.doi.org/10.1007/3-540-46035-7_35

Cited By

Ahmed APeltonen ASethi MAura T(2024)Security Analysis of the Consumer Remote SIM Provisioning ProtocolACM Transactions on Privacy and Security10.1145/3663761Online publication date: 6-May-2024
https://dl.acm.org/doi/10.1145/3663761
Fujita KYoneyama K(2024)Formal Verification of Wireless Charging Standard QiProceedings of the 11th ACM Asia Public-Key Cryptography Workshop10.1145/3659467.3659904(23-31)Online publication date: 1-Jul-2024
https://dl.acm.org/doi/10.1145/3659467.3659904
Lauser TZelle DKern DKrauß CVölker L(2024)Security Protocols for Ethernet-Based In-Vehicle Communication2024 IEEE Vehicular Networking Conference (VNC)10.1109/VNC61989.2024.10575984(148-155)Online publication date: 29-May-2024
https://doi.org/10.1109/VNC61989.2024.10575984
Show More Cited By

Index Terms

A Comprehensive Symbolic Analysis of TLS 1.3
1. Security and privacy
  1. Formal methods and theory of security
    1. Logic and verification
  2. Network security
    1. Security protocols
    2. Web protocol security

Recommendations

TLS 1.3 in Practice:How TLS 1.3 Contributes to the Internet
WWW '21: Proceedings of the Web Conference 2021

Transport Layer Security (TLS) has become the norm for secure communication over the Internet. In August 2018, TLS 1.3, the latest version of TLS, was approved, providing improved security and performance of the previous TLS version. In this paper, we ...
Read More
A Cryptographic Analysis of the TLS 1.3 Handshake Protocol Candidates
CCS '15: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security

The Internet Engineering Task Force (IETF) is currently developing the next version of the Transport Layer Security (TLS) protocol, version 1.3. The transparency of this standardization process allows comprehensive cryptographic analysis of the ...
Read More
On the Security of TLS-DHE in the Standard Model
Proceedings of the 32nd Annual Cryptology Conference on Advances in Cryptology --- CRYPTO 2012 - Volume 7417

TLS is the most important cryptographic protocol in use today. However, up to now there is no complete cryptographic security proof in the standard model, nor in any other model. We give the first such proof for the core cryptographic protocol of TLS ...
Read More

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '17: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security

October 2017

2682 pages

ISBN:9781450349468

DOI:10.1145/3133956

General Chair:
Bhavani Thuraisingham
The University of Texas at Dallas, USA
,
Program Chairs:
David Evans
University of Virginia
,
Tal Malkin
Columbia University
,
Dongyan Xu
Purdue University

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 October 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Data Availability

Jonathan Hoyland - TLS13.mp4 https://dl.acm.org/doi/10.1145/3133956.3134063#Jonathan Hoyland - TLS13.mp4

Funding Sources

Conference

CCS '17

Sponsor:

SIGSAC

CCS '17: 2017 ACM SIGSAC Conference on Computer and Communications Security

October 30 - November 3, 2017

Texas, Dallas, USA

Acceptance Rates

CCS '17 Paper Acceptance Rate 151 of 836 submissions, 18%;

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '24

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 14 - 18, 2024

Salt Lake City , UT , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

117
Total Citations
View Citations
2,898
Total Downloads

Downloads (Last 12 months)851
Downloads (Last 6 weeks)92

Other Metrics

View Author Metrics

Citations

Cited By

Ahmed APeltonen ASethi MAura T(2024)Security Analysis of the Consumer Remote SIM Provisioning ProtocolACM Transactions on Privacy and Security10.1145/3663761Online publication date: 6-May-2024
https://dl.acm.org/doi/10.1145/3663761
Fujita KYoneyama K(2024)Formal Verification of Wireless Charging Standard QiProceedings of the 11th ACM Asia Public-Key Cryptography Workshop10.1145/3659467.3659904(23-31)Online publication date: 1-Jul-2024
https://dl.acm.org/doi/10.1145/3659467.3659904
Lauser TZelle DKern DKrauß CVölker L(2024)Security Protocols for Ethernet-Based In-Vehicle Communication2024 IEEE Vehicular Networking Conference (VNC)10.1109/VNC61989.2024.10575984(148-155)Online publication date: 29-May-2024
https://doi.org/10.1109/VNC61989.2024.10575984
Khan SGaba GBoeira FGurtov A(2024)Formal Verification and Security Assessment of the Drone Remote Identification Protocol2024 2nd International Conference on Unmanned Vehicle Systems-Oman (UVS)10.1109/UVS59630.2024.10467159(1-8)Online publication date: 12-Feb-2024
https://doi.org/10.1109/UVS59630.2024.10467159
Chen LXue KLi JLi ZYu N(2024)Security-Enhanced WireGuard Protocol Design Using Quantum Key Distribution2024 International Conference on Computing, Networking and Communications (ICNC)10.1109/ICNC59896.2024.10556292(718-723)Online publication date: 19-Feb-2024
https://doi.org/10.1109/ICNC59896.2024.10556292
Tran DDo CEscobar SOgata K(2023)Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel versionPeerJ Computer Science10.7717/peerj-cs.15569(e1556)Online publication date: 22-Sep-2023
https://doi.org/10.7717/peerj-cs.1556
Cremers CDax ANaska ACalandrino JTroncoso C(2023)Formal analysis of SPDMProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620607(6611-6628)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620607
Kumar AHippel MManolios PNita-Rotaru C(2023)Verification of GossipSub in ACL2sElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.393.10393(113-132)Online publication date: 14-Nov-2023
https://doi.org/10.4204/EPTCS.393.10
Xin WZhang HXu CYao JLi DJin T(2023)Verification of an Evolving Security Scheme in the Internet of VehiclesElectronics10.3390/electronics1221443812:21(4438)Online publication date: 28-Oct-2023
https://doi.org/10.3390/electronics12214438
Cheval VCrubillé RKremer S(2023)Symbolic protocol verification with dice1Journal of Computer Security10.3233/JCS-23003731:5(501-538)Online publication date: 13-Oct-2023
https://doi.org/10.3233/JCS-230037
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents