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

• 作者: 冯涛 袁占亭 郭显 马建峰
• 来源期刊: 东南大学学报（自然科学版）
• 学科: 工学
• 关键词: Ad Hoc网络 形式逻辑 网络迹 移动IP注册协议
• 年，卷（期）: 2011,（2）
• 页码范围: 258-265
• 分类号: TP393
• 字数: 7767字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-0505.2011.02.009

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	马建峰	西安电子科技大学计算机网络与信息安全教育部重点实验室	389	4956	30.0	50.0
2	袁占亭	兰州理工大学电气工程与信息工程学院	84	771	14.0	25.0
6	冯涛	兰州理工大学计算机与通信学院	33	352	13.0	17.0
10	郭显	兰州理工大学电气工程与信息工程学院	13	50	4.0	6.0