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

Analysis and improvement for authentication protocols of mobile ad hoc network with CSP approach

作　　者：刘礼才[1,2] 殷丽华[2] 郭云川[2] 孙燕[1,2] 

机构地区：[1]北京邮电大学计算机学院,北京100876 [2]中国科学院信息工程研究所,北京100195

出　　处：《通信学报》2013年第S1期58-66,共9页Journal on Communications

基　　金：国家自然科学基金资助项目(61100181;61070186;61100186)~~

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

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

分 类 号：TN929.5[电子电信—通信与信息系统] TN915.04[电子电信—信息与通信工程]