文档介绍：硕士学位论文
基于颜色 Petri 网的无线 Mesh 网路由安全
建模与验证
THE MODELING AND VERIFICATION
OF SECURITY ROUTING IN WIRELESS
WORK BASED ON
COLOURED
周强
哈尔滨工业大学
2011 年 12 月
国内图书分类号: 学校代码:10213
国际图书分类号: 密级:公开
工学硕士学位论文
基于颜色 Petri 网的无线 Mesh 网路由安全
建模与验证
硕士研究:周强
导师:黄荷姣教授
生
申请学位:工学硕士
学科:计算机科学与技术
所在单位:深圳研究生院
答辩日期:20 11 年 12 月
授予学位:哈尔滨工业大学
单位
Classified Index:
:
Thesis for the Master Degree in Engineering
THE MODELING AND VERIFICATION
OF SECURITY ROUTING IN WIRELESS
WORK BASED ON
COLOURED
Candidate: Qiang Zhou
Supervisor: Prof. Hejiao Huang
Academic Degree Applied for: Master of Engineering
Speciality: Computer Science & Technology
Affiliation: Shenzhen Graduate School
Date of Defence: December, 2011
Degree-Conferring-Institution: Harbin Institute of Technology
哈尔滨工业大学工学硕士学位论文
摘要
随着 3G 网络与无线局域网的普及,无线网络通信技术已经在我们的日常
生活中无处不在了。无线 Mesh 网(Wireless work)简称 WMN 作为一种
新型的无线网络,由于其自组织,自适应,成本低,多跳,与其他网络兼容好
等特点逐渐成为下一代无线通信的核心技术。尽管现在的无线网络中有很多安
全机制来保障网络安全,但由于无线 Mesh 网自身的特点,这些安全机制不能
完全地应用到无线 Mesh 网中。路由安全是无线 Mesh 网安全的一个重要方面,
网络的安全传输,离不开路由协议的安全保障,恶意节点通过攻击路由协议,
假冒正常的节点并且插入伪造路由信息来攻击网络,一旦路由协议受到攻击,
其余的安全措施都变得毫无意义。
安全协议的形式化验证方法是指用数学或者逻辑模型对所建立的模型进行
分析验证,从而在理论上证明其安全性。颜色 Petri 网是一种图形化的建模语言,
采用颜色 Petri 网对安全问题进行建模分析具有很多独特的优点。比如,颜色
Petri 网有自动化分析工具如 CPN Tool;可以采用状态空间分析和关联矩阵分析;
用颜色 Petri 网建模可以有效地验证安全协议的安全性,颜色 Petri 网不但可以
检测出模型中存在攻击,当安全协议中没有攻击时,颜色 Petri 网可以有效地证
明其安全性。因此研究基于颜色 Petri 网的无线 Mesh 网安全协议建模和验证具
有重要的理论意义和应用价值。
本文通过分析研究现有无线 Mesh 网路由协议的运行机制和各种形式化验
证方法,首次提出了用颜色 Petri 网对无线 Mesh 网路由协议 HWMP 进行建模
和安全验证。通过对 HWMP 路由协议进行建模分析,Petri 网模型可以有效地
模拟仿真 HWMP 路由协议按需路由建立过程。用状态空间方法和 CPN Tool 仿
真实验分析该模型,可以证明该模型中是否存在黑洞攻击。对于存在黑洞攻击
的模型,通过研究现有的基于密码机制的安全路由方案和基于信任和检测机制
的安全路由方案,本文提出了一种基于公开密钥加密机制的安全路由算法,用
NS2 对基于公开密钥机制的安全方案进行仿真实验,实验结果说明该安全方案
可以有效地防止黑洞攻击对网络造成的影响。用颜色 Petri 网对该安全路由算法
重新建模分析,通过状态空间方法和 CPN