Ad Hoc网络安全路由协议形式化分析模型  

Formal analysis model of secure routing protocols for Ad Hoc networks

作　　者：刘晶[1] 伏飞[2] 肖军模[1] 

机构地区：[1]解放军理工大学通信工程学院 [2]解放军理工大学指挥自动化学院,江苏南京210007

出　　处：《解放军理工大学学报（自然科学版）》2008年第3期215-221,共7页Journal of PLA University of Science and Technology(Natural Science Edition)

基　　金：国家自然科学基金资助项目(69931040);国家部委预研基金资助项目(41101040402)

摘　　要：为了能够对Ad Hoc网络安全路由协议进行有效的安全性证明,需要形式化的分析方法。针对目前缺乏有效方法的现状,结合Ad Hoc网络安全路由协议特点,利用图论理论,对传统安全协议分析方法Mead-ows模型进行扩展,扩展后的Meadows模型具有了路由描述和分析能力。使用扩展后的Meadows模型对AdHoc网络安全路由协议Ariadne进行了分析。分析结果显示,Ariadne协议存在产生虚假路由的漏洞,从而也说明了扩展后的Meadows模型能够用于Ad Hoc网络安全路由协议的安全性分析。Many secure routing protocols for Ad Hoc networks have been proposed by far, but few formal analysis methods for them have been provided. Meadows model is a famous cryptographic analysis method. But it is unfit for Ad Hoc network secure routing protocols, since it lacks the ability to describe and analyze the routing. By adding routing description and analysis scheme based on graphic theory, the analysis ability of Meadows model was extended, which could analyze the secure routing protocols for Ad Hoc networks. As an example, the extended model was used to analyze the routing protocol, Ariadne, and the analysis result shows that Ariadne can generate fault routing.

关 键 词：AD HOC网络 安全路由协议 形式化分析 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]