Automatic security verification for 3-party authentication and key exchange protocols

It is preferable for authentication and key exchange protocols to be verified automatically and rapidly in accordance with security requirements. In order to meet these requirements, we proposed a security verification method for 2-party authentication and key exchange protocols based on Bellare et al.´s model and showed the verification points of the security properties to verify their security efficiently. However, 3-party authentication and key exchange protocols have more security properties than 2-party protocols: key privacy and security against a malicious insider. In this paper, we describe the novel security properties for 3-party protocols and show the verification point of key privacy. We also show the validity of the proposed method by explaining how it verifies the 3-party protocols as two verification examples. Our method is the first automatic security verification method that can verify the aforementioned security properties.