Abstract

Key Management Protocols (KMPs) are intended to manage cryptographic keys in a cryptosystem. KMPs have been standardized for Internet Protocol Security (IPsec), and these KMPs have been formally validated for their security properties. In the Internet, routing protocols have different requirements on their KMPs, which are not met by the existing IPsec KMPs, such as IKE, IKEv2, and GDOI. Protocol modeling has been used to analyze the security of the IPsec KMPs. For routing protocols, there are new KMPs proposed by the Keying and Authentication for Routing Protocols (KARP) working group of the Internet Engineering Task Force: RKMP, MRKM, and MaRK. These KMPs are designed to have better applicability for general routing protocols. However, the security of these protocols has not been validated. In this thesis, we have summarized the necessary conditions for security of routing protocols. We have analyzed the security aspects of RKMP, MRKM, and MaRK, by formally validating those protocols using the AVISPA modeling tool. This has shown that these KMPs meet the necessary security requirements.