无线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机制的有效性。