Cas Cremers (CISPA Helmholtz Center for Information Security), Martin Dehnel-Wild (University of Oxford)

The 5G mobile telephony standards are nearing completion; upon adoption these will be used by billions across the globe. Ensuring the security of 5G communication is of the utmost importance, building trust in a critical component of everyday life and national infrastructure.

We perform a fine-grained formal analysis of 5G’s main authentication and key agreement protocol (5G-AKA), and provide the first models that explicitly consider all parties defined by the protocol specification. Our formal analysis reveals that the security of 5G-AKA critically relies on unstated assumptions on the inner workings of the underlying channels. In practice this means that following the 5G-AKA specification, a provider can easily and ‘correctly’ implement the standard insecurely, leaving the protocol vulnerable to a security-critical race condition. We then provide the first models and analysis considering component and channel compromise in 5G, the results of which further demonstrate the fragility and subtle trust assumptions of the 5G-AKA protocol.

We propose formally verified fixes to the encountered issues, and we have worked with 3GPP to ensure that these fixes are adopted.

View More Papers

Time Does Not Heal All Wounds: A Longitudinal Analysis...

Meng Luo (Stony Brook University), Pierre Laperdrix (Stony Brook University), Nima Honarmand (Stony Brook University), Nick Nikiforakis (Stony Brook University)

Read More

Unveiling your keystrokes: A Cache-based Side-channel Attack on Graphics...

Daimeng Wang (University of California Riverside), Ajaya Neupane (University of California Riverside), Zhiyun Qian (University of California Riverside), Nael Abu-Ghazaleh (University of California Riverside), Srikanth V. Krishnamurthy (University of California Riverside), Edward J. M. Colbert (Virginia Tech), Paul Yu (U.S. Army Research Lab (ARL))

Read More

Send Hardest Problems My Way: Probabilistic Path Prioritization for...

Lei Zhao (Wuhan University), Yue Duan (University of California, Riverside), Heng Yin (University of California, Riverside), Jifeng Xuan (Wuhan University)

Read More

Mind Your Own Business: A Longitudinal Study of Threats...

Platon Kotzias (IMDEA Software Institute, Universidad Politécnica de Madrid), Leyla Bilge (Symantec Research Labs), Pierre-Antoine Vervier (Symantec Research Labs), Juan Caballero (IMDEA Software Institute)

Read More