Formal Analysis And Research Of WAPI Authentication And Key Agreement Protocol

Wireless local area network(WLAN)security has always been central issues due to security vulnerabilities caused by the air interface transmission between terminal devices and local network access points.To ensure the security of WLAN,China has independently proposed the WLAN Authentication and Privacy Infrastructure(WAPI)protocol,which is widely used in essential area such as industrial internet,public security system,and national grid.WAPI is used to provide secure capabilities such as authentication,key negotiation,and MAC layer data encryption between terminal devices and local network access points.However,the security of WAPI protocol has not been fully discussed.We rely on the formal method,model and analyze the protocol with the formal analysis tool ProVerif,and conduct a systematic and comprehensive analysis of the security of WAPI authentication and key agreement protocol.Our main contributions of this thesis are as follows:1.Formalize the process of certificate-based authentication,unicast key negotiation,and multicast key negotiation in the WAPI authentication and key agreement protocol,and provide the protocol message flow.We extract the protocol flow description from the WAPI protocol specifications and figures out the message flow between protocol entities,which is the basis for formal modeling of the protocol.2.Propose security goals and threat model for WAPI authentication and key agreement protocol.In WAPI specifications,there lacks the definition of the security goals.We summarize the threat model and security goals of WAPI protocol by referring to existing formal analysis work of wireless local area network security protocols such as WPA2 and the application scenarios of the WAPI protocol.This is the key to the formal analysis of the WAPI protocol.3.Conduct formal modeling and analysis of the WAPI authentication and key agreement protocol and find several vulnerabilities in WAPI authentication and key agreement protocol.We use ProVerif to analyze WAPI authentication and key agreement protocol and find that the protocol cannot fully meet the authentication and confidentiality goals in the protocol.We find that WAPI authentication and key agreement protocol is vulnerable to DoS attack,MitM attack,unicast key update failure attack,and multicast key reuse attack.We give the detail steps of these attacks.4.Provide some suggestions for the improvements of WAPI authentication and key agreement protocol.Based on the formal analysis results,we explore the causes of attacks in the WAPI authentication and key agreement protocol and give some suggestions for the guidance of the subsequent updates and improvements of WAPI.