@TechReport{	  basin.ea:ofmc:2004,
  abstract	= {We present 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 very large, or even
		  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 known attacks and
		  discovers a new one in a test-suite of 38 protocols from
		  the Clark/Jacob library in a few seconds 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		= {June},
  number	= 450,
  pdf		= {papers/2004/0_tr450.pdf},
  ps		= {papers/2004/0_tr450.ps.gz},
  title		= {OFMC: A Symbolic Model-Checker for Security Protocols},
  url		= {http://www.inf.ethz.ch/research/publications/},
  year		= 2004,
  user		= {moederss}
}