Affiliations: [a] IBM Zurich Research Laboratory, Zurich, Switzerland. E-mail: smo@zurich.ibm.com | [b] Department of Computer Science, University of Verona, Verona, Italy. E-mail: luca.vigano@univr.it | [c] Department of Computer Science, ETH Zurich, Zurich, Switzerland. E-mail: basin@inf.ethz.ch
Correspondence:
[*]
Corresponding author: L. Viganò, Department of Computer Science, University of Verona, Verona, Italy. Tel.: +39 045 8027070; Fax: +39 045 8027068.
Abstract: We introduce constraint differentiation, a powerful technique for reducing search when model-checking security protocols using constraint-based methods. Constraint differentiation works by eliminating certain kinds of redundancies that arise in the search space when using constraints to represent and manipulate the messages that may be sent by an active intruder. We define constraint differentiation in a general way, independent of the technical and conceptual details of the underlying constraint-based method and protocol model. Formally, we prove that constraint differentiation terminates and is correct, under the assumption that the original constraint-based approach has these properties. Practically, as a concrete case study, we have integrated this technique into OFMC, a state-of-the-art model-checker for security protocol analysis, and demonstrated its effectiveness by extensive experimentation. Our results show that constraint differentiation substantially reduces search and considerably improves the performance of OFMC, enabling its application to a wider class of problems.
