Post-Quantum Ready Key Agreement for Aviation

Marcel Tiepelt; Christian Martin; Nils Maeurer

doi:10.62056/aebn2isfg

Post-Quantum Ready Key Agreement for Aviation

Authors

Marcel Tiepelt, Christian Martin, Nils Maeurer

Marcel Tiepelt

Karlsruhe Institute of Technology, Karlsruhe, Germany
marcel dot tiepelt at kit dot edu

Christian Martin

Karlsruhe Institute of Technology, Karlsruhe, Germany
christian dot martin at kit dot edu

Nils Maeurer

Airbus, Taufkirchen, Germany
nils dot maeurer at airbus dot com

Keywords: authenticated key exchange post-quantum key exchange formal verification LDACS

Abstract

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.

References

[{Aer}21]

Aeronautical Radio, Incorporated (ARINC). Internet Protocol Suite (IPS) for Aeronautical Safety Services Part 1 Airborne IPS System Technical Requirements. 06 2021.

Google Scholar ePrint

[BBF⁺19]

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. https://doi.org/10.1007/978-3-030-25510-7_12.

Google Scholar ePrint

[Bel06]

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. https://doi.org/10.1007/11818175_36.

Google Scholar ePrint

[BFWW11]

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. https://doi.org/10.1145/2046707.2046716.

Google Scholar ePrint

[BMS20]

Colin Boyd, Anish Mathuria, and Douglas Stebila. Protocols for Authentication and Key Establishment, Second Edition. Information Security and Cryptography. Springer, 2020. https://doi.org/10.1007/978-3-662-58146-9.

Google Scholar ePrint

[BPR00]

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. https://doi.org/10.1007/3-540-45539-6_11.

Google Scholar ePrint

[CHSW22a]

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. https://doi.org/10.1007/978-3-031-17143-7_4.

Google Scholar ePrint

[CHSW22b]

Sofía Celi, Jonathan Hoyland, Douglas Stebila, and Thom Wiggers. A tale of two models: formal verification of KEMTLS via tamarin. 2022.

Google Scholar ePrint

[CK02]

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. https://doi.org/10.1007/3-540-45708-9_10.

Google Scholar ePrint

[co21]

ISO copyright office. ISO/IEC 11779-3. 2021.

Google Scholar ePrint

[Cre11]

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. https://doi.org/10.1007/978-3-642-23822-2_18.

Google Scholar ePrint

[DFW20]

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. https://doi.org/10.1109/CSF49147.2020.00028.

Google Scholar ePrint

[DM17]

Jason A Donenfeld and Kevin Milner. Formal verification of the WireGuard protocol. Technical Report, Tech. Rep., 2017.

Google Scholar ePrint

[dSGFW19]

Cyprien Delpech de Saint Guilhem, Marc Fischlin, and Bogdan Warinschi. Authentication in Key-Exchange: Definitions, Relations and Composition. 2019. https://doi.org/10.1109/CSF49147.2020.00028.

Google Scholar ePrint

[DY83]

D. Dolev and A. Yao. On the Security of Public Key Protocols. IEEE Transactions on Information Theory, 29(2):198–208, 1983. https://doi.org/10.1109/TIT.1983.1056650.

Google Scholar ePrint

[EUR23]

EUROCONTROL. SatCOM. 2023.

Google Scholar ePrint

[FKMS20]

S. Fluhrer, P. Kampanakis, D. McGrew, and V. Smyslov. Mixing Preshared Keys in the Internet Key Exchange Protocol Version 2 (IKEv2) for Post-quantum Security. June 2020. https://doi.org/10.17487/RFC8784.

Google Scholar ePrint

[fST15]

National Institute for Standards and Technology. Secure Hash Standard. 2015.

Google Scholar ePrint

[fST22]

National Institute for Standards and Technology. Post Quantum Cryptography. 2022.

Google Scholar ePrint

[GGCG⁺21]

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. https://doi.org/10.1145/3485832.3485885.

Google Scholar ePrint

[{Int}21]

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.

Google Scholar ePrint

[JU23a]

