Wilfredo Marrero

Brutus: A Model Checker for Security Protocols Degree Type: Ph.D. in Computer Science
Advisor(s): Edmund Clarke
Graduated: December 2001

Abstract:

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 fifteen different 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 defined 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 verification, 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 efficiency of the model checker, and how they apply to model checking of security protocols in general.

Thesis Committee:
Edmund M. Clarke (Chair)
Doug Tygar
Jeannette Wing
Catherine Meadows (Naval Research Labs)

Randy Bryant, Head, Computer Science Department
James Morris, Dean, School of Computer Science

Keywords:
Formal verification, authentication, electronic commerce, model checking, partial order