协议组合逻辑安全的Ad Hoc网络路由协议安全验证方法  

Formal Verification of Secure Routing for Ad Hoc Networks Using Protocol Composition Logic

作　　者：郭显[1] 冯涛[1] 袁占亭[1] 

机构地区：[1]兰州理工大学计算机与通信学院,兰州730050

出　　处：《小型微型计算机系统》2013年第12期2794-2799,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(60972078)资助;甘肃省自然科学基金项目(1014RJZA005)资助

摘　　要：扩展协议组合逻辑PCL,提出了建模移动Ad Hoc网络和分析路由协议安全性的符号模型PCL-RP模型.PCL-RP模型中,为模型化网络节点移动和多跳无线广播通信特征,引入了线程位置和线程位置相邻概念,定义了广播规约规则.PCLRP模型中提出了运行迹概念,在运行迹上定义了谓词公式和模态公式的语义.分析协议安全属性时,PCL-RP模型证明系统中的公理和规则保证无需明确推理攻击者的行为,这种方法能够简化分析过程,提高安全分析的可信度.另外,提出了路由协议安全目标,设计了基于动态源路由协议DSR的安全路由协议LSDSR.最后,在PCL-RP模型中描述并分析了LSDSR的安全性,证明LSDSR能够满足安全目标.In this paper, PCL is extended, extended PCL is called PCL-RP. A new method is proposed to model mobile Ad Hoc net- work and analyze the security of routing for this network. In PCL-RP, to model nodes mobile and wireless radio communication fea- tures in mobile Ad Hoc network, location of thread is introduced and the rule of broadcasting is defined. The concept of network trace is proposed in this paper. Semantic of predicates and modal formulas are defined on the network trace. Axioms and rules in PCL-RP ensure that security properties of protocol are analyzed without explicitly reasoning about the attacker behavior. This approach can simplify the analysis process, and improve the reliability of safety analysis. In addition, new security objective of routing for mobile Ad Hoc network is proposed, and a secure routing protocol LSDSR based on DSR is designed in this paper. Finally, in PCL-RP, LS- DSR is described and its security is verified. It is proved that LSDSR can meet new security objective.

关 键 词：移动AD HOC网络 协议组合逻辑 安全路由协议 动态源路由协议 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]