Formal Modeling And Analysis Of Wireless Sensor Network Security Protocols

With the extensively use of Wireless Sensor Networks (WSN), WSN security issues have become increasingly prominent. WSN security protocol design has been one of the critical technologies. Therefore, the application of formal methods to WSN security protocol modeling and analysis becomes a hot research topic in the current.Since Dolev and Yao proposed to apply model checking techniques to the analysis and verification of security protocol, model checking has become an important formal method to verify security protocols, and achieved great success. The widely impact model checking tools include SPIN, SMV, UPPAAL, PAT etc. Using tools such as SPIN, model checking has been constantly studied to be applied to the formal analysis of new security protocols. For wireless sensor networks, many scholars have conducted research based on model checking to WSN security protocol modeling and analysis.The thesis concentrates on model checking technology and its application on formal modeling and analysis of WSN security protocols, based on the research of WSN security issues and protocols. This thesis overview the basic characteristic of the existing security protocol modeling language, point out that it can not be used for formal modeling WSN security protocols directly, and propose solutions. First, this thesis propose a Linear Temporal Logic (LTL) description method to characterize properties, and a process-algebra-based WSN security protocol formalized modeling language framework, to facilitate the experts in the field of WSN to describe behavior and properties of WSN security protocol rapidly and accurately. Then, this thesis proposes an SPIN-based formal methods application framework for WSN security protocol analysis and improvement, and give concrete case. This framework can help designers design and improve WSN security protocols through iteratively applying model checking to this Process. Finally, the thesis develop a WSNNode module for WSN security protocol modeling and analysis based on NUS Process Analysis Toolkit (PAT), and illustrate its effectiveness and correctness in WSN security protocol analysis through case study.