Formal Verification of the LDACS MAKE Protocol

In our talk, we present the first formal verification of the security properties of the updated LDACS 3-pass Mutual Authentication and Key Establishment (MAKE) protocol. This protocol allows AS and GS to establish shared keys via Diffie-Hellman or a Key Encapsulation Mechanism, and to mutually authenticate communication partners in a three-way handshake. There are two variants: (1) The LDACS IKEv2 based 3-pass MAKE protocol and (2) the LDACS ISO/IEC 11770-3:2021 key agreement mechanism 7 based 3-pass MAKE protocol. The verification is done with the Tamarin Prover. We present our approach, point out security features and highlight difficulties in modelling the protocol correctly. Our work supports the on-going design and standardization process of LDACS