Using SPIN to model cryptographic protocols

We explore the use of Spin to model cryptographic protocols, and propose a general method to define the data structures used in the verification, such as facts, the intruder's knowledge, and so on. Based on this, we develop a general method to model the behaviors of honest principals and the intruder, in particular; we propose a general model for the intruder's deduction system. The method can be adapted to different protocols, and make it possible to transform a more abstract description of a sample protocol instance to Promela code. Our method is illustrated by using a revised TMN protocol, and the verification result has shown that it is a practical and useful way to analyze cryptographic protocols.