Verifying mobile ad-hoc security routing protocols with type inference

被引：1
作者：
Li, Qin [1 ,2 ]
Zeng, Qing-Kai [1 ,2 ]
机构：
[1] State Key Laboratory for Novel Software Technology, Nanjing University
[2] Department of Computer Science and Technology, Nanjing University
来源：
Ruan Jian Xue Bao/Journal of Software | 2009年 / 20卷 / 10期
关键词：
Ad-hoc protocol; Security routing protocol; Type inference; Verification of security protocol;
D O I：
10.3724/SP.J.1001.2009.03504
中图分类号：
学科分类号：
摘要：
A type-inference-based formal method is proposed for verifying an ad-hoc security routing protocol in this paper. A calculus, called NCCC (neighborhood-constraint communication calculus), is defined to specify the protocol. The security property of the protocol is described with typing rules in a type system. Based on the Dolev-Yao model, an attacker model, called the message set of protocol format, is refined. At last, the simplified version of SAODV (secure ad hoc on-demand routing protocol) is verified with this method. With the type-inference-based formal method, not only is the security of protocols verified, but also the attacke examples are predicted. The complexity of inference is reduced significantly for refining the message set of protocol. © by Institute of Software, the Chinese Academy of Sciences. All rights reserved.
引用
收藏
页码：2822 / 2833
页数：11
相关论文
共 25 条
  • [1] Papadimitratos P., Haas Z.J., Secure routing for mobile ad hoc networks, Proc. of the SCS Communication Networks and Distributed Systems Modeling and Simulation Conf, (2002)
  • [2] Pfitzmann B., Waidner M., A model for asynchronous reactive systems and its application to secure message transmission, Proc. of the IEEE Symp. on Security and Privacy. IEEE, pp. 184-200, (2001)
  • [3] Zapata M.G., Asokan N., Securing ad hoc routing protocols, Proc. of the ACM Workshop on Wireless Security, pp. 1-10, (2002)
  • [4] Hu Y.C., Perrig A., Johnson D., Ariadne: A secure on-demand routing prortocol for ad hoc networks, Wireless Networks, 11, 1-2, pp. 21-38, (2005)
  • [5] Qing S.H., Design and logic analysis of security protocols, Journal of Software, 14, 7, pp. 1300-1309, (2003)
  • [6] Zakiuddin I., Goldsmith M., Whittaker P., Gardiner P., A methodology for mode-checking ad-hoc networks, (2003)
  • [7] Nanz S., Hankin C., A framework for security analysis of mobile wireless networks, Theoretical Computer Science, 367, 1, pp. 203-227, (2006)
  • [8] Dolev D., Yao A.C., On the security of public key protocols, IEEE Trans. on Information Theory, 29, 2, pp. 198-208, (1983)
  • [9] Cardelli L., Gordon A.D., Mobile ambients, Theoretical Computer Science, 240, 1, pp. 177-213, (2000)
  • [10] Castagna G., Vitek J., Nardelli F.Z., The seal calculus, Information and Computation, 201, 1, pp. 1-54, (2005)
123