We also propose a model checking scheme for the verification of security protocols and we make use of the same ``perfect encryption'' assumptions. We propose a very intuitive model which captures the basic idea of message generation and communication. Unlike other systems, where the protocol must be encoded in CSP or in term rewrite rules, in our model, protocol definitions are easily translated into a sequence of commands like SEND, RECEIVE, and NEWNONCE. In fact, it seems clear that this translation could even be done automatically from the simple notation used to describe protocols in the literature as sequences of messages that occur during a run of the protocol.
Once we have a sequence of actions for each of the participants we take their asynchronous composition to get the full model of the protocol. There is one other unspecified participant which we call the intruder. The intruder models an untrusted communication medium as well as any malicious principals. When messages are sent they can always be intercepted by the intruder. The intruder is also allowed to send messages while impersonating a trusted principal. The intruder may even be selected as a participant in a protocol run. In addition, the intruder will be allowed to compromise temporary secrets, such as session keys, which are generated during the run of the protocol and are not meant to be treated as permanent secrets. Care must be taken, however, because it is unreasonable to allow the intruder to compromise temporary session keys as soon as they are generated. In some sense, the participants should be allowed to make some use of the key before it is allowed to be compromised.
A run of the protocol will then consist of some interleaving of actions from the participants and the intruder. This particular run or trace can then be analyzed to determine if the security of the protocol was compromised. In particular we can check if the intruder ever learns a secret which is meant to be permanent or if some principal A believes it has completed a run with principal B , while principal B has not participated in the run. In general, a set of security requirements can be specified in some kind of logic and then the trace can be checked to see if any of these requirements are violated. However, to verify that a protocol is correct, all the possible runs must be checked.
We can think of a trace as an alternating sequence of global states and actions. The global state will consist of the local state of each participant together with some global information like the set of secret information, and which principals have participated in which protocol runs. Since each principal has a finite number of actions it can take at any point in time (typically just one), then the number of possible next states is finite. If we restrict ourselves to a sufficiently large, but still finite number of runs, then the entire state space will be finite and we can do depth-first search of the state space simply checking that no reachable state violates the security specification.