Security analysis of 5G handover in commercial networks utilizing a formal method

The fifth-generation (5G) of mobile network is accelerating and expanding globally. The 5G Mobile subscribers pursue continuous and secure cellular services, even when they are on the move. Handover is the key to address this issue. This paper analyzes the security of 5G handover procedures in commercial networks utilizing a formal method, which has identified 5 vulnerabilities in the signaling process of 5G handover. Firstly, we abstract the state transfer system for 5G handover from the collected commercial network signaling messages, then we extract from the 5G security specifications the security properties that should be achieved by 5G handover and establish the appropriate channel model as well as the threat model. Finally, we use the TAMARIN prover to check whether the 5G handover model satisfies the combed security properties. We find that attackers could still launch attacks by exploiting (1) insufficiently validated measurement report messages and Radio Resource Control (RRC) reconfiguration messages; (2) inadequately protected registration messages, UE capability transfer messages, and identity request messages. Therefore, well-known security risks, such as Denial-of-Service (DoS) attacks, relay attacks, and power drain attacks, still apply to 5G handover in commercial networks.