{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T19:06:09Z","timestamp":1771614369763,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,12,6]],"date-time":"2021-12-06T00:00:00Z","timestamp":1638748800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,12,6]]},"DOI":"10.1145\/3485832.3485885","type":"proceedings-article","created":{"date-parts":[[2021,12,6]],"date-time":"2021-12-06T13:42:32Z","timestamp":1638798152000},"page":"91-105","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["A formal analysis of IKEv2\u2019s post-quantum extension"],"prefix":"10.1145","author":[{"given":"Stefan-Lukas","family":"Gazdag","sequence":"first","affiliation":[{"name":"genua GmbH, Germany"}]},{"given":"Sophia","family":"Grundner-Culemann","sequence":"additional","affiliation":[{"name":"MNM-Team, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, Germany"}]},{"given":"Tobias","family":"Guggemos","sequence":"additional","affiliation":[{"name":"MNM-Team, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen & Institute of Earth Observation, German Aerospace Center (DLR), Germany"}]},{"given":"Tobias","family":"Heider","sequence":"additional","affiliation":[{"name":"genua GmbH, Germany"}]},{"given":"Daniel","family":"Loebenberger","sequence":"additional","affiliation":[{"name":"Fraunhofer AISEC, Germany"}]}],"member":"320","published-online":{"date-parts":[[2021,12,6]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","unstructured":"Carlisle Adams. 2005. Impersonation Attack. Springer US Boston MA 286\u2013286. https:\/\/doi.org\/10.1007\/0-387-23483-7_196","DOI":"10.1007\/0-387-23483-7_196"},{"key":"e_1_3_2_1_2_1","unstructured":"Richard Barnes Benjamin Beurdouche Jon Millican Emad Omara Katriel Cohn-Gordon and Raphael Robert. 2019. The Messaging Layer Security (MLS) Protocol. Internet-Draft draft-ietf-mls-protocol-08. Internet Engineering Task Force. https:\/\/datatracker.ietf.org\/doc\/html\/draft-ietf-mls-protocol-08 Work in Progress."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44987-6_28"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45708-9_10"},{"key":"e_1_3_2_1_5_1","volume-title":"International Symposium on Software Security. Springer, 356\u2013383","author":"Cervesato Iliano","year":"2002","unstructured":"Iliano Cervesato, Nancy Durgin, Patrick Lincoln, J Mitchell, and Andre Scedrov. 2002. A comparison between strand spaces and multiset rewriting for security protocol analysis. In International Symposium on Software Security. Springer, 356\u2013383."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.27"},{"key":"e_1_3_2_1_7_1","unstructured":"Katriel Cohn-Gordon Cas Cremers Luke Garratt Jon Millican and Kevin Milner. 2017. On Ends-to-Ends Encryption: Asynchronous Group Messaging with Strong Security Guarantees. Cryptology ePrint Archive Report 2017\/666. https:\/\/eprint.iacr.org\/2017\/666."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23822-2_18"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134063"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00012"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Jason\u00a0A Donenfeld. 2017. WireGuard: Next Generation Kernel Network Tunnel.. In NDSS.","DOI":"10.14722\/ndss.2017.23160"},{"key":"e_1_3_2_1_13_1","unstructured":"Jason\u00a0A Donenfeld and Kevin Milner. 2017. Formal verification of the wireguard protocol. Technical Report. Technical Report."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","unstructured":"P. Eronen and J. Korhonen. 2006. Multiple Authentication Exchanges in the Internet Key Exchange (IKEv2) Protocol. RFC 4739 (Experimental). https:\/\/doi.org\/10.17487\/RFC4739","DOI":"10.17487\/RFC4739"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","unstructured":"P. Eronen H. Tschofenig and Y. Sheffer. 2010. An Extension for EAP-Only Authentication in IKEv2. RFC 5998 (Proposed Standard). https:\/\/doi.org\/10.17487\/RFC5998","DOI":"10.17487\/RFC5998"},{"key":"e_1_3_2_1_16_1","volume-title":"Maude-NPA: Cryptographic protocol analysis modulo equational properties","author":"Escobar Santiago","unstructured":"Santiago Escobar, Catherine Meadows, and Jos\u00e9 Meseguer. 2009. Maude-NPA: Cryptographic protocol analysis modulo equational properties. In Foundations of Security Analysis and Design V. Springer, 1\u201350."},{"key":"e_1_3_2_1_17_1","volume-title":"29th {USENIX} Security Symposium ({USENIX} Security 20). 1857\u20131874.","author":"Girol Guillaume","unstructured":"Guillaume Girol, Lucca Hirschi, Ralf Sasse, Dennis Jackson, Cas Cremers, and David Basin. 2020. A spectral analysis of noise: a comprehensive, automated, formal analysis of Diffie-Hellman protocols. In 29th {USENIX} Security Symposium ({USENIX} Security 20). 1857\u20131874."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","unstructured":"D. Harkins and D. Carrel. 1998. The Internet Key Exchange (IKE). RFC 2409 (Proposed Standard). https:\/\/doi.org\/10.17487\/RFC2409 Obsoleted by RFC 4306 updated by RFC 4109.","DOI":"10.17487\/RFC2409"},{"key":"e_1_3_2_1_19_1","unstructured":"Tobias Heider. 2019. Towards a Verifiably Secure Quantum Resistant Key Exchange in IKEv2. http:\/\/mnm-team.org\/pub\/Diplomarbeiten\/heid19"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","unstructured":"C. Kaufman P. Hoffman Y. Nir P. Eronen and T. Kivinen. 2014. Internet Key Exchange Protocol Version 2 (IKEv2). RFC 7296 (Internet Standard). https:\/\/doi.org\/10.17487\/RFC7296 Updated by RFCs 7427 7670 8247.","DOI":"10.17487\/RFC7296"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","unstructured":"C. Kaufman (Ed.). 2005. Internet Key Exchange (IKEv2) Protocol. RFC 4306 (Proposed Standard). https:\/\/doi.org\/10.17487\/RFC4306 Obsoleted by RFC 5996 updated by RFC 5282.","DOI":"10.17487\/RFC4306"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","unstructured":"S. Kent. 2005. IP Authentication Header. RFC 4302 (Proposed Standard). https:\/\/doi.org\/10.17487\/RFC4302","DOI":"10.17487\/RFC4302"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","unstructured":"S. Kent. 2005. IP Encapsulating Security Payload (ESP). RFC 4303 (Proposed Standard). https:\/\/doi.org\/10.17487\/RFC4303","DOI":"10.17487\/RFC4303"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","unstructured":"S. Kent and K. Seo. 2005. Security Architecture for the Internet Protocol. RFC 4301 (Proposed Standard). https:\/\/doi.org\/10.17487\/RFC4301 Updated by RFCs 6040 7619.","DOI":"10.17487\/RFC4301"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","unstructured":"T. Kivinen. 2016. Minimal Internet Key Exchange Version 2 (IKEv2) Initiator Implementation. RFC 7815 (Informational). https:\/\/doi.org\/10.17487\/RFC7815","DOI":"10.17487\/RFC7815"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45146-4_24"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/794197.795075"},{"key":"e_1_3_2_1_28_1","unstructured":"Robert\u00a0J. McEliece. 1978. A public-key cryptosystem based on algebraic coding theory. Deep Space Network Progress Report 44 (1978) 114\u2013116."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1999.766916"},{"key":"e_1_3_2_1_30_1","volume-title":"The TAMARIN Prover for the Symbolic Analysis of Security Protocols","author":"Meier Simon","unstructured":"Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 696\u2013701."},{"key":"e_1_3_2_1_31_1","volume-title":"AVISPA Project Deliverable D6. 2: Specification of the Problems in the High-Level Specification Language","author":"Moedersheim S","year":"2003","unstructured":"S Moedersheim, PH Drielsma, 1997. AVISPA Project Deliverable D6. 2: Specification of the Problems in the High-Level Specification Language (2003)."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","unstructured":"E. Rescorla. 2018. The Transport Layer Security (TLS) Protocol Version 1.3. RFC 8446 (Proposed Standard). https:\/\/doi.org\/10.17487\/RFC8446","DOI":"10.17487\/RFC8446"},{"key":"e_1_3_2_1_33_1","unstructured":"Valery Smyslov. 2019. Intermediate Exchange in the IKEv2 Protocol. Internet-Draftdraft-ietf-ipsecme-ikev2-intermediate-03. Internet Engineering Task Force. https:\/\/datatracker.ietf.org\/doc\/html\/draft-ietf-ipsecme-ikev2-intermediate-03 Work in Progress."},{"key":"e_1_3_2_1_34_1","unstructured":"The\u00a0Tamarin Team. 2016. Tamarin-Prover Manual. https:\/\/tamarin-prover.github.io\/manual\/tex\/tamarin-manual.pdf"},{"key":"e_1_3_2_1_35_1","volume-title":"Scott Fluhrer, Daniel\u00a0Van Geest, Oscar Garcia-Morchon, and Valery Smyslov.","author":"Tjhai C.","year":"2020","unstructured":"C. Tjhai, M. Tomlinson, grbartle@cisco.com, Scott Fluhrer, Daniel\u00a0Van Geest, Oscar Garcia-Morchon, and Valery Smyslov. 2020. Multiple Key Exchanges in IKEv2. Internet-Draftdraft-ietf-ipsecme-ikev2-multiple-ke-00. Internet Engineering Task Force. https:\/\/datatracker.ietf.org\/doc\/html\/draft-ietf-ipsecme-ikev2-multiple-ke-00 Work in Progress."},{"key":"e_1_3_2_1_36_1","unstructured":"Trevor Perrin. 2018. The Noise protocol framework. https:\/\/noiseprotocol.org\/noise.html"},{"key":"e_1_3_2_1_37_1","unstructured":"Tristan Ninet. 26.06.2020. Formal verification of the Internet Key Exchange (IKEv2) security protocol. Ph.D. Dissertation. Universit\u00e9 Rennes 1. https:\/\/tel.archives-ouvertes.fr\/tel-02882167\/"}],"event":{"name":"ACSAC '21: Annual Computer Security Applications Conference","location":"Virtual Event USA","acronym":"ACSAC '21"},"container-title":["Annual Computer Security Applications Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485832.3485885","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485832.3485885","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T19:13:51Z","timestamp":1755890031000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485832.3485885"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,6]]},"references-count":37,"alternative-id":["10.1145\/3485832.3485885","10.1145\/3485832"],"URL":"https:\/\/doi.org\/10.1145\/3485832.3485885","relation":{},"subject":[],"published":{"date-parts":[[2021,12,6]]},"assertion":[{"value":"2021-12-06","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}