SESAR JU. LDACS A/G Specification, Edition 01.01.00, Template Edition 02.00.05, Edition date 25.04.2023. Technical Report, SESAR JU, 2023.

Google Scholar ePrint

[JU)23b]

Single European Sky ATM Research Joint Undertaking (SESAR 3 JU). Single European Sky ATM Research. 2023.

Google Scholar ePrint

[KHN⁺14a]

C. Kaufman, P. Hoffman, Y. Nir, P. Eronen, and T. Kivinen. Internet Key Exchange Protocol Version 2. 2014. https://doi.org/10.17487/RFC7296.

Google Scholar ePrint

[KHN⁺14b]

C. Kaufman, P. Hoffman, Y. Nir, P. Eronen, and T. Kivinen. Minimal Internet Key Exchange Protocol Version 2. 2014. https://doi.org/10.17487/RFC7815.

Google Scholar ePrint

[Kra03]

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. https://doi.org/10.1007/978-3-540-45146-4_24.

Google Scholar ePrint

[Low97]

G. Lowe. A Hierarchy of Authentication Specifications. In Proceedings 10th Computer Security Foundations Workshop, 31–43. Rockport, MA, USA, 1997. https://doi.org/10.1109/CSFW.1997.596782.

Google Scholar ePrint

[MGC22]

Nils Mäurer and Sophia Grundner-Culemann. Formal verification of the ldacs make protocol. 2022. https://doi.org/10.18420/cdm-2022-34-24.

Google Scholar ePrint

[MGG⁺21]

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. https://doi.org/10.1109/EuroSPW54576.2021.00019.

Google Scholar ePrint

[MGS21]

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. https://doi.org/10.1049/SBRA545E_ch4.

Google Scholar ePrint

[MSCB13]

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. https://doi.org/10.1007/978-3-642-39799-8_48.

Google Scholar ePrint

[NS78]

Roger M. Needham and Michael D. Schroeder. Using Encryption for Authentication in Large Networks of Computers. Commun. ACM, 21(12):993–999, dec 1978. https://doi.org/10.1145/359657.359659.

Google Scholar ePrint

[oI23]

International Civil Aviation organization (ICAO). CHAPTER 13 L-Band Digital Aeronautical Communications System (LDACS). Technical Report, International Civil Aviation organization (ICAO), 2023.

Google Scholar ePrint

[Pei14]

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. https://doi.org/10.1007/978-3-319-11659-4_12.

Google Scholar ePrint

[PF14]

Monica Paolini and Senza Fili. Enabling the Next Generation in Air Traffic Management with AeroMACS. 2014.

Google Scholar ePrint

[Tea23]

The Tamarin Team. Tamarin-Prover Manual. 2023.

Google Scholar ePrint

[WVOW92]

Diffie Whitfield, Paul C. Van Oorshot, and Michael J. Wiener. Authentication and authenticated key exchanges. Designs, Codes and Cryptography, 1992. https://doi.org/10.1007/BF00124891.

Google Scholar ePrint

PDF Open access

DOI: https://doi.org/10.62056/aebn2isfg

History

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.

License

Copyright is held by the author(s)

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

@article{CiC-1-1-17,
    author = "Tiepelt, Marcel and Martin, Christian and Maeurer, Nils",
    journal = "{IACR} {C}ommunications in {C}ryptology",
    publisher = "{I}nternational {A}ssociation for {C}ryptologic {R}esearch",
    title = "Post-Quantum Ready Key Agreement for Aviation",
    volume = "1",
    number = "1",
    date = "2024-04-09",
    year = "2024",
    issn = "3006-5496",
    doi = "10.62056/aebn2isfg"
}

TY - JOUR
AU - Tiepelt, Marcel
AU - Martin, Christian
AU - Maeurer, Nils
PY  - 2024
TI  - Post-Quantum Ready Key Agreement for Aviation
JF  - IACR Communications in Cryptology
JA  - CIC
VL  - 1
IS  - 1
DO  - 10.62056/aebn2isfg
UR  - https://doi.org/10.62056/aebn2isfg
AB  - <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.</p><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 “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. </p>
ER  -

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.