Communications in Cryptology IACR CiC

Post-Quantum Ready Key Agreement for Aviation


Marcel Tiepelt, Christian Martin, Nils Maeurer
Marcel Tiepelt ORCID
Karlsruhe Institute of Technology, Karlsruhe, Germany
marcel dot tiepelt at kit dot edu
Christian Martin ORCID
Karlsruhe Institute of Technology, Karlsruhe, Germany
christian dot martin at kit dot edu
Nils Maeurer ORCID
Airbus, Taufkirchen, Germany
nils dot maeurer at airbus dot com


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.

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 “pen-and-paper” findings, we model the protocol and its security guarantees using Tamarin, providing an automated proof of the security against a Dolev-Yao attacker.


Aeronautical Radio, Incorporated (ARINC). Internet Protocol Suite (IPS) for Aeronautical Safety Services Part 1 Airborne IPS System Technical Requirements. 06 2021.
Nina Bindel, Jacqueline Brendel, Marc Fischlin, Brian Goncalves, and Douglas Stebila. Hybrid key encapsulation mechanisms and authenticated key exchange. In Jintai Ding and Rainer Steinwandt, editors, Post-Quantum Cryptography - 10th International Conference, PQCrypto 2019, 206–226. Chongqing, China, May 8–10, 2019. Springer, Heidelberg, Germany.
Mihir Bellare. New proofs for NMAC and HMAC: Security without collision-resistance. In Cynthia Dwork, editor, CRYPTO 2006, volume 4117 of LNCS, 602–619. Santa Barbara, CA, USA, August 20–24, 2006. Springer, Heidelberg, Germany.
Christina Brzuska, Marc Fischlin, Bogdan Warinschi, and Stephen C. Williams. Composability of Bellare-Rogaway key exchange protocols. In Yan Chen, George Danezis, and Vitaly Shmatikov, editors, ACM CCS 2011, 51–62. Chicago, Illinois, USA, October 17–21, 2011. ACM Press.
Colin Boyd, Anish Mathuria, and Douglas Stebila. Protocols for Authentication and Key Establishment, Second Edition. Information Security and Cryptography. Springer, 2020.
Mihir Bellare, David Pointcheval, and Phillip Rogaway. Authenticated key exchange secure against dictionary attacks. In Bart Preneel, editor, EUROCRYPT 2000, volume 1807 of LNCS, 139–155. Bruges, Belgium, May 14–18, 2000. Springer, Heidelberg, Germany.
Sofía Celi, Jonathan Hoyland, Douglas Stebila, and Thom Wiggers. A Tale of Two Models: Formal Verification of KEMTLS via Tamarin. In Vijayalakshmi Atluri, Roberto Di Pietro, Christian D. Jensen, and Weizhi Meng, editors, Computer Security – ESORICS 2022, 63–83. Cham, 2022. Springer Nature Switzerland.
Sofía Celi, Jonathan Hoyland, Douglas Stebila, and Thom Wiggers. A tale of two models: formal verification of KEMTLS via tamarin. 2022.
Ran Canetti and Hugo Krawczyk. Security analysis of IKE's signature-based key-exchange protocol. In Moti Yung, editor, CRYPTO 2002, volume 2442 of LNCS, 143–161. Santa Barbara, CA, USA, August 18–22, 2002. Springer, Heidelberg, Germany.
ISO copyright office. ISO/IEC 11779-3. 2021.
Cas J. F. Cremers. Key exchange in IPsec revisited: formal analysis of IKEv1 and IKEv2. In Vijay Atluri and Claudia D\'ıaz, editors, ESORICS 2011, volume 6879 of LNCS, 315–334. Leuven, Belgium, September 12–14, 2011. Springer, Heidelberg, Germany.
Cyprien Delpech de Saint Guilhem, Marc Fischlin, and Bogdan Warinschi. Authentication in key-exchange: definitions, relations and composition. In Limin Jia and Ralf Küsters, editors, CSF 2020 Computer Security Foundations Symposium, 288–303. Boston, MA, USA, June 22–26, 2020. IEEE Computer Society Press.
Jason A Donenfeld and Kevin Milner. Formal verification of the WireGuard protocol. Technical Report, Tech. Rep., 2017.
Cyprien Delpech de Saint Guilhem, Marc Fischlin, and Bogdan Warinschi. Authentication in Key-Exchange: Definitions, Relations and Composition. 2019.
D. Dolev and A. Yao. On the Security of Public Key Protocols. IEEE Transactions on Information Theory, 29(2):198–208, 1983.
National Institute for Standards and Technology. Secure Hash Standard. 2015.
National Institute for Standards and Technology. Post Quantum Cryptography. 2022.
Stefan-Lukas Gazdag, Sophia Grundner-Culemann, Tobias Guggemos, Tobias Heider, and Daniel Loebenberger. A Formal Analysis of IKEv2’s Post-Quantum Extension. In Proceedings of the 37th Annual Computer Security Applications Conference, ACSAC '21, 91–105. New York, NY, USA, 2021. Association for Computing Machinery.
International Civil Aviation Organization (ICAO). ICAO - ANNEX 10 VOL III AMD 91 Aeronautical Telecommunications Volume III - Communications Systems (Part I - Digital Data Communication Systems; Part II - Voice Communication Systems) . 03 2021.
Single European Sky ATM Research Joint Undertaking (SESAR 3 JU). Single European Sky ATM Research. 2023.
C. Kaufman, P. Hoffman, Y. Nir, P. Eronen, and T. Kivinen. Internet Key Exchange Protocol Version 2. 2014.
C. Kaufman, P. Hoffman, Y. Nir, P. Eronen, and T. Kivinen. Minimal Internet Key Exchange Protocol Version 2. 2014.
Hugo Krawczyk. SIGMA: the 'sign-and-mac' approach to authenticated diffie-hellman and its use in the ike-protocols. In Dan Boneh, editor, Advances in Cryptology - CRYPTO 2003, 23rd Annual International Cryptology Conference, Santa Barbara, California, USA, August 17-21, 2003, Proceedings, volume 2729 of Lecture Notes in Computer Science, pages 400–425. Springer, 2003.
G. Lowe. A Hierarchy of Authentication Specifications. In Proceedings 10th Computer Security Foundations Workshop, 31–43. Rockport, MA, USA, 1997.
Nils Mäurer and Sophia Grundner-Culemann. Formal verification of the ldacs make protocol. 2022.
Nils Mäurer, Thomas Gräupl, Christoph Gentsch, Tobias Guggemos, Marcel Tiepelt, Corinna Schmitt, and Gabi Dreo Rodosek. A secure cell-attachment procedure of ldacs. In 2021 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW), volume, 113–122. 2021.
Nils Mäurer, Thomas Gräupl, and Corinna Schmitt. Cybersecurity for the l-band digital aeronautical communications system (ldacs). Technical Report, German Aerospace Center, 06 2021.
S. Meier, B. Schmidt, C. Cremers, and D. Basin. The TAMARIN Prover For The Symbolic Analysis Of Security Protocols. In 25th International Conference on Computer Aided Verification (CAV), 696–701. Saint Petersburg, Russia, 2013.
Roger M. Needham and Michael D. Schroeder. Using Encryption for Authentication in Large Networks of Computers. Commun. ACM, 21(12):993–999, dec 1978.
International Civil Aviation organization (ICAO). CHAPTER 13 L-Band Digital Aeronautical Communications System (LDACS). Technical Report, International Civil Aviation organization (ICAO), 2023.
Chris Peikert. Lattice cryptography for the internet. In Michele Mosca, editor, Post-Quantum Cryptography - 6th International Workshop, PQCrypto 2014, 197–219. Waterloo, Ontario, Canada, October 1–3, 2014. Springer, Heidelberg, Germany.
Monica Paolini and Senza Fili. Enabling the Next Generation in Air Traffic Management with AeroMACS. 2014.
The Tamarin Team. Tamarin-Prover Manual. 2023.
Diffie Whitfield, Paul C. Van Oorshot, and Michael J. Wiener. Authentication and authenticated key exchanges. Designs, Codes and Cryptography, 1992.

PDFPDF Open access

Submitted: 2024-01-09
Accepted: 2024-03-05
Published: 2024-04-09
How to cite

Marcel Tiepelt, Christian Martin, and Nils Maeurer, "Post-Quantum Ready Key Agreement for Aviation," IACR Communications in Cryptology, vol. 1, no. 1, Apr 09, 2024, doi: 10.62056/aebn2isfg.


Copyright is held by the author(s)

This work is licensed under a Creative Commons Attribution (CC BY) license.