Automatic security verification for 3-party authentication and key exchange protocols
Haruki Ota, Shinsaku Kiyomoto, Yutaka Miyake · 2011
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.