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 pubfic key cryptographic technique, ASUE (authentication supplicant entity) and AE (authenticator entity) implement the mutual identity authentication aided by their trusting third ASE (authentication security entity) 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.