Fast and Automatic Verification of Authentication and Key Exchange Protocols
Haruki Ota, Shinsaku Kiyomoto, Toshiaki Tanaka · 2010
Abstract—Security in a peer-to-peer (P2P) system is not considered, although it has many potential threats. In order to make the whole P2P system secure, various security functions require to be taken into consideration for these threats, respectively. We take up authentication and key exchange protocols as a target of the security functions in the P2P system. These protocols can bear one duty in order to realize the secure P2P system. It is preferable for authentication and key exchange protocols to be verified automatically and rapidly in accordance with security requirements. In order to meet this requirement, we proposed the security verification method for the aforementioned protocols based on Bellare et al.’s model and showed the verification points of security properties to verify their security efficiently. However, there are three weaknesses in the aforementioned paper. In this paper, (1) we describe the relations of the six verification points, (2) explain how the proposed method verifies the aforementioned protocols by providing one example and (3) show the validity of the proposed method by verifying the security of 87 authentication and key exchange protocols that were generated automatically. Keywords-security verification method; authentication and key exchange protocols; verification points;