This paper explores the use of Spin for the verification of cryptographic protocol security properties. A general method is
proposed to build a Promela model of the protocol and of the intruder capabilities. The method is illustrated showing the
modeling of a classical case study, i.e. the Needham-Schroeder Public Key Authentication Protocol. Using the model so built,
Spin can find a known attack on the protocol, and it correctly validates the fixed version of the protocol.