Model checking is a very useful technique for verifying the network authentication protocols. in order to improve the efficiency modeling and verification on the protocols with the model checking technology, this paper first propoces a universal formalization description method of the protocol. combined with the model checker SPIN, the method can expediently verify the properties of the protocol. by some modeling simplified strategies, this paper can model several protocol effciently, and reduce the states space of the model. compared with the previos literature, this paper achieves higher degree of automation, and beter efficiency of verification. finally based on the method described in the paper, we model and verify the privacy and key management (PKM) authentication protocol. the experimental result show that the method of model checking is effective, which is useful for the other authentication protocols.