Formal Analysis And Improvement Of Z-wave Protocol For Intelligent Home System

Smart home is a highly intelligent ecosystem,which uses the Internet of Things technology to realize the effective integration of a variety of smart devices,which not only improves the quality of family life,but also brings security and privacy issues to homeowners.The Internet of Things communication protocol is the core of realizing smart home.The Internet of Things communication protocols used include BLE,Zig Bee,Z-Wave,etc.,among which Z-Wave protocol is widely used in smart home communication,and its security is crucial to the reliability of smart home system.Currently,the majority of studies on the security of Z-Wave protocol concentrate on the security of its operational purpose,while few have conducted formal analysis and confirmation.Such verification can effectively identify any potential flaws in the protocol.Such verification can effectively detect the possible vulnerabilities of the protocol.This paper takes Z-Wave protocol as the research object,uses CPN formalized analysis method and Dolev-Yao attack model to discuss the security characteristics of Z-Wave protocol in detail,so as to verify its possible security vulnerabilities.The experimental results show that Z-Wave S0 and S2 have network key leakage and man-in-the-middle attack respectively.Finally,according to the evaluation results,an effective improvement scheme based on HKDF algorithm is proposed,and the security of the improved protocol is verified,so that Z-Wave protocol is more secure,and provides strong guidance and support for the future security research of smart home system.The main contributions and innovations of this paper include:1.Through in-depth analysis of the process of Z-Wave network including new devices,study the security mechanism used in the process,and establish the message flow model based on Z-Wave protocol.Then,based on the formal analysis theory of colored Petri nets,the net entry processes of security frameworks S0 and S2 are simulated respectively.Firstly,based on the protocol message flow model,the modeling hypothesis of Z-Wave protocol is proposed.Secondly,the two-layer initial HCPN model of S0 and S2 protocol is constructed by using hierarchical modeling technology,and its operation process is described in detail.Finally,the state space module of CPN Tools was processed to generate detailed state space report,and the function in ASK-CTL library was used to analyze the state space path and verify the consistency of the protocol specification.2.In view of the security requirements of Z-Wave protocol,this course reassumes the attack capability of Delov-Yao attacker,and adds the attacker model into the initial HCPN model of the protocol to build a formal security evaluation model of the protocol.Then,the model space status report and the SML query function provided by ASKCTL library are used to verify the existence of security attribute violation events and possible vulnerabilities in the model.The experimental results show that Z-Wave S0 and S2 have security vulnerabilities of network key leakage and man-in-the-middle attack respectively.3.Aiming at the man-in-the-middle attack in Z-Wave S2 protocol and combining the knowledge of cryptography and network security,we propose a bidirectional authentication scheme for resource-constrained devices.The scheme uses HKDF function and XOR operation to enhance the confidentiality and authentication of the protocol,thus greatly improving the security level of the protocol.Then,the security of the improved scheme is evaluated by introducing Dolev-Yao attacker model.The results show that this improved scheme can effectively resist the man-in-the-middle attack and improve the security of the system.