Security Verification for Authentication and Key Exchange Protocols, Revisited

It is preferable for authentication and key exchange protocols to be verified automatically and rapidly in accordance with security requirements. We proposed a security verification method (OKT method) for authentication and key exchange protocols based on Bellare et al.´s model (BPR model). However, there is an estrangement between the security of the OKT method and the BPR model. In this paper, we reconsider the OKT method and once again propose a security verification method for authentication and key exchange protocols based on the BPR model. In particular, we show the novel verification points for each security property in the authentication and key exchange protocols.