David Basin
Jannik Dreier
ABSTRACT
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.
Supplemental Material
- 3GPP. 2001. 3G Security: Formal Analysis of the 3G Authentication Protocol. TS 33.902, v4.0.0.Google Scholar
- 3GPP. 2018. Security architecture and procedures for 5G system. TS 33.501, v15.1.0.Google Scholar
- Myrto Arapinis, Loretta Mancini, Eike Ritter, Mark Ryan, Nico Golde, Kevin Redon, and Ravishankar Borgaonkar. 2012. New privacy issues in mobile telephony: fix and verification. In Proceedings of the 2012 ACM conference on Computer and communications security. ACM, 205--216. Google ScholarDigital Library
- David Basin, Cas Cremers, and Simon Meier. 2013. Provably repairing the ISO/IEC 9798 standard for entity authentication. Journal of Computer Security, Vol. 21, 6 (2013), 817--846. Google ScholarDigital Library
- David Basin, Cas Cremers, Kunihiko Miyazaki, Savsa Radomirović, and Dai Watanabe. 2015a. Improving the security of cryptographic protocol standards. IEEE Security & Privacy, Vol. 13, 3 (2015), 24--31.Google ScholarDigital Library
- David Basin, Jannik Dreier, Lucca Hirschi, Savs a Radomirović, Ralf Sasse, and Vincent Stettler. 2018a. A Formal Analysis of 5G Authentication. arXiv preprint arXiv:1806.10360 (2018).Google Scholar
- David Basin, Jannik Dreier, Lucca Hirschi, Savsa Radomirović, Ralf Sasse, and Vincent Stettler. 2018b. Tamarin models, proofs and instructions for reproducibility. https://github.com/tamarin-prover/tamarin-prover/tree/develop/examples/ccs18--5G. Accessed: 2018-08--10.Google Scholar
- David Basin, Jannik Dreier, and Ralf Sasse. 2015b. Automated symbolic proofs of observational equivalence. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security. ACM. Google ScholarDigital Library
- Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. 2017. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. In 2017 IEEE Symposium on Security and Privacy (SP). 483--502.Google ScholarCross Ref
- Bruno Blanchet. 2016. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security, Vol. 1, 1--2 (Oct. 2016), 1--135. Google ScholarDigital Library
- Ravishankar Borgaonkar, Lucca Hirshi, Shinjo Park, Altaf Shaik, Andrew Martin, and Jean-Pierre Seifert. 2017. New Adventures in Spying 3G & 4G Users: Locate, Track, Monitor. https://www.blackhat.com/us-17/briefings.html#new-adventures-in-spying-3g-and-4g-users-locate-track-and-monitor Briefing at BlackHat USA 2017.Google Scholar
- Colin Boyd and Wenbo Mao. 1993. On a limitation of BAN logic. In Workshop on the Theory and Application of of Cryptographic Techniques. Springer, 240--247. Google ScholarDigital Library
- Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. 2018. DEEPSEC: Deciding Equivalence Properties in Security Protocols - Theory and Practice. In Proceedings of the 39th IEEE Symposium on Security and Privacy (S&P'18). IEEE Computer Society Press, San Francisco, CA, USA, 529--546.Google ScholarCross Ref
- Katriel Cohn-Gordon, Cas Cremers, and Luke Garratt. 2016. On post-compromise security. In Computer Security Foundations Symposium (CSF), 2016 IEEE 29th. IEEE, 164--178.Google ScholarCross Ref
- Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017. A Comprehensive Symbolic Analysis of TLS 1.3. In ACM CCS 2017: Proceedings of the 24th ACM Conference on Computer and Communications Security, Dallas, USA, 2017. 1773--1788. Google ScholarDigital Library
- Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017. A Comprehensive Symbolic Analysis of TLS 1.3. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, Bhavani M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). ACM, 1773--1788. Google ScholarDigital Library
- Cas Cremers, Marko Horvat, Sam Scott, and Thyla van der Merwe. 2016. Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication. In IEEE Symposium on Security and Privacy .Google Scholar
- Martin Dehnel-Wild and Cas Cremers. 2018. Authentication vulnerability in the most recent 5G AKA drafts (February 2018). http://www.cs.ox.ac.uk/people/cas.cremers/tamarin/5G/.Google Scholar
- Danny Dolev and Andrew C. Yao. 1981. On the security of public key protocols. Information Theory, IEEE Transactions on, Vol. 29, 2 (March 1981), 198--208. Google ScholarDigital Library
- Jannik Dreier, Lucca Hirschi, Savsa Radomirović, and Ralf Sasse. 2018. Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9--12, 2018. IEEE Computer Society, 359--373.Google Scholar
- Pierre-Alain Fouque, Cristina Onete, and Benjamin Richard. 2016. Achieving better privacy for the 3GPP AKA protocol. Proceedings on Privacy Enhancing Technologies, Vol. 2016, 4 (2016), 255--275.Google ScholarCross Ref
- Nico Golde, Kévin Redon, and Jean-Pierre Seifert. 2013. Let Me Answer That for You: Exploiting Broadcast Information in Cellular Networks. In 22Nd USENIX Conference on Security. USENIX Association. Google ScholarDigital Library
- GSMA. 2017. Global Mobile Trends 2017. https://www.gsma.com/globalmobiletrends/. Accessed: 2018-05-06.Google Scholar
- Syed Rafiul Hussain, Omar Chowdhury, Shagufta Mehnaz, and Elisa Bertino. 2018. LTEInspector: A Systematic Approach for Adversarial Testing of 4G LTE. In Network and Distributed Systems Security (NDSS) Symposium 2018 .Google ScholarCross Ref
- Nadim Kobeissi, Karthikeyan Bhargavan, and Bruno Blanchet. 2017. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. In IEEE European Symposium on Security and Privacy (EuroS&P) .Google ScholarCross Ref
- Robert Künnemann and Graham Steel. 2013. YubiSecure? Formal Security Analysis Results for the Yubikey and YubiHSM. In Security and Trust Management, Audun Jøsang, Pierangela Samarati, and Marinella Petrocchi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 257--272.Google Scholar
- Gavin Lowe. 1997. A Hierarchy of Authentication Specifications. In 10th Computer Security Foundations Workshop. IEEE Computer Society Press. Google ScholarDigital Library
- Simon Meier. 2013. Advancing automated security protocol verification. Ph.D. Dissertation. ETH Zurich.Google Scholar
- Simon Meier, Benedikt Schmidt, Cas J. F. Cremers, and David Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In CAV (LNCS), Vol. 8044. Springer, 696--701.Google Scholar
- Piers O'Hanlon, Ravishankar Borgaonkar, and Lucca Hirschi. 2017. Mobile subscriber WiFi Privacy. In 2017 IEEE Security and Privacy Workshops, SP Workshops 2017, San Jose, CA, USA, May 25, 2017. 169--178.Google ScholarCross Ref
- David Rupprecht, Adrian Dabrowski, Thorsten Holz, Edgar Weippl, and Christina Pöpper. 2018. On Security Research towards Future Mobile Network Generations. IEEE Communications Surveys & Tutorials (2018).Google ScholarCross Ref
- Benedikt Schmidt, Simon Meier, Cas Cremers, and David Basin. 2012. Automated analysis of Diffie-Hellman protocols and advanced security properties. In Computer Security Foundations Symposium (CSF). IEEE, 78--94. Google ScholarDigital Library
- Benedikt Schmidt, Ralf Sasse, Cas Cremers, and David Basin. 2014. Automated Verification of Group Key Agreement Protocols. In Proceedings of the 2014 IEEE Symposium on Security and Privacy (SP '14). IEEE Computer Society, Washington, DC, USA, 179--194. Google ScholarDigital Library
- Altaf Shaik, Jean-Pierre Seifert, Ravishankar Borgaonkar, N. Asokan, and Valtteri Niemi. 2016. Practical Attacks Against Privacy and Availability in 4G/LTE Mobile Communication Systems. In 23nd Annual Network and Distributed System Security Symposium, NDSS.Google ScholarCross Ref
- Fabian van den Broek, Roel Verdult, and Joeri de Ruiter. 2015. Defeating IMSI Catchers. Proceedings of the 2015 ACM Conference on Computer and Communications Security - CCS '15 (2015). Google ScholarDigital Library
Index Terms
- A Formal Analysis of 5G Authentication
Recommendations
A comprehensive formal analysis of 5G handover
WiSec '21: Proceedings of the 14th ACM Conference on Security and Privacy in Wireless and Mobile Networks5G has been under standardization for over a decade and will drive the world's mobile technologies in the decades to come. One of the cornerstones of the 5G standard is its security, also for devices that move frequently between networks, such as ...
Authentication for paranoids: multi-party secret handshakes
ACNS'06: Proceedings of the 4th international conference on Applied Cryptography and Network SecurityIn a society increasingly concerned with the steady assault on electronic privacy, the need for privacy-preserving techniques is both natural and justified. This need extends to traditional security tools such as authentication and key distribution ...
A Multi-Party Contract Signing Protocol and its Formal Analysis in Strand Space Model
ETCS '09: Proceedings of the 2009 First International Workshop on Education Technology and Computer Science - Volume 03Difficulties in designing multi-party contract signing (MPCS) protocols include providing concise and efficient protocols and at the same time keeping the protocols fair and abuse-free. This paper proposed an optimistic MPCS protocol. The number of ...
Comments