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.
展开▼
