In this paper we explore partial order reduction that make the task of verifying cryptographic protocols more efficient. These
reduction techniques have been implemented in our tool Brutus. Although we have implemented several reduction techniques in
our tool Brutus, due to space restrictions in this paper we only focus on partial order reductions. Partial order reductions
have proved very useful in the domain of model checking reactive systems. These reductions are not directly applicable in
our context because of additional complications caused by tracking knowledge of various agents. We present partial order reductions
in the context of verifying security protocols and prove their correctness. Experimental results showing the benefits of this
reduction technique are also presented.
Keywords Model checking - partial order reductions - and security
This research is sponsored by the National Science Foundation (NSF) under Grant No. CCR-9505472 and the Defense Advanced Research
Projects Agency (DARPA) under Contract No. DABT63-96-C-0071. Any opinions, findings and conclusions or recommendations expressed
in this material are those of the author(s) and do not necessarily reflect the views of NSF, DARPA, or the United States Government.