In our talk, we therefore 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, which has also been used to formally verify TLS 1.3 and (post-quantum-)IKEv2, among others. 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.