Design, Formal Verification, and Evaluation of a Post-Quantum EDHOC Variant for UAV Communications - Meneses, Rodrigo Duarte de; Teixeira, Caio; Henriques, Marco Amaral (Anais do Simpósio Brasileiro de Cibersegurança (SBSeg), 2026)
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.