Formalization for Formal Analysis of Cryptographic Protocols with Reasoning Approach

摘要

Formal analysis of cryptographic protocols is necessary to find flaws before using them. However, in traditional approaches based on proving, it is difficult for analysts to enumerate all security goals for proving that a cryptographic protocol is secure because analysts sometimes overlook or do not recognize some security goals. Reasoning approach was proposed as an alternative approach, but its concrete method has not been established yet. In order to establish the concrete method, this paper presents a method of formalization for formal analysis of cryptographic protocols with reasoning approach. The paper presents a method of formalization for key exchange protocols, shows that it can be applied to any key exchange protocols, and shows that it can be extended to be applied to various cryptographic protocols.