Computational Security Analysis of the UMTS and LTE Authentication and Key Agreement Protocols

TL;DR

This paper provides the first formal computational security analysis of LTE and UMTS AKA protocols, revealing vulnerabilities and confirming security properties under certain cryptographic assumptions.

Contribution

It introduces the first formal, computational security analysis of LTE AKA and a detailed analysis of UMTS AKA considering core network message transport mechanisms.

Findings

Identifies vulnerabilities in UMTS and LTE AKA protocols.

Shows that certain configurations satisfy authentication and key secrecy properties.

Highlights the importance of session identifiers in security guarantees.

Abstract

We present a computational security analysis of the Authentication and Key Agreement (AKA) protocols for both Long-Term Evolution (LTE) and Universal Mobile Telecommunications System (UMTS). This work constitutes the first security analysis of LTE AKA to date and the first computationally sound analysis of UMTS AKA. Our work is the first formal analysis to consider messages that are sent in the core network, where we take into account details of the carrying protocol (i.e., MAP or Diameter) and of the mechanism for secure transport (i.e., MAPsec/TCAPsec or IPsec ESP). Moreover, we report on a deficiency in the protocol specifications of UMTS AKA and LTE AKA and the specifications of the core network security (called network domain security), which may enable efficient attacks. The vulnerability allows an inside attacker not only to impersonate an honest protocol participant during a run of the protocol but also to subsequently use wireless services on his behalf. UMTS AKA run over MAP with MAPsec seems vulnerable in the most straight-forward application of the attack. On the other hand, our analysis shows that UMTS and LTE AKA over Diameter/IPsec and UMTS AKA over MAP/TCAPsec (with sufficiently long session identifiers) computationally satisfy intended authentication properties as well as some key secrecy properties, assuming that the used primitives meet standard cryptographic assumptions.