In a ubiquitous environment, it is preferable for authentication and key exchange protocols to be optimized automatically in accordance with security requirements. In this paper, we propose a security verification method for authentication and key exchange protocols that is based on Bellare et al.'s model. In particular, we show the verification points of one security property for authentication protocols and five security properties for key exchange protocols. We show that this method is valid by verifying the security of four typical examples of the authentication and key exchange protocols and the 87 authentication and key exchange protocols which were generated automatically.

Security Verification Method, Authentication and Key Exchange Protocols, Verification Points, Bellare et al.'s Model, Ubiquitous Environment