[1]郭显,冯涛,袁占亭,等.用逻辑方法验证移动Ad Hoc网络协议[J].东南大学学报(自然科学版),2011,41(2):258-265.[doi:10.3969/j.issn.1001-0505.2011.02.009]
 Guo Xian,Feng Tao,Yuan Zhanting,et al.Formal modeling and analysis in a logic for mobile Ad Hoc networks[J].Journal of Southeast University (Natural Science Edition),2011,41(2):258-265.[doi:10.3969/j.issn.1001-0505.2011.02.009]
点击复制

用逻辑方法验证移动Ad Hoc网络协议()
分享到:

《东南大学学报(自然科学版)》[ISSN:1001-0505/CN:32-1178/N]

卷:
41
期数:
2011年第2期
页码:
258-265
栏目:
计算机科学与工程
出版日期:
2011-03-20

文章信息/Info

Title:
Formal modeling and analysis in a logic for mobile Ad Hoc networks
作者:
郭显124冯涛23袁占亭12马建峰3
(1兰州理工大学电气工程与信息工程学院, 兰州 730050)
(2兰州理工大学计算机与通信学院, 兰州 730050)
(3西安电子科技大学计算机网络与信息安全教育部重点实验室, 西安 710071)
(4甘肃联合大学电子信息工程学院, 兰州 730010)
Author(s):
Guo Xian124Feng Tao23Yuan Zhanting12Ma Jianfeng3
(1 School of Electrical and Information Engineering, Lanzhou University of Technology, Lanzhou 730050, China)
(2School of Computer and Communication, Lanzhou University of Technology, Lanzhou 730050, China)
(3 Key Laboratory of Computer Networks and Information Security of Ministry of Education, Xidian University, Xian 710071, China)
(4 School of Electronic Information Engineering, Gansu Lianhe University, Lanzhou 730010, China)
关键词:
Ad Hoc网络形式逻辑网络迹移动IP注册协议
Keywords:
Ad Hoc networks logic network trace mobile IP registration protocol
分类号:
TP393
DOI:
10.3969/j.issn.1001-0505.2011.02.009
摘要:
针对移动Ad Hoc网络节点移动和无线广播通信特征, 引入移动算子和广播算子, 扩展形式逻辑LS2, 提出了建模和分析移动Ad Hoc网络安全系统的逻辑ELS2. ELS2把网络模型化为不同位置上执行程序的线程复合, 把攻击者模型化为与协议参与方并发运行的线程. ELS2中提出网络迹概念,描述网络节点内部计算和外部交互, 以及节点移动导致的网络进化过程, 并在网络迹上定义谓词公式和模态公式的语义, 分析网络协议属性. ELS2证明系统中,设计了捕获程序行为直观属性的新公理. 最后, 在ELS2逻辑中建模并分析了移动IP注册协议正确性属性.
Abstract:
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.

参考文献/References:

[1] Datta A,Roy A,Mitchell J.Protocol composition logic (PCL) [J].Electronic Notes in Theoretical Computer Science,2007,172(1):311-358.
[2] Datta A,Franklin J,Garg D,et al.A logic of secure systems and its application to trusted computing [C]//Proceedings of Security and Privacy,IEEE Symposium.Washington DC,2009:221-236.
[3] Pura M L,Patriciu V V,Bica I.Formal verification of secure Ad Hoc routing protocols using AVISPA:ARAN case study [C]//Proceedings of 4th Conference on European Computing Conference.Stevens Point,WI,USA,2010:200-206.
[4] Godskesen J C.A calculus for mobile Ad Hoc networks with static location binding [J].Electronic Notes in Theoretical Computer Science,2009,242(1):161-183.
[5] 李沁,曾庆凯.利用类型推理验证Ad Hoc安全路由协议[J].软件学报,2009,20(10):2822-2833.
  Li Qin,Zeng Qingkai.Verifying mobile Ad-Hoc security routing protocols with type inference [J].Journal of Software,2009,20(10):2822-2833.(in Chinese)
[6] Andel T R.Formal security evaluation of Ad Hoc routing protocols [D].Florida:College of Arts and Sciences,Florida State University,2007.
[7] Yang C Y,Shiu C Y.A secure mobile IP registration protocol [J].International Journal of Network Security,2005,1(1):38-45.
[8] Sufatrio K Y L.Mobile IP registration protocol:a security attack and new secure minimal public-key based authentication [C]// Proceedings of the 1999 International Symposium on Parallel Architectures,Algorithms and Networks.Washington DC,1999:364-369.
[9] Dolev D,Yao A.On the security of public-key protocols [J].IEEE Transactions on Information Theory,1983,29(2):198-208.
[10] 冯涛,郭显,马建峰,等.可证明安全的节点不相交多路径源路由协议[J].软件学报,2010,21(7):1717-1731.
  Feng Tao,Guo Xian,Ma Jianfeng,et al.Provably secure approach for multiple node-disjoint paths source routing protocol [J].Journal of Software, 2010,21(7):1717-1731.(in Chinese)

相似文献/References:

[1]陈晓曙,李霞.一种高效的Ad Hoc网络AODV改进路由协议[J].东南大学学报(自然科学版),2003,33(2):127.[doi:10.3969/j.issn.1001-0505.2003.02.002]
 Chen Xiaoshu,Li Xia.Improved high efficiency AODV routing protocol for Ad Hoc networks[J].Journal of Southeast University (Natural Science Edition),2003,33(2):127.[doi:10.3969/j.issn.1001-0505.2003.02.002]
[2]李密,沈连丰,夏玮玮.Ad Hoc网络中多点对点视频传输系统设计与仿真[J].东南大学学报(自然科学版),2008,38(4):553.[doi:10.3969/j.issn.1001-0505.2008.04.002]
 Li Mi,Shen Lianfeng,Xia Weiwei.Design and simulation of multipoint-to-point video transmission system over Ad Hoc networks[J].Journal of Southeast University (Natural Science Edition),2008,38(2):553.[doi:10.3969/j.issn.1001-0505.2008.04.002]
[3]姚文强,杨哲,朱艳琴,等.Ad hoc网络消息传播过程的高阶描述模型[J].东南大学学报(自然科学版),2015,45(3):428.[doi:10.3969/j.issn.1001-0505.2015.03.003]
 Yao Wenqiang,Yang Zhe,Zhu Yanqin,et al.High-order description model of message propagation process in Ad hoc network[J].Journal of Southeast University (Natural Science Edition),2015,45(2):428.[doi:10.3969/j.issn.1001-0505.2015.03.003]

备注/Memo

备注/Memo:
作者简介:郭显(1971—),男,博士生,讲师;冯涛(联系人),男,博士,教授,fengt@lut.cn.
基金项目:国家高技术研究发展计划(863计划)资助项目(2007AA01Z429)、国家自然科学基金资助项目(60972078)、甘肃省高等学校基本科研业务费资助项目(0914ZTB186)、兰州理工大学博士基金资助项目(BS14200901)、网络安全与密码技术福建省高校重点实验室开放课题资助项目(09A006)、甘肃省自然科学基金资助项目(1014RJZA005).
引文格式: 郭显,冯涛,袁占亭,等.用逻辑方法验证移动Ad Hoc网络协议[J].东南大学学报:自然科学版,2011,41(2):258-265.[doi:10.3969/j.issn.1001-0505.2011.02.009]
更新日期/Last Update: 2011-03-20