Formalization and evaluation of EAP-AKA’ protocol for 5G network access security

The end user’s Quality of Experience (QoE) will be improved while accessing services in Fifth Generation Mobile Network (5G), supported by enhanced security and privacy. The security guarantees offered by the Authentication and Key Agreement (AKA) protocols will be depended upon by end users and network operators. The AKA protocols have been standardized for 5G networks, and the Extensible Authentication Protocol (EAP)-AKA’ protocol is one of the main authentication mechanisms that has been specified for User Equipment (UE) and network mutual authentication. This article models the EAP-AKA’ protocol and conducts an extensive formal verification of the EAP-AKA’ protocol as defined in the 5G security standard to determine whether the protocol is verifiably secure for 5G. It provides a security evaluation of the EAP-AKA’ protocol based on the current 5G specifications using ProVerif, a security protocol proof verifier. It also presents security properties that support the security verification, as well as quantitative properties that are used to assess the protocol’s performance. Finally, it compares the EAP-AKA’ and 5G-AKA protocols’ security and performance results.