Title: Formal verification of secondary authentication protocol for 5G secondary authentication

Authors: Ed Kamya Kiyemba Edris; Mahdi Aiash; Jonathan Kok-Keong Loo; Mohammad Shadi Alhakeem

Addresses: School of Science and Technology, Middlesex University, London, UK ' School of Science and Technology, Middlesex University, London, UK ' School of Computer and Engineering, University of West London, London, UK ' Naif Arab University for Security Sciences, Riyadh, Saudi Arabia

Abstract: The fifth-generation mobile network (5G) will enable interconnectivity between the home network (HN) and data network (DN) whereby mobile users with their user equipment (UE) will be able to access services provided by external service providers (SP) seamlessly. The mobile user and SP will rely on security assurances provided by authentication protocols used. For 5G, primary authentication between the UE and the HN has been defined and specified by the Third Generation Partnership Project (3GPP) while the secondary authentication has also been defined but not specified. 3GPP recommends the extensible authentication protocol (EAP) framework for secondary authentication between the UE and the SP. However, the secondary authentication methods have not been formally verified, so this paper proposes a secondary authentication protocol (SAP) for service authentication and provides a comprehensive formal analysis using ProVerif a security protocol verifier. Finally, it conducts a security analysis on the protocol's security properties.

Keywords: 5G; secondary authentication; security protocol; services; formal methods; ProVerif; applied Pi calculus.

DOI: 10.1504/IJSN.2021.119379

International Journal of Security and Networks, 2021 Vol.16 No.4, pp.223 - 234

Received: 17 Aug 2020
Accepted: 03 Oct 2020
Published online: 02 Dec 2021 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article