Model Checking of the NSPK Protocol with Spin
Donghuo Chen · Microelectronics & Computer · 2008
NSPK protocol is a classic authentication cryptographic protocol. Through establishing the Promela models of the protocol, and using linear temporal logic to describe the properties of models, at last, using the model checking tools Spin to verify the properties, and then we find the sequence of the intruder attack.