| MANET路由协议的正确性分析 |
| |
| 引用本文： | 杨华兵,张兴元,王元元.MANET路由协议的正确性分析[J].南京邮电大学学报(自然科学版),2007,27(2):15-19. |
| |
| 作者姓名： | 杨华兵 张兴元 王元元 |
| |
| 作者单位： | 解放军理工大学,指挥自动化学院,江苏,南京,210007 |
| |
| 摘 要： | 移动自组网(MANET)是当前网络研究的一个热点,但是由于安全问题致使其未能广泛应用.在安全问题中,路由协议的正确性尤为重要.采用形式验证方法分析了MANET非安全路由协议和安全路由协议的正确性.首先给出了协议正确性的形式描述以及攻击者的形式定义,将协议的正确性分为安全性(Safety property)和活性(Liveness property),前者指协议所发现的路由具有某些良好的性质,后者指协议能够发现路由而且能够顺利地传输数据;然后提出了两个活性证明规则--响应性证明规则和反应性证明规则,并用所提出的活性证明规则在Isabelle/HOL中证明了DSR协议和SRP协议的正确性.
|
| 关 键 词： | MANET 路由协议 形式验证 正确性 MANET 路由协议 正确性分析 Routing Protocols Analysis 反应性 响应性 证明规则 传输数据 性质 发现 Liveness 活性 Safety property 安全性 形式定义 攻击者 形式描述 非安全 |
| 文章编号： | 1673-5439（2007）02-0015-05 |
| 收稿时间： | 2006-08-12 |
| 修稿时间： | 2006年8月12日 |
Correctness Analysis of MANET Routing Protocols |
| |
| YANG Hua-bing,ZHANG Xing-yuan,WANG Yuan-yuan.Correctness Analysis of MANET Routing Protocols[J].Journal of Nanjing University of Posts and Telecommunications,2007,27(2):15-19. |
| |
| Authors: | YANG Hua-bing ZHANG Xing-yuan WANG Yuan-yuan |
| |
| Institution: | Institute of Command Automation, PLA University of Science and Technology, Nanjing 210007, China |
| |
| Abstract: | MANET is one of the hot topics of network research.However,MANET has not been applied widely due to security issues,of which the most important is the correctness of routing protocols.This paper focuses on the formal verification of MANET non-secure and secure routing protocols.Firstly,the formal definition of the correctness of routing protocols and the formal definition of attackers are given.The proved correctness of the routing protocol consists of two parts: safety properties and liveness properties.The former requires that the discovered route(s) should have some desired characters,while the latter requirse that the route(s) should be discovered and data be transmitted successfully.Secondly,two liveness proof rules,response property proof rule and reactivity property proof rule,are devised.The correctness of DSR and SRP protocols are proved in Isabelle/HOL using these two rules. |
| |
| Keywords: | mobile Ad hoe network routing protocol formal verification correctness |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
