PAT Based WSNs Security Protocol Research

With the application of Wireless Sensor Networks(WSNs),WSNs becoming more and more popular,and WSNs security protocols have become a hotspot.Due to the protocol development process,complex protocol flow and application scenarios may lead to protocol description of the emergence of logic vulnerabilities,or the existence of the agreement itself is often to provide the possibility of attack for attackers.Therefore,in order to analyze the security of the protocol and reduce the risk of being attack,it is hot to apply the formal method and the model checking technology to the research and analysis of WSNs security protocol.WSNs clustering protocol makes it difficult for defense nodes to attack because of the different role of nodes in the network and the complicated communication flow.ORLEACH protocol is based on LEACH(Low energy adaptive clustering Hierachy)clustering routing protocol,added the intrusion detection mechanism and other security mechanisms of the protocol.In order to verify the security of ORLEACH protocol,this paper uses the model checking tool PAT(Process Analysis Toolkit)to model and verify.First of all,the PAT function library is expanded,new data structures and functions are added,and then the security attributes represented by LTL formula are verified,such as confidentiality,integrity and authentication.Finally,according to the shortcomings of ORLEACH protocol,Improved the protocol.The main contributions of this paper are as follows:(1)To extend the PAT library,adding new data structures and functions.WSNode library is the abstraction of all the attributes of the node;Key key function library includes a series of encryption operations and decryption operations;for the ORLEACHLIB library includes the pre-distribution stage key pool generation,key ring allocation and other operations.The WSNode library and the Key key library are common libraries for clustering security protocol modeling and can be used to model other WSNs clustering security protocols.(2)Establishment of node behavior model and attack model for ORLEACH clustering protocol.Based on the extended PAT function library,the input model of CSP # language is established for the cluster head node,monitoring node,member node and base station in the protocol,and then the black hole attack and tampering are established for the protocol establishment and data transmission phase Attack model,and the establishment of comprehensive attack model for protocol neighbor node authentication phase;(3)Verify the ORLEACH protocol using PAT.On the basis of protocol modeling,the PAT tool is used to verify the confidentiality and integrity of the message.The result is that the ORLEACH protocol realizes the confidentiality of the data and ensures that the external attack node can not break the contents even if it can steal the packet.ORLEACH The protocol can detect the node that implements the black hole attack and isolate it.However,it can not guarantee the integrity of the message if the node that has implemented the tamper attack can not guarantee the integrity of the message.In addition,when the neighbor node is authenticated at the time of the shared key discovery phase,The results show that the intervention of the attack node can make the non-neighbor node complete the authentication.(4)Improved ORLEACH protocol.According to the counter example given in the PAT verification result,the proposed improvement scheme includes the following steps: when the node sends data,it sends a data obtained by MAC operation of the packet using the key K shared with the receiving node Message authentication code to ensure the integrity of the message;the use of timestamps.When the node performs broadcast authentication,it sends a timestamp of the current time and realizes bidirectional authentication between neighbor nodes.