A Formal Model and Algorithm for Verifying Security Protocols Based on Strand Spaces

Network security is very important in the information era, while the security protocol is one of the key problems of the network security In this paper, a model of strand spaces, a current leading branch of formal automatic verifying, is described in detail Based on the model of strand spaces, a model checker T is designed for the analysis of security protocols When model T is used, the number of reachable states decreases significantly After that, the framework and the algorithm level descriptions of model T are given It is presented and demonstrated with the Needham Schroeder protocol and the Needham Schroeder Lowe protocol