Civil aviation is undergoing a transition towards digital, IP-based air–ground communication systems in order to accommodate increasing air traffic density, improve operational efficiency, and maintain safety-critical services. Within this evolution, technologies such as Controller–Pilot Data Link Communications (CPDLC), the L-band Digital Aeronautical Communications System (LDACS), and the Future Communication Infrastructure (FCI) have become key to enabling continuous data exchange between aircraft and ground systems. Despite their operational benefits, however, these systems do not yet provide security protection in a unified and consistently deployed manner across communication establishment, operational message exchange, and mobility or handover phases. In particular, guarantees related to mutual authentication, key establishment, integrity, confidentiality, and secure mobility management are not uniformly maintained across current air–ground communication environments. As a result, aviation communication systems remain exposed to replay, impersonation, message injection, man-in-the-middle (MITM), session hijacking, and denial-of-service (DoS) attacks, especially during mobility events and handover transitions, thereby posing significant risks to operational safety.

Motivated by these challenges, we develop lightweight, aviation-compatible, and formally verifiable security frameworks in this thesis to secure communication and handover across CPDLC, LDACS, and heterogeneous FCI environments. For CPDLC, the thesis introduces lightweight security mechanisms that provide mutual authentication, session key establishment, and secure handover by using Elliptic Curve Cryptography (ECC), Elliptic Curve Diffie–Hellman (ECDH), Schnorr signatures, and symmetric protection. For LDACS, the thesis strengthens security through lightweight authentication together with post-quantum-resilient key establishment and handover mechanisms. In this framework, Physically Unclonable Functions (PUFs) enable lightweight hardware-bound authentication, while the Bit-Flipping Key Encapsulation (BIKE) mechanism supports post-quantum-secure key establishment. This design reduces reliance on conventional public key infrastructure and supports secure key continuity across intra- and inter-domain scenarios. At the network level, the thesis further introduces a Host Identity Protocol (HIP)-based framework for the FCI to enable secure multi-homing and seamless mobility across heterogeneous links, including LDACS, the Aeronautical Mobile Airport Communications System (AeroMACS), and Satellite Communications (SATCOM).

To ensure that the proposed mechanisms provide rigorous security guarantees suitable for safety-critical aviation environments, the thesis complements framework design with formal security assurance. Symbolic analysis using Tamarin Prover and ProVerif is employed to establish essential properties, including authentication, key secrecy, forward secrecy, and secure handover, under strong adversary models. Overall, this thesis advances the security and robustness of both legacy and nextgeneration aviation communication systems across operational communication and mobility scenarios.