Computer Science Department
School of Computer Science, Carnegie Mellon University
BRUTUS: A Model Checker for Security Protocols
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.