Formal analysis and improvement of IKEv2 protocol

IKEv2 is the new version of Internet Key Exchange protocol. Despite of its several advantages, it is still susceptible to some attacks, such as man-in-the-middle attack and replay attack. The protocol is analyzed based on BSW logic formally, then an improved scheme is proposed and proved by extended BSW logic. The improvement can achieve the identity authentication in advance, resist man-in-the-middle attack and replay attack, and fulfill the authentication, secrecy and integrity of this protocol.