Sciweavers

JCS
2010

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

12 years 10 months ago
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...
Sebastian Mödersheim, Luca Viganò, Dav
Added 19 May 2011
Updated 19 May 2011
Type Journal
Year 2010
Where JCS
Authors Sebastian Mödersheim, Luca Viganò, David A. Basin
Comments (0)