Formal Verification of EAP-AKA with Improved Authentication Tests

EAP-AKA is the extensible authentication protocol (EAP) mechanism for authentication and key distribution using the authentication and key agreement (AKA) mechanism used in the 3^rd generation mobile networks. The improved authentication tests model is a formal verification method for security protocol analysis, 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