IPsec is a protocol suite to protect the data communication between computers on internet and many VPNs(Virtual Private Networks) use IPsec protocol. IKE protocol is used to exchange keys in IPsec. Formal analysis method is used increasingly in computer science to increase the reliability of a system. In this paper, the IKE protocol is analyzed formally. This paper shows that IKE with Authentication with Signature and Authentication with Pre-Shared Key is safe, but Authentication with Public Key Encryption and A Revised Method of Authentication with Public Key Encryption are safe only with the assumption that a participant has the correct public key of the correspondent. To make sure that a participant has the correct public key of the correspondent, the usage of certificate is recommended.