基于Authentication Test方法的高效安全IKE形式化设计研究  

Research on Formal Design of ESIKE Based on Authentication Tests

作　　者：蒋睿 胡爱群[1] 李建华[2] 

机构地区：[1]东南大学无线电工程系,南京210096 [2]上海交通大学电子工程系,上海200030

出　　处：《计算机学报》2006年第9期1694-1701,共8页Chinese Journal of Computers

基　　金：国家"八六三"高技术研究发展计划项目基金(2003AA142160)资助;国家115科研基金(P2006014EA)资助.

摘　　要：基于Authentication Test方法,围绕高效安全Internet密钥交换(ESIKE)协议的安全目标,提出一种具体地构建唯一满足两个通信实体变换边的形式化协议设计方法,设计出了高效安全的IKE协议;并且基于StrandSpace模型和Authentication Test方法,形式化分析ESIKE协议,证明了其所具有的安全特性.该ESIKE协议克服了原有Internet密钥交换(IKE)协议存在的安全缺陷,提供了安全的会话密钥及安全关联(SA)协商,保护了通信端点的身份,并且保证了协议发起者和响应者间的双向认证.同时,ESIKE仅需3条消息及更少的计算量,更加简单、高效.Based on the authentication tests, this paper presents a concrete formal protocol design approach, which constructs the only transforming edge between the two communication entities, to create an Efficient and Secure Internet Key Exchange （ESIKE） protocol according to the security goals of the ESIKE protocol. Then the secure properties of ESIKE are formally proved with the strand space model and the authentication tests. The ESIKE protocol overcomes the security shortages of the Internet Key Exchange （IKE）, and can provide secure negotiation of session key and Security Association （SA）, protection of endpoints＇ identities, and mutual authentication between the initiator and the responder. It needs only three messages and less computational load, and it is simple and efficient.

关 键 词：协议设计 形式化方法 AUTHENTICATION TESTS 密钥交换Strand space模型 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]