基于Petri网的无线Mesh网虫洞攻击检测及形式化验证

发布时间：2018-03-05 02:26

本文选题：无线Mesh网　切入点：路由协议　出处：《哈尔滨工业大学》2014年硕士论文　论文类型：学位论文

【摘要】：无线Mesh网(Wireless Mesh Networks,WMNs)是一种具有动态网络拓扑、自组织、自配置的新型无线网络,能够提供大容量、网络覆盖范围广、易接入、高速率的网络服务,已经应用到许多领域。但是由于WMN的分布式网络结构、共享无线信道等特点,很容易受到各种安全攻击,影响网络性能与正常工作。其中路由攻击是威胁WMN网络安全的重要方面,路由安全是网络安全的前提,是解决网络安全问题关键之一。本文研究了WMN路由协议的工作机制与存在的路由安全攻击,主要分析研究了混合无线Mesh协议(Hybrid Wireless Mesh Protocol,HWMP)存在的虫洞攻击及现有抵抗虫洞攻击的安全路由方案,提出并设计了基于单程时间检测机制(Single-trip Time Detection Mechanism,STDM)的安全路由方案。在该方案中,中间节点与目的节点都参与检测,并且中间节点能够在检测到攻击之后隔离假邻居。与基于往返时间方案相比,STDM在目的节点发送路径响应之前就能够检测出是否存在虫洞攻击,缩短了检测时间。安全协议形式化验证技术,可以用来消除无线网络安全协议的缺陷,为协议的安全性提供了理论依据。Petri网是其中一类重要的形式化验证方法,兼具严密的数学理论基础与可自动化验证的优点。本文采用时间着色Petri网(Timed Colored Petri Net,TCPN)分别对WMN虫洞攻击与基于STDM的虫洞攻击检测机制进行形式化建模与验证,通过运行模拟实验得到上述Petri网模型的状态空间,然后分析Petri网有界性、计算状态空间生成树、搜索攻击状态是否可达等,验证了STDM机制的有效性。
[Abstract]:Wireless Mesh Networks Wireless Mesh Networks (WMNs) is a new wireless network with dynamic network topology, self-organization and self-configuration, which can provide large capacity, wide network coverage, easy access and high speed network services. It has been applied to many fields. However, due to the characteristics of distributed network structure and shared wireless channel of WMN, it is vulnerable to various kinds of security attacks. Routing attack is an important aspect that threatens the security of WMN network, and routing security is the premise of network security. This paper studies the working mechanism of WMN routing protocol and the existing routing security attacks. This paper mainly analyzes and studies the wormhole attack existing in Hybrid Wireless Mesh Protocol (HWMP) and the existing secure routing scheme against wormhole attack, and proposes and designs a secure routing scheme based on Single-trip Time Detection MechanismSTDM, which is based on one-way time detection mechanism. Both the intermediate node and the destination node are involved in the detection, and the intermediate node can isolate the false neighbor after detecting the attack. Compared with the round-trip time scheme, STDM can detect whether the wormhole attack exists before the destination node sends the path response. The technology of formal verification of security protocols can be used to eliminate the defects of wireless network security protocols and provide a theoretical basis for the security of protocols. Petri net is one of the most important formal verification methods. In this paper, the time-colored Petri net is used to model and verify the WMN wormhole attack and the STDM based wormhole attack detection mechanism, respectively. The state space of the above Petri net model is obtained by running the simulation experiment, then the boundedness of the Petri net is analyzed, the state space spanning tree is calculated, and the attack state is searched. The validity of the STDM mechanism is verified.
【学位授予单位】：哈尔滨工业大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TN915.08

【相似文献】