Formal Verification of Quantum-Resilient Authentication and Handover Protocols for LDACS
A systematic security and vulnerability assessment of LDACS authentication and mobility mechanisms using formal symbolic verification with the Tamarin prover provides formal evidence that the analyzed security mechanisms effectively mitigate cyber risks and enhance operational resilience, thereby supporting the safety...