In order to use the strong system verfication technology model checking in the security property analysis of network protocols

formal modeling method is still the critical problem. In this paper

a modeling method based on a high-level process descriplion language is presented According to the categorizing based on intruders'objectives and roles

we analyze the running mode of protocols from the point of view of the intruders

constructing individual process specification for each principal

then verify them using model checking tools.The analysis of the BAN-Yahalom protocol illustrates the feasibility of the approach. This approach has some generality

and provids a good reference for analysis of other network protocols.