Biblio

The advent of 5G, one of the most recent and promising technologies currently under deployment, fulfills the emerging needs of mobile subscribers by introducing several new technological advancements. However, this may lead to numerous attacks in the emerging 5G networks. Thus, to guarantee the secure transmission of user data, 5G Authentication protocols such as Extensible Authentication Protocol - Authenticated Key Agreement Protocol (EAP-AKA) were developed. These protocols play an important role in ensuring security to the users as well as their data. However, there exists no guarantees about the security of the protocols. Thus formal verification is necessary to ensure that the authentication protocols are devoid of vulnerabilities or security loopholes. Towards this goal, we formally verify the security of the 5G EAP-AKA protocol using an automated verification tool called ProVerif. ProVerif identifies traces of attacks and checks for security loopholes that can be accessed by the attackers. In addition, we model the complete architecture of the 5G EAP-AKA protocol using the language called typed pi-calculus and analyze the protocol architecture through symbolic model checking. Our analysis shows that some cryptographic parameters in the architecture can be accessed by the attackers which cause the corresponding security properties to be violated.