A Formal Analysis of 5G Authentication
By David A. Basin, Jannik Dreier, Lucca Hirschi, Sasa Radomirovic, Ralf Sasse, Vincent Stettler. Conference on Computer and Communications Security, 2018
441 citations recorded by the source corpus.
Mobile communication networks connect much of the world's population. The security of users' calls, SMSs, and mobile data depends on the guarantees provided by the Authenticated Key Exchange protocols used. For the next-generation network (5G), the 3GPP group has standardized the 5G AKA protocol for this purpose. We provide the first comprehensive formal model of a protocol from the AKA family: 5G AKA. We also extract precise requirements from the 3GPP standards defining 5G and we identify missing security goals. Using the security protocol verification tool Tamarin, we conduct a full, systematic, security evaluation of the model with respect to the 5G security goals. Our automated analysis identifies the minimal security assumptions required for each security goal and we find that some critical security goals are not met, except under additional assumptions missing from the standard. Finally, we make explicit recommendations with provably secure fixes for the attacks and weaknesses we found.
Subfields: Computer Networks and Communications, Information Systems
View Paper: https://www.semanticscholar.org/paper/7bf7e109dbfe2544488e174018c17e263f96a70a
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Computer Networks and Communications
In Information Systems
Citations in the corpus
- A Survey on Security and Privacy of 5G Technologies: Potential Solutions, Recent Advancements, and Future Directions (2020, methodology): “This is possible in 5G as the current USIMs are now capable of performing randomized asymmetric encryption operations [100], [108].”
- Security and Privacy for 6G: A Survey on Prospective Technologies and Challenges (2021, methodology): “Exploiting the vulnerability, an attacker can transfer his network bill to someone else for what he used on the SN [73].”