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

摘要

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

目录

封面

中文摘要

英文摘要

目录

第1章 绪 论

1.1 课题来源

1.2 课题背景和研究意义

1.3 国内外研究现状

1.4 本文的主要内容

1.5 本文的组织结构

第2章 无线Mesh网路由安全与Petri网理论

2.1 无线Mesh网路由协议与安全攻击

2.2 Petri网理论

2.3 本章小结

第3章 虫洞攻击检测与避免及Petri网建模

3.1 虫洞攻击

3.2 虫洞攻击的安全路由方案

3.3 STDM虫洞攻击检测机制设计

3.4 虫洞攻击的TCPN模型

3.5 基于STDM安全路由机制的TCPN模型

3.6 本章小结

第4章 模拟实验结果与分析

4.1 Petri网仿真实验工具CPN Tools介绍

4.2 虫洞攻击的TCPN模型实验结果

4.3 基于STDM的TCPN模型实验结果

4.4 本章小结

结论

参考文献

攻读硕士学位期间发表的论文及其它成果

声明

致谢