[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网络协议() 分享到： var jiathis_config = { data_track_clickback: true };

41

2011年第2期

258-265

2011-03-20

文章信息/Info

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

(1兰州理工大学电气工程与信息工程学院, 兰州 730050)
(2兰州理工大学计算机与通信学院, 兰州 730050)
(3西安电子科技大学计算机网络与信息安全教育部重点实验室, 西安 710071)
(4甘肃联合大学电子信息工程学院, 兰州 730010)
Author(s):
(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)

Keywords:

TP393
DOI:
10.3969/j.issn.1001-0505.2011.02.009

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.
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)