Formalizing, Analyzing and Improving Aerospace Security Protocols

Secure networking protocols for domains such as the internet and the internet-of-things are regularly scrutinized and discussed by the research community. This status quo can be attributed to their pervasiveness in the modern technological landscape and the heavy dependence on the security of these protocols to reliably fulfill myriad everyday tasks. In contrast, the security of aerospace protocols has not received a proportionate level of investigation despite the fact that an attack on these protocols may result in catastrophic consequences. The reason for this can be twofold; the digitization of avionic communication is an experimental and ongoing process with legacy analogue components still in use; and most non-terrestrial communication protocols are closed-source which limits their public scrutiny. This work endeavors to address this gap in three parallels; we propose a formalism that captures the security of the integral handover phase of aviation communication; we analyze the security of non-terrestrial protocol Bundle Protocol Security (BPSec) and propose security improvements; finally, we propose quantum-secure protocol constructions for aviation communication, supported by empirical results of their performance on resource-constrained devices.
We begin by introducing a universal formalized framework that captures handover schemes as a unique primitive. Moreover, we construct security experiments that cap- ture distinct security properties for handovers, and propose a generic protocol construction that captures all identified security properties. We then shift our focus to the analysis of the non-terrestrial BPSec protocol, which we analyze as a flexible secure channel and propose a stronger construction with additional integrity guarantees. Finally, we return to the aviation domain and propose quantum-secure protocol constructions for air-to-ground communication as well as handovers. We implement our secure avionic constructions and evaluate their performance on resource-constrained devices to account for resource limitations of on-board avionic components. We design our avionic handover construction
integrating our formalism for handovers, focusing on reducing the computational overhead of complex cryptographic operations. We formally prove the cryptographic security of our avionic protocol constructions within appropriate models capable of capturing their post- quantum security.