用逻辑方法验证移动Ad Hoc网络协议

Formal modeling and analysis in a logic for mobile Ad Hoc networks

针对移动Ad Hoc网络节点移动和无线广播通信特征,引入移动算子和广播算子,扩展形式逻辑LS2,提出了建模和分析移动Ad Hoc网络安全系统的逻辑ELS2.ELS2把网络模型化为不同位置上执行程序的线程复合,把攻击者模型化为与协议参与方并发运行的线程.ELS2中提出网络迹概念,描述网络节点内部计算和外部交互,以及节点移动导致的网络进化过程,并在网络迹上定义谓词公式和模态公式的语义,分析网络协议属性.ELS2证明系统中,设计了捕获程序行为直观属性的新公理.最后,在ELS2逻辑中建模并分析了移动IP注册协议正确性属性.

Aiming at the features of mobility and wireless broadcast communication of node,in order to model and analyze secure systems for mobile Ad Hoc networks,two constructors,i.e.mobility and broadcast,are introduced in LS2（logic of secure systems）.So LS2 is extended to be ELS2.In ELS2,the network is modeled as the combination of threads with different physical locations.A thread is a sequentially executing program.The threads execute programs of secure systems.The attacker is also modeled as a thread which runs concurrently with the threads of system participants.The concept of network trace is proposed in this paper.This concept describes the process of the network evolution caused by system behaviors,such as internal computation,external interaction and mobility of nodes.On the network trace,semantic of predicates and modal formulas are defined,and properties of a system can be analyzed.New axioms are designed in ELS2.Intuitive properties of system behaviors can be captured by these axioms.Finally,in ELS2,mobile IP registration protocol is described and its correctness property is analyzed.