Research on Formal Design of ESIKE Based on Authentication Tests
Rui Jiang, Hu Ai, Jian Li · Chinese Journal of Computers · 2006
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.