@InCollection{	  basin.ea:on-the-fly:2003,
  abstract	= {We introduce the on-the-fly model-checker OFMC, a tool
		  that combines two methods for analyzing security protocols.
		  The first is the use of lazy data-types as a simple way of
		  building an efficient on-the-fly model checker for
		  protocols with infinite state spaces. The second is the
		  integration of symbolic techniques for modeling a Dolev-Yao
		  intruder, whose actions are generated in a demand-driven
		  way. We present experiments that demonstrate that our tool
		  is state-of-the-art, both in terms of coverage and
		  performance, and that it scales well to industrial-strength
		  protocols.},
  address	= {Heidelberg},
  author	= {David Basin and Sebastian M{\"o}dersheim and Luca
		  Viganò},
  booktitle	= {Proceedings of Esorics'03},
  copyright	= {\copyright Springer-Verlag},
  language	= {USenglish},
  pages		= {253--270},
  pdf		= {papers/2003/1_ofmc.pdf},
  ps		= {papers/2003/ofmc.ps.gz},
  publisher	= {Springer-Verlag},
  series	= {LNCS 2808},
  title		= {An On-The-Fly Model-Checker for Security Protocol
		  Analysis},
  year		= 2003
}