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

摘要：

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

关键词： Ad Hoc网络 形式逻辑 网络迹 移动IP注册协议

作者: 郭显 冯涛 袁占亭 马建峰

作者单位: 兰州理工大学电气工程与信息工程学院, 兰州 730050 兰州理工大学计算机与通信学院, 兰州 730050 甘肃联合大学电子信息工程学院,兰州 730010 兰州理工大学计算机与通信学院, 兰州 730050 西安电子科技大学计算机网络与信息安全教育部重点实验室, 西安 710071 兰州理工大学电气工程与信息工程学院, 兰州 730050 兰州理工大学计算机与通信学院, 兰州 730050 西安电子科技大学计算机网络与信息安全教育部重点实验室, 西安 710071

会议类型: 国内会议

会议名称: 第七届全国计算机支持的协同工作学术会议暨第五届全国智能信息网络学术会议

会议地点: 南京

会议语种:中文

页码: 1-8

在线出版日期: 2010-11-26（万方平台首次上网日期，不代表论文的发表时间）