Implement And Formal Analysis Of IKEv2

IKE (Internet Key Exchange) is the protocol which performs mutual authentication and establishes security associations (SAs) for IPSec (IP Security). It is a very important component of the IPSec protocol suite. IKE is very complex and there are some security flaws in it. So IKEv2 was presented as a successor of IKE. The goal of IKEv2 is to simplify and improve IKE, and fix various problems in it that had been found through deployment or analysis.This paper introduces IKE protocol at the first part and analyse some flaws in it.. Then IKEv2 is introduced. IKEv2 is a cryptographic protocol and its security is very important. In this paper WK logic which is a logic of belief is used to formal analysis the security of IKEv2. During the research of WK logic it is found that the calculus of WK logic is not strong enough to handle IKEv2 and an axiom is not reasonable. Some improved advises are put forward to solve these problems. These improvements do not affect the soundness of the logic. According to the analysis of the protocol this paper presents an architecture and feasible implementation of IKEv2, and describes the main function partitions of such implement. The last part of the paper is about some extended funcntions of IKEv2. These Extended functions are added in IKEv2 to satisfy different requirements in different enviroment. The principle of these functions and how they are used in IKEv2 are introduced and a mothod on rekeying a IKE SA which is to expire is put forward.