基于PCL的3GPP-AKA协议的形式化分析与证明

Formal Analysis and Proof of the 3GPP-AKA Protocol Based on PCL

3GPP-AKA协议在第三代移动通信的安全性方面起着至关重要的作用,它保证了移动用户MS与VLR/HLR之间的双向认证及密钥协商。文中通过协议组合逻辑(PCL)对3GPP-AKA协议进行了形式化分析及安全性证明。分析表明3GPP-AKA协议可以满足它的安全目标,因此该协议可以安全的作为第三代移动通信中的认证和密钥分配协议。

The 3GPP-AKA protocol plays a very important role in the security of the third generation wireless communications. It captures the properties of mutual authentication and cipher key agreement between the MS and VLR/HLR. The formal analysis and security proof of the 3GPP-AKA protocol with protocol composition logic is presented in this paper. The analysis shows that the security goals of the protocol can be achieved. Therefore it can be securely used as the authentication and key agreement protocol in the third generation wireless communications.