We introduce CDiff, a new technique for reducing search when model-checking security protocols. Our technique is based on eliminating certain kinds of redundancies that arise in the search space when using symbolic exploration methods, in particular methods that employ constraints to represent and manipulate possible messages from an active intruder. Formally, we prove that CDiff terminates and is correct and complete, in that it preserves the set of reachable states so that all state-based properties holding before reduction (such as the intruder discovering a secret on the network) hold after reduction. Practically, 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 CDiff substantially reduces search and considerably improves the performance of OFMC, enabling its application to a wider class of problems.

Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols

VIGANO', Luca
2003

Abstract

We introduce CDiff, a new technique for reducing search when model-checking security protocols. Our technique is based on eliminating certain kinds of redundancies that arise in the search space when using symbolic exploration methods, in particular methods that employ constraints to represent and manipulate possible messages from an active intruder. Formally, we prove that CDiff terminates and is correct and complete, in that it preserves the set of reachable states so that all state-based properties holding before reduction (such as the intruder discovering a secret on the network) hold after reduction. Practically, 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 CDiff substantially reduces search and considerably improves the performance of OFMC, enabling its application to a wider class of problems.
1581137389
Protocol Verification; Constraints; Partial-Order Reduction
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/243768
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact