AKA Protocol for 3G Mobile Communications and Its Formal Verification
Zhang Ai · Huadong Li-Gong Daxue xuebao · 2003
The development process and security mechanisms for mobile communications are reviewed. The 3GPP authentication and key agreement protocol (AKA) is introduced and formally verified using AUTLOG. It is proved that the goals of AKA protocol can be met successfully with the assumption that the communicatioin path between HE and SN is secure.