Title: Using SPIN to model cryptographic protocols
Abstract: 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.
Publication Year: 2004
Publication Date: 2004-01-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 4
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot