Abstract: It is a hard problem in the area of computer network security to analyze cryptographic protocols Using formal methods to analyze cryptographic protocols remains the key issue in this field In this paper, a methodology is presented by using a model checker of formal methods, SMV, to analyze the TMN cryptographic protocol After building a finite state system of the protocol and describing the security property of the protocol,SMV is used to discover some new attacks upon TMN cryptographic protocol