Verification Method of Key-Exchange Protocols with a Small Amount of Input Using Tamarin Prover

Abstract

We propose an automatic verification method for cryptographic protocols. Our method can verify whether or not the key-exchange protocol satisfies main security properties, requiring only the protocol specification as its input. The specification consists of, for example, how session keys are computed and which party sends/receives which data to/from the communication channel. We materialize our method using the Tamarin prover, which is an automatic verification tool for cryptographic protocols. To show the validity of our method, we verify main security properties of several existing protocols and find that the results coincide with what are theoretically known in cryptography. Our method is effective, because the complexity of cryptographic protocols has significantly increased in recent years. To overcome the complexity, people have started using automatic verification tools to verify the security of cryptographic protocols, but existing tools have two problems. First, the user must be familiar with the details of cryptography in order to describe formally the security model as part of input. Second, the input code is complex and its creation is error-prone; protocol specification and security model must be written in a specific language together with protocol-dependent extra codes. These two problems are resolved by our method.