The Modeling Analysis of Cryptographic Protocols using Promela

摘要

The analysis and verification of security protocols is an important field in the security of computer nowadays. Model checking technique to the analysis of security protocols has proved remarkably successful, which involves three parts: modeling of system behaviors, description of system properties and system verification. Modeling of system behaviors is a highly challenging task because of its complexity, especially modeling of intruder capability. A general method is proposed to construct a Promela model of the cryptographic protocol, and make use of this way to model the Helsinki protocol. The Promela model of Helsinki protocol is automatically verified by model checker Spin and an attack to Helsinki protocol has successfully been found. Experimental result shows the verification validity via message sequence chart. The general method may become a good guideline for verifying similar cryptographic protocols.