AERO-GUARD: A Post-Quantum Mutual Authentication Drone Protocol with Homomorphic Encryption for Secure Road Surveillance in Smart Cities
TL;DR
Formal verification results demonstrate that AERO-GUARD satisfies the targeted security properties, including mutual authentication, secrecy preservation, and replay resistance, confirming the protocol’s resilience against common authentication attacks.
Abstract
This paper presents AERO-GUARD, a formally verified drone authentication and road surveillance system that integrates Kyber post-quantum key encapsulation, physical unclonable functions (PUFs), decentralized IPFS-based identity storage, and blockchain-anchored audit logging. AERO-GUARD operates across three phases, key provisioning, enrollment, and authentication, enforcing mutual authentication, replay resistance, and privacy-preserving comparison through an off-chain evaluator (OCE) that performs homomorphic subtraction on encrypted PUF responses without accessing plaintext secrets. The protocol is modeled and verified using ProVerif 2.05 under the Dolev–Yao adversary model. To evaluate the system beyond theoretical verification, a simulation environment was developed to replicate realistic road conditions, incorporating a simulated road network and a virtual drone traversing monitored routes. An AI model is deployed to perform real-time detection of suspicious and anomalous activities along the road. All detection events are surfaced through a centralized monitoring dashboard that provides authorized personnel with live alerts, a drone camera livestream with detection annotations, and contextual drone telemetry, enabling timely and informed incident response. Formal verification results demonstrate that AERO-GUARD satisfies the targeted security properties, including mutual authentication, secrecy preservation, and replay resistance, confirming the protocol’s resilience against common authentication attacks.