Design, Formal Verification, and Evaluation of a Post-Quantum EDHOC Variant for UAV Communications

• Rodrigo Duarte de Meneses UNICAMP
• Caio Teixeira UNICAMP
• Marco Amaral Henriques UNICAMP

DOI: https://doi.org/10.5753/sbseg.2026.27127

Resumo

Unmanned Aerial Vehicle (UAV) swarms require secure and efficient protocols for communication in dynamic and adversarial environments. This paper presents a post-quantum authenticated key exchange protocol for UAV communications, inspired by recent post-quantum extensions of EDHOC. The protocol is modeled in SAPIC+ and verified in the Tamarin Prover under a Dolev–Yao adversary, establishing executability, mutual authentication, key secrecy, and forward secrecy properties. Communication overhead and handshake latency are estimated using standardized parameter sizes and benchmark data for ARM Cortex-M4 and x86 platforms, showing how the choice of post-quantum primitives affects the feasibility of authenticated key exchange in constrained UAV deployments.

Referências

Abadi, M., Blanchet, B., and Fournet, C. (2018). The applied pi calculus: Mobile values, new names, and secure communication. Journal of the ACM, 65(1):1–41.

Aissaoui, R. (2024). Assessment and Optimization of Post-Quantum Cryptographic Protocols for Civil UAV Communications. PhD thesis, École Nationale de l’Aviation Civile. Theses.fr ID: 2024ENAC0009.

Barbosa, M., Barthe, G., Bhargavan, K., Blanchet, B., Cremers, C., Liao, K., and Parno, B. (2021). SoK: Computer-aided cryptography. IEEE Symposium on Security and Privacy.

Bernstein, D. J. and Lange, T. (2024). eBACS: ECRYPT benchmarking of cryptographic systems. [link]. Accessed: 2026-05-07.

Blanchet, B. (2016). Modeling and verifying security protocols with the applied pi calculus and ProVerif. Foundations and Trends in Privacy and Security, 1(1–2):1–135.

Boneh, D. and Shoup, V. (2023). A graduate course in applied cryptography. [link]. Version 0.6.

Boyd, C. and Mathuria, A. (2019). Protocols for Authentication and Key Establishment. Springer, 2 edition.

Cheval, V., Jacomme, C., and Kremer, S. (2022). SAPIC+: Protocol verifiers of the world, unite! In 31st USENIX Security Symposium (USENIX Security 2022).

Cohn-Gordon, K., Cremers, C., and Garratt, L. (2016). Post-compromise security. Cryptology ePrint Archive, Paper 2016/221.

Dolev, D. and Yao, A. C. (1983). On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198–207.

Fedrecheski, G., Vučinić, M., and Watteyne, T. (2024). Performance comparison of EDHOC and DTLS 1.3 in internet-of-things environments. In 2024 IEEE Wireless Communications and Networking Conference (WCNC), pages 1–6.

Fraile, L. P., Koulamas, C., Fournaris, A. P., and Haleplidis, E. (2026). KEM-based authentication for EDHOC in initiator-known responder (IKR) scenarios. Internet-Draft draft-pocero-authkem-ikr-edhoc-02, Internet Engineering Task Force. Work in Progress.

Günther, F. and Mukendi, M. I. T. (2022). Careful with MAC-then-Sign: A computational analysis of the EDHOC lightweight authenticated key exchange protocol. Cryptology ePrint Archive, Paper 2022/1705.

He, L., Zhao, M., Wang, X., Wang, J., Wang, Z., and Liu, S. (2025). A post-quantum authentication and key agreement scheme for drone swarms. Electronics, 14(17).

Jacomme, C., Cremers, C., Bhargavan, K., Cherrier, S., Fouque, P.-A., and Lahiani, S. (2023). A comprehensive formal security analysis of EDHOC. In 32nd USENIX Security Symposium (USENIX Security 2023), pages 2607–2624, Anaheim, CA. USENIX Association.

Kannwischer, M. J., Petri, R., Rijneveld, J., Schwabe, P., and Stoffelen, K. (2024). PQM4: Post-quantum crypto library for the ARM Cortex-M4. [link].

Lenngren, E. (2021). P256-Cortex-M4: P-256 ECDSA / ECDH for Cortex-M4 and Cortex-M33. [link]. GitHub repository. Accessed: 2026-05-20.

Lowe, G. (1997). A hierarchy of authentication specifications. In Proceedings of the 10th IEEE Workshop on Computer Security Foundations, CSFW ’97, page 31, USA. IEEE Computer Society.

Meier, S., Schmidt, B., Cremers, C., and Basin, D. (2013). The Tamarin prover for the symbolic analysis of security protocols. In Computer Aided Verification – CAV 2013, volume 8044 of Lecture Notes in Computer Science, pages 696–701. Springer.

Nguyen, C. (2025). A formally verified quantum-safe key exchange protocol. Master’s thesis, Aalto University. Aaltodoc URN: urn:nbn:fi:aalto-202512179381.

NIST (2024a). Module-lattice-based digital signature standard (ML-DSA). Federal Information Processing Standards Publication FIPS 204, NIST.

NIST (2024b). Module-lattice-based key-encapsulation mechanism standard (ML-KEM). Federal Information Processing Standards Publication FIPS 203, NIST.

NIST (2024c). Stateless hash-based digital signature standard. Federal Information Processing Standards Publication FIPS 205, NIST.

NIST (2025a). NIST selects HQC as fifth algorithm for post-quantum encryption. [link]. Accessed: 2026-05-11.

NIST (2025b). Post-quantum cryptography standardization. [link]. Accessed: 2026-05-11.

Papon, C. and Onete, C. (2026). Post-quantum EDHOC: Initiator and responder using signature and/or KEM. Internet-Draft draft-papon-lake-pq-edhoc-00, Internet Engineering Task Force. Work in Progress.

Rescorla, E. (2018). The transport layer security (TLS) protocol version 1.3. RFC 8446, RFC Editor.

Selander, G., Mattsson, J., Palombini, F., and Seitz, L. (2024). Ephemeral Diffie-Hellman over COSE (EDHOC). RFC 9528, Internet Engineering Task Force.

Wu, Y., Jia, Z., Wu, Q., and Zhu, Y. (2025). A lightweight authentication and key agreement protocol design for FANET.

Xia, T., Wang, M., He, J., Yang, G., Fan, L., and Wei, G. (2024). A quantum-resistant identity authentication and key agreement scheme for UAV networks based on Kyber algorithm. Drones, 8(8).