Abstract: 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