A Supporting Tool for Spiral Model of Cryptographic Protocol Design with Reasoning-Based Formal Analysis

摘要

Many cryptographic protocols proposed to securely send and receive information with someone in unsecured network for various purposes. To design secure cryptographic protocols, formal analysis for cryptographic protocols should be included as an essential activity in a process of cryptographic protocol design. In other word, the ideal process consists of design, formalization, formal analysis, interpretation, and improvement, and the five activities are done repeatedly as similar as activities in spiral model of software development. This paper presents a supporting tool for the ideal process of cryptographic protocol design. At first, the paper presents the spiral model of cryptographic protocol design, and introduces formal analysis method with reasoning as a suitable formal analysis method for the spiral model. The paper also presents design of the supporting tool and its implementation for key exchange protocols. By the supporting tool, designers can only focus on design and improvement activities in the spiral model.