@TechReport{	  basin.ea:constraint:2003-c,
  abstract	= {We introduce constraint differentiation, 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
		  constraint differentiation 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 existence of an attack) 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 constraint differentiation substantially reduces
		  search and considerably improves the performance of OFMC,
		  enabling its application to a wider class of problems.},
  author	= {David Basin and Sebastian M{\"o}dersheim and Luca
		  Vigan{\`o}},
  institution	= {ETH Z{\"u}rich, Computer Science},
  language	= {USenglish},
  month		= {April},
  number	= 405,
  pdf		= {papers/2003/405.pdf},
  ps		= {papers/2003/405.ps.gz},
  title		= {Constraint Differentiation: A New Reduction Technique for
		  Constraint-Based Analysis of Security Protocols},
  year		= 2003
}