Formal Verification for EAP-AKA Protocol in 3G Networks

In the 3G mobile networks, EAP-AKA is the extensible authentication protocol (EAP) mechanism for authentication and key distribution using the authentication and key agreement (AKA) mechanism. The improved authentication tests model is a formal method for authentication protocol verification, which enhances the original authentication tests model in proving symmetric key protocol and succeeds in finding flaws of security protocols. This paper formally analyzes and verifies the security properties of EAP-AKA authentication process with the improved authentication tests. The proof result shows that the authentication process of EAP-AKA can guarantee the security of wireless communication.