Improved formal model and algorithm for verifying cryptographic protocols
Lei Zhang · Journal of Tsinghua University(Science and Technology) · 2002
The state exploration technique is one of the most popular formal verification methods for analyzing the security properties of cryptographic protocols. Mur φ is a simple useful general purpose state exploration tool, but it is subject to the exploding state problem. To solve this problem, a new model and algorithm are developed which are adapted to the natures of cryptographic protocols. First, a state space is defined according to the protocol specification, then a verification model under the control of the intruder is established and an exploring algorithm is applied to determine if any insecure states exist. By adjusting the communication process, the message exchange method etc., the number of reachable states decreases significantly and the verifying system efficiency is greatly improved.