MANET路由协议的正确性分析

• 作者: 张兴元 杨华兵 王元元
• 来源期刊: 南京邮电大学学报（自然科学版）
• 学科: 工学
• 关键词: MANET 路由协议 形式验证 正确性
• 年，卷（期）: 2007,（2）
• 所属期刊栏目: 首届江苏省青年科学家年会通信与信息技术分会优秀论文专栏
• 页码范围: 15-19
• 页数: 5页
• 分类号: TP393.08
• 字数: 4164字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-5439.2007.02.004

摘要

移动自组网(MANET)是当前网络研究的一个热点,但是由于安全问题致使其未能广泛应用.在安全问题中,路由协议的正确性尤为重要.采用形式验证方法分析了MANET非安全路由协议和安全路由协议的正确性.首先给出了协议正确性的形式描述以及攻击者的形式定义,将协议的正确性分为安全性(Safety property)和活性(Liveness property),前者指协议所发现的路由具有某些良好的性质,后者指协议能够发现路由而且能够顺利地传输数据;然后提出了两个活性证明规则--响应性证明规则和反应性证明规则,并用所提出的活性证明规则在Isabelle/HOL中证明了DSR协议和SRP协议的正确性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王元元	解放军理工大学指挥自动化学院	46	351	12.0	16.0
2	张兴元	解放军理工大学指挥自动化学院	14	20	2.0	3.0
3	杨华兵	解放军理工大学指挥自动化学院	6	16	3.0	3.0