基于扩展Spi演算的IKEv2协议形式化分析与改进  

Formal Analysis and Improvement of IKEv2 Protocol Based on Extended Spi Calculus

作　　者：韩明奎[1] 潘进[1] 刘琼[1] 李波[1] 

机构地区：[1]西安通信学院,陕西西安710106

出　　处：《计算机技术与发展》2010年第8期154-158,共5页Computer Technology and Development

基　　金：国家"863"计划资助项目(2007AA01Z472)

摘　　要：安全性是新一代密钥交换协议的关键,而Spi演算是研究协议安全性的一种形式化方法,文中采用Spi演算研究了IKEv2协议的安全属性。针对Spi演算不能形式化定义Diffie-Hellman密钥交换和密钥生成的问题,扩展了Spi演算的语法和语义。基于扩展的Spi演算形式化分析了IKEv2协议,分析结果表明协议满足认证性和私密性,但不能保护相对重要的发起方身份。针对IKEv2协议的不足,提出了一种基于Weil对签名算法的改进方案。改进后的协议解决了发起方身份保护问题,具有更好的安全性。Since security is important for the new Internet Key Exchange protocol,and Spi calculus can be used to formal analysis protocol＇s security,the paper has studied IKEv2 based on Spi calculus.Firstly,as Spi couldn＇t define the Diffie-Hellman key exchanging and key creating during the process of modeling IKEv2 protocol,authors extended Spi calculus＇ syntax and semantic.Secondly,IKEv2 protocol has been analyzed based on the extended Spi calculus,and analysis results indicated IKEv2 protocol satisfied authentication and security,but couldn＇t protect initiator＇s identity.At last,an improved protocol has been presented based on Weil pairing＇s signature method.The new protocol has a better performance in protecting initiator＇s identity and secure.

关 键 词：IKEV2协议 SPI演算 DIFFIE-HELLMAN密钥交换 身份保护 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]