Abstract: With the rapid development of the internet, a lot of attentions have been paid to the reliability of the security protocols. Model checking can be used to obtain the assurance that a protocol can not be threatened by an intruder. In this study, on the basis of former researches, an approach is presented for using efficient and complete formal verification tool SMV to model and verify security protocol. By this approach, we can construct related model easily and verifying the property automatically. We illustrate the approach by taking Otway-Rees protocol as an example and discover an attack upon the protocol. Finally, the protocol is adapted to satisfy the security properties.