To cite ofmc-isabelle, please use
  
  Achim D. Brucker and Sebastian A. Mödersheim. Integrating Automated 
  and Interactive Protocol Verification. In Workshop on Formal Aspects 
  in Security and Trust (FAST 2009). Lecture Notes in Computer Science (5983), 
  pages 248-262, Springer-Verlag , 2009. 
  doi: 10.1007/978-3-642-12459-4_18

A BibTeX entry for LaTeX users is

@InCollection{	  brucker.ea:integrating:2009,
  title		= {Integrating Automated and Interactive Protocol
		  Verification},
  author	= {Achim D. Brucker and Sebastian A. M{\"o}dersheim},
  booktitle	= {Workshop on Formal Aspects in Security and Trust (FAST
		  2009)},
  publisher	= {Springer-Verlag},
  address	= {Heidelberg},
  series	= {Lecture Notes in Computer Science},
  number	= {5983},
  categories	= {isabelleofmc},
  pages		= {248--262},
  doi		= {10.1007/978-3-642-12459-4_18},
  editor	= {Pierpaolo Degano and Joshua Guttman},
  year		= {2009},
  classification= {workshop},
  keywords	= {protocol verification, model-checking, theorem proving},
  areas		= {security, formal methods},
  public	= {yes},
  abstract	= {A number of current automated protocol verification tools
		  are based on abstract interpretation techniques and other
		  over-approximations of the set of reachable states or
		  traces. The protocol models that these tools employ are
		  shaped by the needs of automated verification and require
		  subtle assumptions. Also, a complex verification tool may
		  suffer from implementation bugs so that in the worst case
		  the tool could accept some incorrect protocols as being
		  correct. These risks of errors are also present, but
		  considerably smaller, when using an LCF-style theorem
		  prover like Isabelle. The interactive security proof,
		  however, requires a lot of expertise and time.
		  
		  We combine the advantages of both worlds by using the
		  representation of the over-approx\-imated search space
		  computed by the automated tools as a ``proof idea'' in
		  Isabelle. Thus, we devise proof tactics for Isabelle that
		  generate the correctness proof of the protocol from the
		  output of the automated tools. In the worst case, these
		  tactics fail to construct a proof, namely when the
		  representation of the search space is for some reason
		  incorrect. However, when they succeed, the correctness only
		  relies on the basic model and the Isabelle core.},
  pdf		= {https://www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009.pdf},
  note		= {An extended version of this paper is available as IBM
		  Research Technical Report, RZ3750.},
  filelabel	= {Extended Version},
  file		= {https://www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009-b.pdf},
  url		= {https://www.brucker.ch/bibliography/abstract/brucker.ea-integrating-2009}
}