5G-AKA-FS: A 5G Authentication and Key Agreement Protocol for Forward Secrecy

5G acts as a highway enabling innovative digital transformation and the Fourth Industrial Revolution in our lives. It is undeniable that the success of such a paradigm shift hinges on robust security measures. Foremost among these is primary authentication, the initial step in securing access to 5G network environments. For the 5G primary authentication, two protocols, namely 5G Authentication and Key Agreement (5G-AKA) and Improved Extensible Authentication Protocol Method for 3rd Generation Authentication and Key Agreement (EAP-AKA'), were proposed and standardized, where the former is for 3GPP devices, and the latter is for non-3GPP devices. Recent scrutiny has unveiled vulnerabilities in the 5G-AKA protocol, exposing it to security breaches, including linkability attacks. Moreover, mobile communication technologies are dramatically evolving while 3GPP has standardized Authentication and Key Management for Applications (AKMA) to reuse the credentials, generated during primary authentication, for 5G network applications. That makes it so significant for 5G-AKA to be improved to support forward secrecy as well as address security attacks. In response, several protocols have been proposed to mitigate these security challenges. In particular, they tried to strengthen security by reusing secret keys negotiated through the Elliptic Curve Integrated Encryption Scheme (ECIES) and countering linkability attacks. However, they still have encountered limitations in completing forward secrecy. Motivated by this, we propose an augmentation to 5G-AKA to achieve forward security and thwart linkability attacks (called 5G-AKA-FS). In 5G-AKA-FS, the home network (HN), instead of using its static ECIES key pair, generates a new ephemeral key pair to facilitate robust session key negotiation, truly realizing forward security. In order to thoroughly and precisely prove that 5G-AKA-FS is secure, formal security verification is performed by applying both BAN Logic and ProVerif. As a result, it is demonstrated that 5G-AKA-FS is valid. Besides, our performance comparison highlights that the communication and computation overheads are intrinsic to 5G-AKA-FS. This comprehensive analysis showcases how the protocol effectively balances between security and efficiency.