Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Kwon, S., Choim, H.K.: Evolution of Wi-Fi protected access: security challenges. IEEE Consum. Electron. Mag. 99, 1–1 (2020)
Ting, C., Guozheng, W., Liu, Z., Geguang, P., Zhao, R., Liu, K.: Analysis of NSFC formal methods field fund applications. Prospective Technol. 2(01), 132–140 (2023)
Tian, C., Deng, Y., Jiang, Y.: Introduction to the special topic on formal methods and applications. J. Soft. 32(06) (2021)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Soft. Concepts Tools. 17, 93–102 (1996)
Vanhoef, M., Piessens, F.: Key reinstallation attacks: Forcing nonce reuse in WPA2. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, ACM (2017)
Wang, W., Liu, Z.: The development and improvement of cryptography and encryption technology. Digital Technol. Appl. 40(01), 237–239 (2022)
Hyun, N.J., Yeop, L.J., Hui, K.S., Kee, C.H.: Comparative analysis on security protocols of WPA3 standard for secure wireless LAN environments. J. Korean Inst. 44(10), 1878–1887 (2019)
Yao, S.: Analysis of asymmetric encryption technology. Electron. Technol. 49(07), 50–51 (2020)
Harkins. D.: Simultaneous authentication of equals: a secure, password-based key exchange for mesh networks. In: Proceedings of the 2008 Second International Conference on Sensor Technologies and Applications, IEEE (2008)
Heng, W.G., Lin, Q.Y, Wei, F.: An Improved Security authentication protocol for lightweight RFID based on ECC. J. Sens. 2022 (2022)
Liu, C., Liang, L., Chen, R.: Analysis and research of wireless attack vulnerability based on WPA/WPA2 protocol. Netw. Secur. Technol. Appl. 231(03), 71–72 (2020)
Lounis, K, Zulkernine, M.: Bad-token: denial of service attacks on WPA3. SIN ’19. In: Proceedings of the 12th International Conference on Security of Information and Network, vol. 15, pp. 1–8 (2019)
Kohlios, C.P., Hayajneh, T.: Comprehensive attack flow model and security analysis for Wi-Fi and WPA3. Electron. 7(11), 284 (2018)
Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT press, Cambridge (1999)
Bell Labs. What is spin [EB/OL]. http://spinroot.com/spin/what.html. 1:17 (2019)
Zhong, X., Xiao, M., Li, W.: Formal analysis and improvement of RFID ultra-lightweight authentication protocol RCIA. Comput. Eng. Sci. 40(12), 2183–2192 (2018)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendix a
Appendix a
//Process Initiator proctype PIni(mtype self;mtype party;mtype nonce){ end: do ::atomic{ startflag==0->syn!self,party,nonce,0,counterIni,0; startflag=-1; } ::atomic{ syn?eval(NULL),eval(NULL),eval(NULL),eval(0),ev al(0),eval(0)-> counterIni=counterIni+1; syn!self,party,nonce,0,counterIni,0; } ::atomic{ syn?g1,eval(self),eval(Snonce),eval(0),eval(counterIni ),g2->ResRun(self,g1); PTK=derPTK(0,Anonce,Snonce); MICIni=PTK; PTKA=PTK; PTKS=g2; counterIni=counterIni+1; equal(g2,MICIni)->MICIni=MICIni+1; syn!self,g1,NULL,Encrytion(PTK,5),counterIni,MICI ::atomic{ syn?eval(NULL),eval(NULL),eval(NULL),eval(1),ev al(1),eval(1)-> MICIni=MICIni-1; counterIni=counterIni+1; syn!self,g1,NULL,Encrytion(PTK,5),counterIni,MICI ni; MICIni=MICIni+1; } ni; ResCommit(self,g1); MICIni=MICIni+1; } ::atomic{ syn?eval(NULL),eval(NULL),eval(NULL),eval(2),ev al(2),eval(2)-> counterIni=counterIni+1; MICIni=MICIni+1; syn!self,g1,NULL,Encrytion(PTK,5),counterIni,MICI ni; MICIni=MICIni+1; } ::atomic{ syn?g1,eval(self),eval(NULL),eval(0),eval(counterIni) ,eval(MICIni)-> printf("success"); AuthEnd=1; SecEnd=1; } od; } //Process Responder proctype PRes(mtype self;mtype nonce){ end: do ::atomic{ syn?g3,eval(self),g4,eval(0),g5,eval(0)->counterRes= g5; PTK=derPTK(0,Anonce,Snonce); MICRes=PTK; syn!self,g3,nonce,0,counterRes,MICRes; IniRun(g3,self); counterRes=counterRes+1; MICRes=MICRes+1; } ::atomic{ syn?g3,eval(self),eval(NULL),g5,eval(counterRes),ev al(MICRes)-> IniCommit(g3,self); MICRes=MICRes+1; GTK=g5-PTK; GTKS=GTK; syn!self,g3,NULL,0,counterRes,MICRes; counterRes=counterRes+1; MICRes=MICRes+1; comm ! Encrytion(PTK,6); }
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Xiao, M., Qiao, S., Liu, T., Yang, K., Li, Z., Zhan, D. (2024). Modeling and Verification of WPA3 Security Protocol Based on SPIN. In: Cai, Z., Xiao, M., Zhang, J. (eds) Theoretical Computer Science. NCTCS 2023. Communications in Computer and Information Science, vol 1944. Springer, Singapore. https://doi.org/10.1007/978-981-99-7743-7_16
Download citation
DOI: https://doi.org/10.1007/978-981-99-7743-7_16
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-99-7742-0
Online ISBN: 978-981-99-7743-7
eBook Packages: Computer ScienceComputer Science (R0)