Modeling and Verification of WPA3 Security Protocol Based on SPIN

Wi-Fi Protected Access 3 (WPA3) is the latest generation of Wi-Fi encryption protocol, and a comprehensive and systematic analysis of its security properties is of great significance for ensuring the security of network information transmission. In this paper, model checking technology is used to formalize analysis and verification of WPA3 protocol’s authentication and secrecy. Abstract modeling principles are proposed, initiator, responder and intruder models are constructed, authentication and secrecy are formally defined through operational semantics, and a state reduction strategy is proposed, that is, according to the protocol message set, static analysis strategy is used to reduce the invalid message attacks of attackers, and the problem of state explosion is effectively alleviated. Experimental results show that there is a key reinstallation attack in the protocol, and the corresponding solution is given. The method proposed in this paper can provide guideline for analyzing similar network security protocols.