Our model checker provides a number of advantages over other formalisms. The way we model a protocol is very intuitive. We simply list the sequence of actions that each participant takes in the protocol. Unlike systems based on logics, we need not interpret the beliefs that each message is meant to convey, and we can generate counterexamples when an error is found. Unlike term rewriting approaches, we need not construct a set of rewrite rules to model how an intruder can manipulate participants to generate new messages. We simply model the protocol as a set of programs, one for each participant in the protocol. Because we separate the algorithms that maintain the intruder's knowledge from the state exploration algorithms, we also never need to encode the intruder for our models.
The prototype model checker described here has successfully discovered previously published errors in protocols. When run on correct protocols, the model checker takes a bit longer because it ends up exploring the entire reachable state space, but for the examples investigated so far, the system still terminates in about a minute. We are confident that this kind of exhaustive simulation is a feasible and useful technique for verifying security protocols. However, there are still many extensions that can be investigated and implemented as well as additional experiments to be carried out.
Despite that fact that there is a simple and straightforward translation from protocol descriptions in the literature into our modelling language, this process is tedious and prone to error. We are currently developing a better interface that would allow protocols to be specified exactly the same way they are specified in the literature. We are also working on defining a logic in which to specify the properties we are interested in checking. We are investigating how to add other message operations such as XOR and encryption with non-atomic keys. While these extensions should be possible, it is not clear how these additions will affect the efficiency of our decision procedure for message derivations.
Efficiency is also an important concern. Currently, the model checker runs in an acceptable amount of time. As we begin to increase the number of concurrent protocol runs, and as we increase the complexity of the model checker itself, we can expect the execution time to increase dramatically. Techniques that increase the efficiency of the model checker are necessary to combat this increase in complexity. In particular, it has become clear that a number of operations can be thought of as independent of each other, in the sense that they can be swapped in the execution trace without affecting the rest of the trace. This leads us to believe that partial order techniques [20] can be applied. The increase in efficiency, ease of use, and expressibility will prove useful in analyzing more complex protocols, including electronic commerce protocols.