Petri Net Based Detection And Formal Verification Of Wormhole Attack In Wireless Mesh Network

Wireless Mesh Network(WMN) is a type of wireless networks characterized by dynamic network topology, self-organizing and self-configuring. WMN has been applied to many fields since it provides network services of high capacity, wide network coverage, easy to access and high speed. However, due to the intrinsic characteristics such as distributed network architecture and shared radio channel, WMN is vulnerable to various security attacks that affect the performance and normal operation of network. Among the security attacks, routing attack is an important aspect of threat to WMN network security. Routing security is a prerequisite for network security, and it is one of the keys to solve problems of network security.The thesis researches the working mechanism of WMN routing protocols and existing routing security attacks, mainly analyzes the wormhole attack in Hybrid Wireless Mesh Protocol(HWMP) and off-the-shelf secure routing solutions against wormhole attack. Then a secure routing solution called Single-trip Time Detection Mechanism(STDM) is proposed and designed. In this mechanism, both the intermediate and destination nodes are involved in the detection, and the intermediate nodes are capable of isolating fake neighbors after the attack is detected. Compared with the solutions based on Round-Trip Time(RTT), STDM is able to detect the presence of wormhole attack before the sending of response generated by the destination node, thus shortens the detection time.Formal verification techniques of security protocols can be used to eliminate the deficiencies of security protocols in wireless network. They provide a theoretical basis for security of protocols. Petri net is one of the important classes of formal verification methods, and has the advantages of rigorous mathematical foundation and automated verification. In this thesis, the Timed Colored Petri Net(TCPN) is applied to respectively formally model and verify wormhole attack in WMN and wormhole defense mechanism STDM. Running simulation experiment, we get the state spaces of the above Petri net models. Then the effectiveness of STDM is verified by analyzing the boundedness of Petri nets, computing the spanning tree of state space, and searching to see whether attacking states are reachable, etc.