As more resources are added to computer networks, and as more vendor s look to the world wide web as a viable marketplace, the importance of being able to restrict access and to ensure some kind of acceptable behavior, even in the presence of malicious adversaries, becomes paramount. Many researchers have proposed the use of security protocols to provide these security guarantees. In this thesis, I describe a method of verifying these protocols using a special purpose model checker, BRUTUS , which performs an exhaustive state space search of a protocol model. This tool also includes a natural deduction style derivation engine which models the capabilities of an adversary trying to attack the protocol. Since the models are necessarily abstractions, one cannot prove a protocol correct. However, the tool is extremely useful as a debugger. I have used this tool to analyze fteen di erent security protocols, and have found the previously reported attacks for them.

The common limitation for model checking is the state explosion problem. This is particularly true of models in BRUTUS because they are composed of multiple components that are executing concurrently. The traces of the system are de ned by an interleaved execution. For this reason, I implemented two well known state reduction techniques in BRUTUS. The first technique exploits the symmetry due to replicated components. The second reduction technique is called the partial order reduction. This technique exploits the fact that the relative order of certain pairs of actions is immaterial to the overall correctness of the model. This means that it is not always necessary to explore all possible interleavings of actions when performing the analysis. It is also of interest that in the case of security protocol veri cation, the partial order reduction technique can be generalized so that an even greater reduction is achieved. This thesis describes how these reductions are implemented in Brutus, how they improve the eÆciency of the model checker, and how they apply to model checking of security protocols in general.

215 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu