{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T17:04:56Z","timestamp":1753895096797,"version":"3.41.2"},"reference-count":37,"publisher":"International Association for Cryptologic Research","license":[{"start":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T00:00:00Z","timestamp":1704758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IACR CiC"],"accepted":{"date-parts":[[2024,3,5]]},"abstract":"<jats:p>Transitioning from classically to quantum secure key agreement protocols may require to exchange fundamental components, for example, exchanging Diffie-Hellman-like key exchange with a key encapsulation mechanism (KEM). Accordingly, the corresponding security proof can no longer rely on the Diffie-Hellman assumption, thus invalidating the security guarantees. As a consequence, the security properties have to be re-proven under a KEM-based security notion.<\/jats:p><jats:p>We initiate the study of the LDACS key agreement protocol (Edition 01.01.00 from 25.04.2023), which is soon-to-be-standardized by the International Civil Aviation Organization. The protocol's cipher suite features Diffie-Hellman as well as a KEM-based key agreement protocol to provide post-quantum security. While the former results in an instantiation of an ISO key agreement inheriting all security properties, the security achieved by the latter is ambiguous. We formalize the computational security using the systematic notions of de Saint Guilhem, Fischlin and Warinshi (CSF '20), and prove the exact security that the KEM-based variant achieves in this model; primarily entity authentication, key secrecy and key authentication. To further strengthen our \u201cpen-and-paper\u201d findings, we model the protocol and its security guarantees using Tamarin, providing an automated proof of the security against a Dolev-Yao attacker.<\/jats:p>","DOI":"10.62056\/aebn2isfg","type":"journal-article","created":{"date-parts":[[2024,4,9]],"date-time":"2024-04-09T19:27:10Z","timestamp":1712690830000},"update-policy":"https:\/\/doi.org\/10.62056\/adfjwm02dj","source":"Crossref","is-referenced-by-count":0,"title":["Post-Quantum Ready Key Agreement for Aviation"],"prefix":"10.62056","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3389-208X","authenticated-orcid":false,"given":"Marcel","family":"Tiepelt","sequence":"first","affiliation":[{"id":[{"id":"https:\/\/ror.org\/04t3en479","id-type":"ROR","asserted-by":"publisher"}],"name":"Karlsruhe Institute of Technology","place":["Am Fasanengarten 5, Karlsruhe, Germany, 76137, Germany"],"department":["KASTEL"]}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-4332-1194","authenticated-orcid":false,"given":"Christian","family":"Martin","sequence":"additional","affiliation":[{"id":[{"id":"https:\/\/ror.org\/04t3en479","id-type":"ROR","asserted-by":"publisher"}],"name":"Karlsruhe Institute of Technology","place":["Am Fasanengarten 5, Karlsruhe, Germany, 76137, Germany"],"department":["KASTEL"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1324-7574","authenticated-orcid":false,"given":"Nils","family":"Maeurer","sequence":"additional","affiliation":[{"id":[{"id":"https:\/\/ror.org\/04a3akw68","id-type":"ROR","asserted-by":"publisher"}],"name":"Airbus","place":["Willy-Messerschmitt-Stra\u00dfe 1, Taufkirchen, Germany, 82024, Germany"],"department":["Airbus Defence and Space"]}]}],"member":"48349","published-online":{"date-parts":[[2024,4,9]]},"reference":[{"article-title":"Post Quantum Cryptography","year":"2022","author":"National Institute for Standards","key":"ref1:nistpqcomp"},{"key":"ref2:CCS:BFWW11","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1145\/2046707.2046716","article-title":"Composability of Bellare-Rogaway key exchange protocols","volume-title":"ACM CCS 2011","author":"Christina Brzuska","year":"2011"},{"key":"ref3:C:CanKra02","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-45708-9_10","article-title":"Security Analysis of IKE's Signature-based Key-Exchange Protocol","volume-title":"CRYPTO\u00a02002","volume":"2442","author":"Ran Canetti","year":"2002"},{"key":"ref4:DBLP:series\/isc\/BoydMS20","series-title":"Information Security and Cryptography","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-58146-9","article-title":"Protocols for Authentication and Key Establishment, Second Edition","author":"Colin Boyd","year":"2020"},{"key":"ref5:DVW92","doi-asserted-by":"publisher","DOI":"10.1007\/BF00124891","article-title":"Authentication and authenticated key exchanges","author":"Diffie Whitfield","year":"1992","journal-title":"Designs, Codes and Cryptography"},{"key":"ref6:iso.11779.3","first-page":"23","article-title":"ISO\/IEC 11779-3","author":"ISO copyright office","year":"2021"},{"key":"ref7:RFC7296","doi-asserted-by":"publisher","DOI":"10.17487\/RFC7296","article-title":"Internet Key Exchange Protocol Version 2","author":"C. Kaufman","year":"2014"},{"key":"ref8:Krawczyk2003SIGMAT","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-540-45146-4_24","article-title":"SIGMA: The 'SIGn-and-MAc' Approach to Authenticated Diffie-Hellman and Its Use in the IKE-Protocols","volume-title":"Advances in Cryptology - CRYPTO 2003, 23rd Annual International Cryptology Conference, Santa Barbara, California, USA, August 17-21, 2003, Proceedings","volume":"2729","author":"Hugo Krawczyk","year":"2003"},{"key":"ref9:ESORICS:Cremers11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-23822-2_18","article-title":"Key Exchange in IPsec Revisited: Formal Analysis of IKEv1 and IKEv2","volume-title":"ESORICS\u00a02011","volume":"6879","author":"Cas J. F. Cremers","year":"2011"},{"key":"ref10:gazdag2021","series-title":"ACSAC '21","isbn-type":"print","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1145\/3485832.3485885","article-title":"A Formal Analysis of IKEv2\u2019s Post-Quantum Extension","volume-title":"Proceedings of the 37th Annual Computer Security Applications Conference","author":"Stefan-Lukas Gazdag","year":"2021","ISBN":"https:\/\/id.crossref.org\/isbn\/9781450385794"},{"key":"ref11:RFC8784","series-title":"Internet Request for Comments","doi-asserted-by":"publisher","DOI":"10.17487\/RFC8784","article-title":"Mixing Preshared Keys in the Internet Key Exchange Protocol Version 2 (IKEv2) for Post-quantum Security","author":"S. Fluhrer","year":"2020","ISSN":"https:\/\/id.crossref.org\/issn\/2070-1721","issn-type":"electronic"},{"key":"ref12:PQCRYPTO:BBFGS19","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-030-25510-7_12","article-title":"Hybrid Key Encapsulation Mechanisms and Authenticated Key Exchange","volume-title":"Post-Quantum Cryptography - 10th International Conference, PQCrypto 2019","author":"Nina Bindel","year":"2019"},{"key":"ref13:PQCRYPTO:Peikert14","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-319-11659-4_12","article-title":"Lattice Cryptography for the Internet","volume-title":"Post-Quantum Cryptography - 6th International Workshop, PQCrypto 2014","author":"Chris Peikert","year":"2014"},{"article-title":"Single European Sky ATM Research","year":"2023","author":"Single European Sky ATM Research Joint Undertaking (SESAR 3 JU)","key":"ref14:sesar"},{"article-title":"Internet Protocol Suite (IPS) for Aeronautical Safety Services Part 1 Airborne IPS System Technical Requirements","year":"2021","author":"Incorporated (ARINC) Aeronautical Radio","key":"ref15:arinc2021"},{"article-title":"ICAO - ANNEX 10 VOL III AMD 91 Aeronautical Telecommunications Volume III - Communications Systems (Part I - Digital Data Communication Systems; Part II - Voice Communication Systems)","year":"2021","author":"International Civil Aviation Organization (ICAO)","key":"ref16:icao20211"},{"article-title":"LDACS A\/G Specification, Edition 01.01.00, Template Edition 02.00.05, Edition date 25.04.2023","year":"2023","author":"SESAR JU","key":"ref17:ldacs.spec"},{"key":"ref18:9583714","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1109\/EuroSPW54576.2021.00019","article-title":"A Secure Cell-Attachment Procedure of LDACS","volume-title":"2021 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW)","author":"Nils M\u00e4urer","year":"2021"},{"key":"ref19:LDACSsec","isbn-type":"print","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1049\/SBRA545E_ch4","article-title":"Cybersecurity for the L-band Digital Aeronautical Communications System (LDACS)","author":"Nils M\u00e4urer","year":"2021","ISBN":"https:\/\/id.crossref.org\/isbn\/9781839533211"},{"key":"ref20:LDACSMakeformal","doi-asserted-by":"publisher","DOI":"10.18420\/cdm-2022-34-24","article-title":"Formal Verification of the LDACS MAKE Protocol","author":"Nils M\u00e4urer","year":"2022"},{"article-title":"Enabling the Next Generation in Air Traffic Management with AeroMACS","year":"2014","author":"Monica Paolini","key":"ref21:AeroMACS"},{"article-title":"SatCOM","year":"2023","author":"EUROCONTROL","key":"ref22:satcom"},{"key":"ref23:cryptoeprint:2019\/1203","doi-asserted-by":"publisher","DOI":"10.1109\/CSF49147.2020.00028","article-title":"Authentication in Key-Exchange: Definitions, Relations and Composition","author":"Cyprien Delpech de Saint Guilhem","year":"2019"},{"key":"ref24:EC:BelPoiRog00","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/3-540-45539-6_11","article-title":"Authenticated Key Exchange Secure against Dictionary Attacks","volume-title":"EUROCRYPT\u00a02000","volume":"1807","author":"Mihir Bellare","year":"2000"},{"key":"ref25:CSF:DelFisWar20","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1109\/CSF49147.2020.00028","article-title":"Authentication in Key-Exchange: Definitions, Relations and Composition","volume-title":"CSF 2020 Computer Security Foundations Symposium","author":"Cyprien Delpech de Saint Guilhem","year":"2020"},{"key":"ref26:needham1978","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","article-title":"Using Encryption for Authentication in Large Networks of Computers","volume":"21","author":"Roger M. Needham","year":"1978","journal-title":"Commun. ACM","ISSN":"https:\/\/id.crossref.org\/issn\/0001-0782","issn-type":"electronic"},{"key":"ref27:dolev1983","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","article-title":"On the Security of Public Key Protocols","volume":"29","author":"D. Dolev","year":"1983","journal-title":"IEEE Transactions on Information Theory"},{"key":"ref28:meier2013","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","article-title":"The TAMARIN Prover For The Symbolic Analysis Of Security Protocols","volume-title":"25th International Conference on Computer Aided Verification (CAV)","author":"S. Meier","year":"2013"},{"article-title":"Tamarin-Prover Manual","year":"2023","author":"The Tamarin Team","key":"ref29:tamarin2023"},{"key":"ref30:celi2022","isbn-type":"print","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-031-17143-7_4","article-title":"A Tale of Two Models: Formal Verification of KEMTLS via Tamarin","volume-title":"Computer Security \u2013 ESORICS 2022","author":"Sof\u00eda Celi","year":"2022","ISBN":"https:\/\/id.crossref.org\/isbn\/9783031171437"},{"key":"ref31:lowe1997","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1109\/CSFW.1997.596782","article-title":"A Hierarchy of Authentication Specifications","volume-title":"Proceedings 10th Computer Security Foundations Workshop","author":"G. Lowe","year":"1997"},{"key":"ref32:wireguard2017","article-title":"Formal verification of the WireGuard protocol","author":"Kevin Donenfeld Jason A and Milner","year":"2017","journal-title":"Technical Report, Tech. Rep."},{"key":"ref33:ldacs.sarps","first-page":"1","article-title":"CHAPTER 13 L-Band Digital Aeronautical Communications System (LDACS)","author":"International Civil Aviation organization (ICAO)","year":"2023"},{"key":"ref34:nist:fips1804","doi-asserted-by":"crossref","DOI":"10.6028\/NIST.FIPS.180-4","article-title":"Secure Hash Standard","author":"National Institute for Standards","year":"2015"},{"key":"ref35:C:Bellare06","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"602","DOI":"10.1007\/11818175_36","article-title":"New Proofs for NMAC and HMAC: Security without Collision-Resistance","volume-title":"CRYPTO\u00a02006","volume":"4117","author":"Mihir Bellare","year":"2006"},{"key":"ref36:rfc7815","doi-asserted-by":"publisher","DOI":"10.17487\/RFC7815","article-title":"Minimal Internet Key Exchange Protocol Version 2","author":"C. Kaufman","year":"2014"},{"article-title":"A tale of two models: formal verification of KEMTLS via Tamarin","year":"2022","author":"Sof\u00eda Celi","key":"ref37:EPRINT:CHSW22"}],"container-title":["IACR Communications in Cryptology"],"original-title":[],"language":"en","deposited":{"date-parts":[[2024,12,10]],"date-time":"2024-12-10T21:25:09Z","timestamp":1733865909000},"score":1,"resource":{"primary":{"URL":"https:\/\/cic.iacr.org\/p\/1\/1\/17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,9]]},"references-count":37,"URL":"https:\/\/doi.org\/10.62056\/aebn2isfg","archive":["Internet Archive","Internet Archive"],"relation":{},"ISSN":["3006-5496"],"issn-type":[{"type":"electronic","value":"3006-5496"}],"subject":[],"published":{"date-parts":[[2024,4,9]]},"assertion":[{"value":"2024-01-09","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-03-05","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}}],"article-number":"cc1-1-47"}}