Formal Analysis of 5G AKA Finds Gaps in the 5G Authentication Standard
At ACM CCS 2018 (Toronto, October 2018), Basin, Dreier, Hirschi, Radomirović, Sasse and Stettler presented the first comprehensive formal model of 3GPP 5G AKA and showed several critical security goals are not met without assumptions missing from the standard.
02Deep-Dive Technical Analysis
The team, led from ETH Zurich, extracted 5G AKA's security goals from 3GPP TS 33.501 and modelled the UE, serving network and home network in the Tamarin prover. Automated proofs confirmed improvements over 3G/4G AKA, such as SUPI concealment, but found that the standard alone does not guarantee the serving network and home network agree on which subscriber a session belongs to; per ETH, a poor implementation could leave users "charged for the mobile phone usage of a third party." The analysis also confirmed a subscriber-traceability privacy weakness and proposed provably secure fixes.
03Vulnerability & Exploit Flow
Underspecified binding between session keys and subscriber identity across serving and home networks, plus SQN-based traceability.
04Recommended Defense & Mitigation Protocol
Explicit key confirmation and subscriber-identity binding as recommended by the authors, considered through 3GPP SA3.
05Security Impact & Geopolitical Consequence
Established symbolic formal verification as a mainstream tool for 3GPP security review; the authors engaged with 3GPP and published their Tamarin models.
06Authoritative Standards & External References
07Related Topic Cluster Records
Master 5G Core, SS7 Defense & Subsea Cable Auditing
Ready to turn your historical knowledge into certified hands-on expertise? Register free on TelcoSec Academy to access interactive lab challenges, or consult our enterprise team for carrier-grade signaling assessments and portable BTS hardware.