research-article

Open access

A comprehensive formal analysis of 5G handover

Authors:

Aleksi Peltonen,

David BasinAuthors Info & Claims

WiSec '21: Proceedings of the 14th ACM Conference on Security and Privacy in Wireless and Mobile Networks

Pages 1 - 12

https://doi.org/10.1145/3448300.3467823

Published: 28 June 2021 Publication History

Abstract

5G 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 autonomous vehicles, and must therefore be handed over from one network operator to another. We present a novel, comprehensive, formal analysis of the security of the device handover protocols specified in the 5G standard. Our analysis covers both handovers within the 5G core network, as well as fallback methods for backwards compatibility with 4G/LTE. We identify four main handover protocols and formally model them in the security protocol verification tool Tamarin. Using these models, we determine for each protocol the minimal set of security assumptions required for its intended security goals to be met. Understanding these requirements is essential when designing devices and other protocols that depend on the reliability and security of network handovers.

References

[1]

3GPP. 2020. 3GPP System Architecture Evolution (SAE); Security architecture. TS 33.401, V16.3.0.

[2]

3GPP. 2020. General Packet Radio Service (GPRS) enhancements for Evolved Universal Terrestrial Radio Access Network (E-UTRAN) access. TS 23.401, V16.7.0.

[3]

3GPP. 2020. Generic Authentication Architecture (GAA); Generic Bootstrapping Architecture (GBA). TS 33.220, V16.7.0.

[4]

3GPP. 2020. NR and NG-RAN Overall Description. TS 38.300, V16.2.0.

[5]

3GPP. 2020. Procedures for the 5G System (5GS). TS 23.502, V16.5.0.

[6]

3GPP. 2020. Security architecture and procedures for 5G system. TS 33.501, V16.3.0.

[7]

3GPP. 2020. Summary of Rel-16 Work Items. TR 21.916, V0.4.0.

[8]

3GPP. 2020. System Architecture for the 5G System (5GS). TS 23.501, V16.5.0.

[9]

