基于CSP方法的移动自组织网络认证协议TAM的分析与改进

doi:10.3969/j.issn.1000-436x.2013.z1.008

摘要/Abstract

摘要：

针对移动自组织网络认证协议应对安全威胁、满足安全目标的有效性问题，提出了采用基于通信顺序进程（CSP, communicating sequential process）和模型检测的协议分析方法，对移动自组织网络的代表性认证协议TAM进行分析、建模、检验并改进。首先采用CSP方法对TAM中参与者的通信行为建立模型、给出了安全目标的安全规范；然后利用模型检测工具FDR验证了TAM的CSP进程，结果表明TAM不满足认证性和机密性安全规范；最后对TAM进行了改进并检验，结果表明改进后的TAM满足安全目标，实验表明与TAM相比，改进的TAM在合理的簇规模情况下增加可接受的额外开销。

关键词: 移动自组织网络, 认证协议, 安全协议分析, 通信顺序进程, TAM

Abstract:

Authentication protocols are often adopted to reduce the security threats in mobile ad hoc network(MANET). However, a vulnerable protocol might bring more serious threats to MANET. As a result, formal verifications of security protocols become more important. An approach based on the communicating sequential process (CSP) and Model Checking tool FDR was proposed to model and verify a typical authentication protocol of MANET, callced TAM. First, the communication behaviors of all participants in TAM and its security (authentication and confidentiality) specifications were formally modeled using CSP. Second, based on these models, the participants' behaviors were verified by FDR and the verification result indicates that the original TAM could not guarantee authentication and confidentiality. Finally, an improvement was proposed and the experiment result shows that the improved TAM satisfies security goals and increases an acceptable consumption in the case of a reasonable size of clusters compared with the original TAM.

Key words: MANET, authentication protocols, security protocol analysis, communicating sequential process, TAM

刘礼才,殷丽华,郭云川,孙燕. 基于CSP方法的移动自组织网络认证协议TAM的分析与改进[J]. 通信学报, 2013, 34(Z1): 58-66.

Li-cai LIU,Li-hua YIN,Yun-chuan GUO,Yan SUN. Analysis and improvement for authentication protocols of mobile ad hoc network with CSP approach[J]. Journal on Communications, 2013, 34(Z1): 58-66.

图/表 7

表1

CSP基本规则"

规则	语义	规则	语义
Stop	停止进程	Skip	进程成功终止
P ,Q	顺序组合	μp.F(p)	递归进程
a→b	事件前缀	a→P	进程事件前缀
?x:A→P(x)	事件前缀选择	c ?x:A→P(x)	输入前缀选择
□x :S	集合外部选择	P□Q	进程间的选择
P∏Q	非确定选择	P‖Q	紧接并行
$P_{X} ‖_{Y} Q$	同步并行	$P \underset{Y}{\| \|} Q$	接口并行
P [R]	普通穿插进程重命名	P=F (P)	事件隐藏递归定义

表1

图1

图2

图3

图4

图5

图6

参考文献 26

