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

基于Authentication Test方法，围绕高效安全Internet密钥交换（ESIKE）协议的安全目标，提出一种具体地构建唯一满足两个通信实体变换边的形式化协议设计方法，设计出了高效安全的IKE协议；并且基于Strand Space模型和Authentication Test方法，形式化分析ESIKE协议，证明了其所具有的安全特性．该ESIKE协议克服了原有Internet密钥交换（IKE）协议存在的安全缺陷，提供了安全的会话密钥及安全关联（SA）协商，保护了通信端点的身份，并且保证了协议发起者和响应者间的双向认证．同时，ESIKE仅需3条消息及更少的计算量，更加简单、高效．

Research on Formal Design of ESIKE Based on Authentication Tests

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.