首页 | 本学科首页   官方微博 | 高级检索  
     

基于Authentication Test方法的高效安全IKE形式化设计研究
引用本文:蒋睿,胡爱群,李建华.基于Authentication Test方法的高效安全IKE形式化设计研究[J].计算机学报,2006,29(9):1694-1701.
作者姓名:蒋睿  胡爱群  李建华
作者单位:1. 东南大学无线电工程系,南京,210096
2. 上海交通大学电子工程系,上海,200030
基金项目:国家高技术研究发展计划(863计划);国家115科研基金
摘    要:基于Authentication Test方法,围绕高效安全Internet密钥交换(ESIKE)协议的安全目标,提出一种具体地构建唯一满足两个通信实体变换边的形式化协议设计方法,设计出了高效安全的IKE协议;并且基于Strand Space模型和Authentication Test方法,形式化分析ESIKE协议,证明了其所具有的安全特性.该ESIKE协议克服了原有Internet密钥交换(IKE)协议存在的安全缺陷,提供了安全的会话密钥及安全关联(SA)协商,保护了通信端点的身份,并且保证了协议发起者和响应者间的双向认证.同时,ESIKE仅需3条消息及更少的计算量,更加简单、高效.

关 键 词:协议设计  形式化方法  密钥交换  Strand  space模型
收稿时间:2005-12-10
修稿时间:2005-12-102006-06-01

Research on Formal Design of ESIKE Based on Authentication Tests
JIANG Rui,HU Ai-un,LI Jian-Hua.Research on Formal Design of ESIKE Based on Authentication Tests[J].Chinese Journal of Computers,2006,29(9):1694-1701.
Authors:JIANG Rui  HU Ai-un  LI Jian-Hua
Affiliation:1. Department of Radio Engineering, Southeast University, Nanjing 210096; 2. Department of Electronic Engineering, Shanghai Jiaotong University, Shanghai 200030
Abstract: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.
Keywords:Authentication tests
本文献已被 CNKI 维普 万方数据 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号