@TechReport{	  basin.ea:on-the-fly:2003-b,
  abstract	= {We introduce the on-the-fly model-checker OFMC, a tool
		  that combines two ideas for analyzing security protocols
		  based on lazy, demand-driven search. The first is the use
		  of lazy data-types as a simple way of building efficient
		  on-the-fly model checkers for protocols with infinite state
		  spaces. The second is the integration of symbolic
		  techniques and optimizations for modeling a lazy Dolev-Yao
		  intruder, whose actions are generated in a demand-driven
		  way. We present both techniques, along with optimizations
		  and proofs of correctness and completeness.Our tool is
		  state-of-the-art both in terms of coverage and performance.
		  For example, it finds all (but one) known attacks and
		  discovers a new one in a test-suite of 36 protocols from
		  the Clark/Jacob library in under one minute of CPU time for
		  the entire suite. We also give examples demonstrating how
		  our tool scales to, and finds errors in, large
		  industrial-strength protocols.},
  author	= {David Basin and Sebastian M{\"o}dersheim and Luca
		  Vigan{\`o}},
  institution	= {ETH Z\"urich, Computer Science},
  language	= {USenglish},
  month		= {April},
  number	= 404,
  pdf		= {papers/2003/404.pdf},
  ps		= {papers/2003/404.ps.gz},
  title		= {An On-The-Fly Model-Checker for Security Protocol
		  Analysis.},
  url		= {http://www.inf.ethz.ch/research/publications/},
  year		= 2003
}