Constraint Differentiation: Search-Space Reduction for the Constraint-Based Analysis of Security Protocols

Sebastian Alexander Mödersheim, David Basin, Luca Viganò

    Research output: Contribution to journalJournal articleResearchpeer-review


    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.
    Original languageEnglish
    JournalJournal of Computer Security
    Issue number4
    Pages (from-to)575-618
    Publication statusPublished - 2010


    • Security protocols, security protocol verification, constraints, model checking, partial-order reduction


    Dive into the research topics of 'Constraint Differentiation: Search-Space Reduction for the Constraint-Based Analysis of Security Protocols'. Together they form a unique fingerprint.

    Cite this