{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,21]],"date-time":"2026-04-21T03:44:35Z","timestamp":1776743075665,"version":"3.51.2"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,30]],"date-time":"2017-10-30T00:00:00Z","timestamp":1509321600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-17-1-0206"],"award-info":[{"award-number":["FA9550-17-1-0206"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["610150"],"award-info":[{"award-number":["610150"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K035584\/1"],"award-info":[{"award-number":["EP\/K035584\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,10,30]]},"DOI":"10.1145\/3133956.3134063","type":"proceedings-article","created":{"date-parts":[[2017,10,27]],"date-time":"2017-10-27T12:48:18Z","timestamp":1509108498000},"page":"1773-1788","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":160,"title":["A Comprehensive Symbolic Analysis of TLS 1.3"],"prefix":"10.1145","author":[{"given":"Cas","family":"Cremers","sequence":"first","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}]},{"given":"Marko","family":"Horvat","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}]},{"given":"Jonathan","family":"Hoyland","sequence":"additional","affiliation":[{"name":"Royal Holloway, University of London, London, United Kingdom"}]},{"given":"Sam","family":"Scott","sequence":"additional","affiliation":[{"name":"Royal Holloway, University of London, London, United Kingdom"}]},{"given":"Thyla","family":"van der Merwe","sequence":"additional","affiliation":[{"name":"Royal Holloway, University of London, London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2017,10,30]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813707"},{"key":"e_1_3_2_2_2_1","volume-title":"Plaintext-Recovery Attacks Against Datagram TLS 19th Annual Network and Distributed System Security Symposium, NDSS 2012","author":"Nadhem","year":"2012","unstructured":"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"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.42"},{"key":"e_1_3_2_2_4_1","volume-title":"Formal Verification of TLS 1.3 Full Handshake Protocol Using ProVerif. TLS mailing list post. (February","author":"Arai Kenichi","year":"2016","unstructured":"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"},{"key":"e_1_3_2_2_5_1","volume-title":"5th USENIX Security Symposium. 689--706","author":"Aviram Nimrod","year":"2016","unstructured":"Nimrod Aviram, Sebastian Schinzel, Juraj Somorovsky, Nadia Heninger, Maik Dankel, Jens Steube, Luke Valenta, David Adrian, J. Alex Halderman, Viktor Dukhovni, Emilia K\u00e4sper, Shaanan Cohney, Susanne Engels, Christof Paar, and Yuval Shavitt 2016. DROWN: Breaking TLS with SSLv2. In 5th USENIX Security Symposium. 689--706."},{"key":"e_1_3_2_2_6_1","first-page":"111","article-title":"The Vulnerability of SSL to Chosen Plaintext Attack","volume":"2004","author":"Bard Gregory V.","year":"2004","unstructured":"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","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_3_2_2_7_1","volume-title":"SECRYPT","author":"Bard Gregory V.","year":"2006","unstructured":"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\u00fabal, Portugal, August 7--10, 2006, SECRYPT is part of ICETE - The International Joint Conference on e-Business and Telecommunications. 99--109."},{"key":"e_1_3_2_2_8_1","volume-title":"Annual International Cryptology Conference. Springer, 232--249","author":"Bellare Mihir","year":"1993","unstructured":"Mihir Bellare and Phillip Rogaway 1993. Entity authentication and key distribution. In Annual International Cryptology Conference. Springer, 232--249."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.39"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.37"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.14"},{"key":"e_1_3_2_2_14_1","unstructured":"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."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978423"},{"key":"e_1_3_2_2_16_1","volume-title":"IKE, and SSH Network and Distributed System Security Symposium--NDSS","author":"Bhargavan Karthikeyan","year":"2016","unstructured":"Karthikeyan Bhargavan and Ga\u00ebtan Leurent 2016. Transcript collision attacks: Breaking authentication in TLS, IKE, and SSH Network and Distributed System Security Symposium--NDSS 2016."},{"key":"e_1_3_2_2_17_1","unstructured":"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"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055716"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44987--6_28"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45146-4_34"},{"key":"e_1_3_2_2_21_1","unstructured":"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\/."},{"key":"e_1_3_2_2_22_1","volume-title":"2016 IEEE Symposium on. IEEE, 470--485","author":"Cremers Cas","unstructured":"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."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_2_24_1","volume-title":"USA","author":"Dowling Benjamin","year":"2015","unstructured":"Benjamin Dowling, Marc Fischlin, Felix G\u00fcnther, 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"},{"key":"e_1_3_2_2_26_1","volume-title":"Here Come the \u00f8plus Ninjas. Unpublished manuscript. (May","author":"Duong Thai","year":"2011","unstructured":"Thai Duong and Juliano Rizzo 2011. Here Come the \u00f8plus Ninjas. Unpublished manuscript. (May 2011)."},{"key":"e_1_3_2_2_27_1","volume-title":"The CRIME Attack. Ekoparty Security Conference presentation.","author":"Duong Thai","year":"2012","unstructured":"Thai Duong and Juliano Rizzo 2012. The CRIME Attack. Ekoparty Security Conference presentation. (2012)."},{"key":"e_1_3_2_2_28_1","volume-title":"SP 2016, San Jose, CA, USA, May 23--25","author":"Fischlin Marc","year":"2016","unstructured":"Marc Fischlin, Felix G\u00fcnther, 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."},{"key":"e_1_3_2_2_29_1","unstructured":"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."},{"key":"e_1_3_2_2_31_1","volume-title":"USA","author":"Jager Tibor","year":"2015","unstructured":"Tibor Jager, J\u00f6rg 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"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45238-6_33"},{"key":"e_1_3_2_2_33_1","first-page":"20","article-title":"(De-)Constructing TLS","volume":"2014","author":"Kohlweiss Markulf","year":"2014","unstructured":"Markulf Kohlweiss, Ueli Maurer, Cristina Onete, Bj\u00f6rn Tackmann, and Daniele Venturi. 2014. (De-)Constructing TLS. IACR Cryptology ePrint Archive Vol. 2014 (2014), 20. http:\/\/eprint.iacr.org\/2014\/020","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14623-7_34"},{"key":"e_1_3_2_2_35_1","first-page":"978","article-title":". The OPTLS Protocol and TLS 1.3","volume":"2015","author":"Krawczyk Hugo","year":"2015","unstructured":"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","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75670-5_1"},{"key":"e_1_3_2_2_37_1","unstructured":"A. Langley and W. Chang 2013. QUIC Crypto. (June 2013). Available at https:\/\/docs.google.com\/document\/d\/1g5nIXAIkN_Y-7XJW5K45IblHd_L2f5LTaDUDwvZ5L6g\/."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54631-0_38"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.1997.596782"},{"key":"e_1_3_2_2_40_1","volume-title":"Security review of TLS1.3 0-RTT. TLS mailing list post. (May","author":"MacC\u00e1rthaigh Colm","year":"2017","unstructured":"Colm MacC\u00e1rthaigh. 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."},{"key":"e_1_3_2_2_41_1","volume-title":"Attacking SSL when using RC4. White Paper. (March","author":"Mantin Itsik","year":"2015","unstructured":"Itsik Mantin. 2015. Attacking SSL when using RC4. White Paper. (March 2015). https:\/\/www.imperva.com\/docs\/HII_Attacking_SSL_when_using_RC4.pdf"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382206"},{"key":"e_1_3_2_2_43_1","volume-title":"Security of CBC Ciphersuites in SSL\/TLS: Problems and Countermeasures. Unpublished manuscript. (May","author":"Moeller Bodo","year":"2004","unstructured":"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."},{"key":"e_1_3_2_2_44_1","volume-title":"This POODLE bites: Exploiting The SSL 3.0 Fallback. Security Advisory. (September","author":"M\u00f6ller Bodo","year":"2014","unstructured":"Bodo M\u00f6ller, 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"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49100-4_7"},{"key":"e_1_3_2_2_46_1","volume-title":"The Transport Layer Security (TLS) Protocol Version 1.3 (draft, revision 10). (October","author":"Rescorla E.","year":"2015","unstructured":"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."},{"key":"e_1_3_2_2_47_1","volume-title":"Guidelines for writing RFC text on security considerations. RFC 3552 (Informational). (July","author":"Rescorla Eric","year":"2003","unstructured":"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"},{"key":"e_1_3_2_2_48_1","volume-title":"Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties 25th IEEE Computer Security Foundations Symposium, CSF 2012","author":"Schmidt Benedikt","year":"2012","unstructured":"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."},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46035-7_35"}],"event":{"name":"CCS '17: 2017 ACM SIGSAC Conference on Computer and Communications Security","location":"Dallas Texas USA","acronym":"CCS '17","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133956.3134063","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133956.3134063","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133956.3134063","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:03Z","timestamp":1750212663000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133956.3134063"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,30]]},"references-count":45,"alternative-id":["10.1145\/3133956.3134063","10.1145\/3133956"],"URL":"https:\/\/doi.org\/10.1145\/3133956.3134063","relation":{},"subject":[],"published":{"date-parts":[[2017,10,30]]},"assertion":[{"value":"2017-10-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}