@Article{         ofmc:2005,
  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 in terms of both
                  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\"odersheim \and Luca Vigan\`o},
  copyright     = {Springer-Verlag},
  copyrighturl  = {http://www.springeronline.com},
  journal       = {International Journal of Information Security},
  language      = {USenglish},
  month         = {June},
  note          = {Published online December 2004},
  number        = 3,
  pages         = {181--208},
  pdf           = {papers/2005/ofmc-springer.pdf},
  title         = {OFMC: A symbolic model checker for security protocols},
  url           = {http://www.springerlink.com/index/10.1007/s10207-004-0055-7} ,
  volume        = 4,
  year          = 2005,
  user          = {lvigano}
}