Constraint differentiation: Search-space reduction for the constraint-based analysis of security protocols

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 constraintbased 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, and demonstrated its effectiveness by extensive experimentation. Our results show that constraint differentiation substantially reduces search and considerably improves the performan...

• Type: Journal
• Year: 2010
• Where: JCS
• Authors: Sebastian Mödersheim, Luca Viganò, David A. Basin
• Keywords: Concrete Case Study, JCS 2010, Original Constraint-based Approach, Security Protocol