Formal Verification of EAP-AKA with Improved Authentication Tests

Author

Li, Xiehua ; Hao, Liming ; Yang, Shutang ; Li, Jianhua

Author_Institution

Dept. of Electron. Eng., Shanghai Jiao Tong Univ.

fYear

2006

fDate

22-24 Sept. 2006

Firstpage

1

Lastpage

4

Abstract

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

Keywords

3G mobile communication; formal verification; mobile radio; protocols; telecommunication security; 3^rd generation mobile networks; EAP-AKA; authentication and key agreement mechanism; authentication tests; extensible authentication protocol mechanism; formal verification method; security protocol analysis; symmetric key protocol; wireless communication; Access protocols; Authentication; Communication system security; Data communication; Data security; Formal verification; Random number generation; Testing; Wireless LAN; Wireless communication;

fLanguage

English

Publisher

ieee

Conference_Titel

Wireless Communications, Networking and Mobile Computing, 2006. WiCOM 2006.International Conference on

Conference_Location

Wuhan

Print_ISBN

1-4244-0517-3

Type

conf

DOI

10.1109/WiCOM.2006.300

Filename

4149477