A Correctness Proof of WAPI Certificate Authentication Protocol

WAPI certificate authentication protocol is the core and key component of WAPI security mechanism proposed by Chinese WLAN standard. This protocol adopts public key cryptographic technique, ASUE and AE implement the mutual identity authentication aided by their trusting third ASE to realize secure access and negotiate the corresponding BK. Using a formal logic of PCL, WAPI certificate authentication protocol is programmed and its security properties are proved. The results show that if all the entities involved in the protocol do not reveal their long-term keys or short-term keys, this protocol provides the properties of strong session authentication and key secrecy and achieves its predefined security goals.