Modeling and Verifying Cryptographic Protocols Using SPIN
Fan Jiang · Dianzi xuebao · 2002
In order to use the strong system verification 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 description 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.