Formal Analysis of WAPI Authentication and Key Agreement Protocol

Formal Analysis of WAPI Authentication and Key Agreement Protocol

연구 분야: Analysis

학회: International Conference on Information Security and Cryptology

The Wireless LAN Authentication and Privacy Infrastructure protocol(WAPI) is a mandatory standard for wireless LAN security in China. It has been widely used to protect the security of information transmission between mobile devices and access points in wireless LANs. However, the security of the WAPI protocol has not been fully proven, and there has been a lack of comprehensive and systematic analysis of its security. In this work, we conduct an extensive formal analysis of the WAPI authentication and key agreement protocol using the formal analysis tool Proverif. Our model is the first detailed enough to describe the security goals and the interaction process of WAPI, including certificate-based authentication, unicast key agreement, and multicast key agreement. The analysis reveals that the WAPI protocol cannot meet 9 out of 21 security goals, resulting in defects such as MITM attacks, DoS attacks, unicast key update failures, and multicast key reuse attacks. To address these issues, we propose specific improvement suggestions for the WAPI authentication and key agreement protocol.