David Basin, Jannik Dreier, Lucca Hirschi, Saša Radomirović, Ralf Sasse, and Vincent Stettler. 2018. A Formal Analysis of 5G Authentication. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (Toronto, Canada) (CCS '18). Association for Computing Machinery, New York, NY, USA, 1383--1396.

Digital Library

[10]

David Basin, Saša Radomirović, and Lara Schmid. 2016. Modeling Human Errors in Security Protocols. In 2016 IEEE 29th Computer Security Foundations Symposium. IEEE, 325--340.

[11]

Piergiuseppe Bettassa Copet, Guido Marchetto, Riccardo Sisto, and Luciana Costa. 2017. Formal verification of LTE-UMTS and LTE-LTE handover procedures. Computer Standards & Interfaces 50 (2017), 92--106.

Digital Library

[12]

Cas Cremers and Martin Dehnel-Wild. 2019. Component-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion. In Network and Distributed Systems Security (NDSS) Symposium 2019.

[13]

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 (Dallas, Texas, USA) (CCS '17). Association for Computing Machinery, New York, NY, USA, 1773--1788.

Digital Library

[14]

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 2016 IEEE Symposium on Security and Privacy (SP). IEEE, 470--485.

[15]

Konstantinos Dimou, Min Wang, Yu Yang, Muhammmad Kazmi, Anna Larmo, Jonas Pettersson, Walter Muller, and Ylva Timner. 2009. Handover within 3GPP LTE: Design Principles and Performance. In 2009 IEEE 70th Vehicular Technology Conference Fall. IEEE, 1--5.

[16]

Danny Dolev and Andrew Yao. 1983. On the Security of Public Key Protocols. IEEE Transactions on Information Theory 29, 2 (1983), 198--208.

Digital Library

[17]

Ericsson. 2016. Cellular networks for Massive IoT. Technical Report. https://www.ericsson.com/4ada75/assets/local/reports-papers/white-papers/wp_iot.pdf.

[18]

Ericsson. 2020. Ericsson Mobility Report, June 2020. Technical Report. https://www.ericsson.com/49da93/assets/local/mobility-report/documents/2020/june2020-ericsson-mobility-report.pdf.

[19]

Ericsson. 2021. Ericsson Mobility Report, February 2021. Technical Report. https://www.ericsson.com/49220c/assets/local/mobility-report/documents/2020/emr-q4-2020-update.pdf.

[20]

Noomene Ben Henda and Karl Norrman. 2014. Formal Analysis of Security Procedures in LTE - A Feasibility Study. In Research in Attacks, Intrusions and Defenses. Springer International Publishing, Cham, 341--361.

[21]

Mads Lauridsen, Lucas Chavarría Giménez, Ignacio Rodriguez, Troels B Sørensen, and Preben Mogensen. 2017. From LTE to 5G for Connected Mobility. IEEE Communications Magazine 55, 3 (March 2017), 156--162.

Digital Library

[22]

Gavin Lowe. 1997. A Hierarchy of Authentication Specifications. In Proceedings 10th Computer Security Foundations Workshop. IEEE, 31--43.

[23]

Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In Computer Aided Verification. Springer Berlin Heidelberg, Berlin, Heidelberg, 696--701.

[24]

Nokia and Omdia. 2020. Beyond connectivity: CSP perspectives on higher-value 5G use cases. Technical Report. https://onestore.nokia.com/asset/207152.

[25]

Hyun-Seo Park, Yuro Lee, Tae-Joong Kim, Byung-Chul Kim, and Jae-Yong Lee. 2018. Handover Mechanism in NR for Ultra-Reliable Low-Latency Communications. IEEE Network 32, 2 (2018), 41--47.

[26]

Aleksi Peltonen, Ralf Sasse, and David Basin. 2021. Tamarin models and instructions for reproducibility. https://github.com/tamarin-prover/tamarin-prover/tree/develop/examples/wisec21-5G-handover. Accessed: 2021-05-25.

[27]

Benedikt Schmidt, Simon Meier, Cas Cremers, and David Basin. 2012. Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties. In 2012 IEEE 25th Computer Security Foundations Symposium (CSF '12). IEEE Computer Society, USA, 78--94.

Digital Library

Cited By

Tu KAl Ishtiaq ARashid SDong YWang WWu THussain SBalzarotti DXu W(2024)Logic gone astrayProceedings of the 33rd USENIX Conference on Security Symposium10.5555/3698900.3699072(3063-3080)Online publication date: 14-Aug-2024
https://dl.acm.org/doi/10.5555/3698900.3699072
Corici MZope HBuhr HScheich CMagedanz T(2024)Shortcuts: A Simple Mechanism for Reducing the Data Path Delay in Beyond 5G and 6G Networks2024 27th Conference on Innovation in Clouds, Internet and Networks (ICIN)10.1109/ICIN60470.2024.10494443(47-51)Online publication date: 11-Mar-2024
https://doi.org/10.1109/ICIN60470.2024.10494443
Zhang BHu PAzirani ASalahuddin MBarradas DLimam NBoutaba R(2024)Secure and Efficient Group Handover Protocol in 5G Non-Terrestrial NetworksICC 2024 - IEEE International Conference on Communications10.1109/ICC51166.2024.10622669(5063-5068)Online publication date: 9-Jun-2024
https://doi.org/10.1109/ICC51166.2024.10622669
Show More Cited By

Index Terms

A comprehensive formal analysis of 5G handover
1. Networks
  1. Network protocols
    1. Protocol correctness
      1. Protocol testing and verification
  2. Network types
    1. Mobile networks

Recommendations

A Formal Analysis of 5G Authentication
CCS '18: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security

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 ...
5G: The Convergence of Wireless Communications

As the rollout of 4G mobile communication networks takes place, representatives of industry and academia have started to look into the technological developments toward the next generation (5G). Several research projects involving key international ...
5G mobile terminals with advanced QoS-based user-centric aggregation (AQUA) for heterogeneous wireless and mobile networks

In this paper we present an advanced QoS provisioning module with vertical multi-homing framework for future fifth generation (5G) mobile terminals with radio network aggregation capability and traffic load sharing in heterogeneous mobile and wireless ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

WiSec '21: Proceedings of the 14th ACM Conference on Security and Privacy in Wireless and Mobile Networks

June 2021

412 pages

ISBN:9781450383493

DOI:10.1145/3448300

General Chairs:
Christina Pöpper
New York University Abu Dhabi, AE
,
Mathy Vanhoef
New York University Abu Dhabi, AE
,
Program Chairs:
Lejla Batina
Radboud University, NL
,
René Mayrhofer
Johannes Kepler University Linz, AT

Copyright © 2021 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 June 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Academy of Finland

Conference

WiSec '21

Sponsor:

SIGSAC

WiSec '21: 14th ACM Conference on Security and Privacy in Wireless and Mobile Networks

June 28 - July 2, 2021

Abu Dhabi, United Arab Emirates

Acceptance Rates

WiSec '21 Paper Acceptance Rate 34 of 121 submissions, 28%;

Overall Acceptance Rate 98 of 338 submissions, 29%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
6,389
Total Downloads

Downloads (Last 12 months)823
Downloads (Last 6 weeks)69

Reflects downloads up to 29 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Tu KAl Ishtiaq ARashid SDong YWang WWu THussain SBalzarotti DXu W(2024)Logic gone astrayProceedings of the 33rd USENIX Conference on Security Symposium10.5555/3698900.3699072(3063-3080)Online publication date: 14-Aug-2024
https://dl.acm.org/doi/10.5555/3698900.3699072
Corici MZope HBuhr HScheich CMagedanz T(2024)Shortcuts: A Simple Mechanism for Reducing the Data Path Delay in Beyond 5G and 6G Networks2024 27th Conference on Innovation in Clouds, Internet and Networks (ICIN)10.1109/ICIN60470.2024.10494443(47-51)Online publication date: 11-Mar-2024
https://doi.org/10.1109/ICIN60470.2024.10494443
Zhang BHu PAzirani ASalahuddin MBarradas DLimam NBoutaba R(2024)Secure and Efficient Group Handover Protocol in 5G Non-Terrestrial NetworksICC 2024 - IEEE International Conference on Communications10.1109/ICC51166.2024.10622669(5063-5068)Online publication date: 9-Jun-2024
https://doi.org/10.1109/ICC51166.2024.10622669
Yang JWang Y(2024)Dependency-Graph Enabled Formal Analysis for 5G AKA Protocols: Assumption Propagation and VerificationICC 2024 - IEEE International Conference on Communications10.1109/ICC51166.2024.10622353(715-721)Online publication date: 9-Jun-2024
https://doi.org/10.1109/ICC51166.2024.10622353
Yang JArya SWang Y(2024)Formal-Guided Fuzz Testing: Targeting Security Assurance From Specification to Implementation for 5G and BeyondIEEE Access10.1109/ACCESS.2024.336961312(29175-29193)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2024.3369613
Goswami BChoudhury H(2024)A Secure and Fast Handover Authentication Scheme for 5G-Enabled IoT Using Blockchain TechnologyWireless Personal Communications10.1007/s11277-024-11559-5138:4(2155-2181)Online publication date: 15-Oct-2024
https://doi.org/10.1007/s11277-024-11559-5
Ye KMetere RYadav P(2024)User-Guided Verification of Security Protocols via Sound AnimationSoftware Engineering and Formal Methods10.1007/978-3-031-77382-2_3(33-51)Online publication date: 26-Nov-2024
https://doi.org/10.1007/978-3-031-77382-2_3
Morio KEsiyok IJackson DKünnemann RCalandrino JTroncoso C(2023)Automated security analysis of exposure notification systemsProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620606(6593-6610)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620606
Akon MYang TDong YHussain SMeng WJensen CCremers CKirda E(2023)Formal Analysis of Access Control Mechanism of 5G Core NetworkProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623113(666-680)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623113
Wang DQiu APartani SZhou QSchotten H(2023)Mitigating Unnecessary Handovers in Ultra-Dense Networks through Machine Learning-based Mobility Prediction2023 IEEE 97th Vehicular Technology Conference (VTC2023-Spring)10.1109/VTC2023-Spring57618.2023.10200542(1-7)Online publication date: Jun-2023
https://doi.org/10.1109/VTC2023-Spring57618.2023.10200542
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Figures

Tables

Media

View Table of Conten