[1]	LOU W J , FANG Y G . A Survey of Wireless Security in Mobile AdHoc Networks: Challenges and Available Solutions[M]. New York: Kluwer Academic Publishers, 2004.
[2]	YOUNIS M , FARRAG O , ALTHOUSE B . TAM: a tiered authentica-tion of multicast protocol for ad-hoc networks[J]. IEEE Transactions on Network and Service Management, 2012,9 (1):100-113.
[3]	PERKINS C E . Ad Hoc Networking[M]. New York: Addison-Wesley Professional, 2008.
[4]	YANG H , LUO H Y , YE F , et al. Security in mobile ad hoc networks:challenges and solutions[J]. IEEE Wireless Communications, 2004,11 (1):38-47.
[5]	LUO J H , YE D X , XUE L , et al. A survey of multicast routing proto-cols for mobile ad-hoc networks[J]. IEEE Communications Surveys ＆Tutorials, 2009,11 (1):78-91.
[6]	ISLAM N , SHAIKH Z A . Security Issues in Mobile Ad Hoc Net-work[M]. Berlin: Springer Berlin Heidelberg, 2013.49-80
[7]	PERRIG A , CANNETI R , SONG D , et al. The TESLA broadcast authentication protocol[J]. RSA Cryptobytes, 2002,5 (2):2-13.
[8]	STUDER A , BAI F , BELLUR B , et al. Flexible, extensible, and effi-cient VANET authentication[J]. Journal of Communications and Net-works, 2009,11 (6):574-588.
[9]	ZHU S C , XU S H , SETIA S , et al. LHAP: a lightweight hop-by-hop authentication protocol for ad-hoc networks[J]. Ad Hoc Networks, 2006,4 (5):567-585.
[10]	LIN X D , SUN X T , WANG X Y , et al. TSVC: timed efficient and secure vehicular communications with privacy preserving[J]. IEEE Transactions on Wireless Communications, 2008,7 (12):4987-4998.
[11]	BU S R , YU F R , LIU X P , et al. Structural results for combined con-tinuous user authentication and intrusion detection in high security mobile ad-hoc networks[J]. IEEE Transactions on Wireless Commu-nications, 2011,10 (9):3064-3073.
[12]	GUAN Q , YU F , JIANG S , et al. Joint topology control and authenti-cation design in mobile ad hoc networks with cooperative communica-tions[J]. IEEE Transactions on Vehicular Technology, 2012,61 (6):2674-2685.
[13]	GIRUKA V C , SINGHAL M , ROYALTY J , et al. Security in wireless sensor networks[J]. Wirel Commun Mob Comput, 2008,8 (1):1-24.
[14]	CAYIRCI E , RONG C M . Security in Wireless Ad Hoc and Sensor Networks[M]. Hoboken: John Wiley ＆ Sons, 2009.
[15]	BURROWS M , ABADI M , NEEDHAM R M . A logic of authentica-tion[A]. Proceedings of the Royal Society of London Series A Mathe-matical and Physical Sciences[C]. 1989,426(1871):233-271.
[16]	FABREGA F J T , HERZOG J C , GUTTMAN J D . Strand spaces: why is a security protocol correct?[A]. Proceedings of the 1998 IEEE Sympo-sium on Security and Privacy[C]. Oakland, CA, USA, 1998.160-171.
[17]	HOARE C A R . Communicating sequential processes[J]. Commun ACM, 1978,21 (8):666-677.
[18]	LOWE G . Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR[M]. Berlin, Heidelberg: Springer, 1996.147-166.
[19]	LOWE G , ROSCOE B . Using CSP to detect errors in the TMN protocol[J]. IEEE Transactions on Software Engineering, 1997,23 (10):659-669.
[20]	ABADI M , GORDON A D . A calculus for cryptographic protocols:the spi calculus[A]. Proceedings of the 4th ACM Conference on Computer and Communications Security[C]. Zurich, Switzerland, 1997.36-47.
[21]	MEADOWS C . The NRL protocol analyzer: an overview[J]. The Journal of Logic Programming, 1996,26 (2):113-131.
[22]	ROSCOE A W . The Theory and Practice of Concurrency[M]. Upper Saddle River, USA: Prentice-Hall, 2010.
[23]	NEEDHAM R M , SCHROEDER M D . Using encryption for authen-tication in large networks of computers[J]. Commun ACM, 1978,21 (12):993-999.
[24]	LOWE G . Casper: a compiler for the analysis of security protocols[J]. Journal of Computer Security, 1998,6 (1):53-84.
[25]	YACINE C , HATEM B , ABDELMADJID B . A taxonomy of multicast data origin authentication: issues and solutions[J]. IEEE Communica-tions Surveys ＆ Tutorials, 2004,6 (3):34-57.
[26]	DOLEV D , YAO A . On the security of public key protocols[J]. IEEE Transactions on Information Theory, 1983,29 (2):198-208.