@MastersThesis{	  meiersi:master:2008,
  abstract	= {As a result of the last twenty years of research on the
		  verification of security protocols, there exists now
		  a range of protocol models, security properties, logics and
		  verification tools. Finding attacks on a flawed
		  protocol can nowadays be done efficiently using tools
		  such as Scyther [12]. However, the highest level of the
		  Common Criteria (ISO 15408) requires a formal
		  verification of protocol correctness. Doing this
		  strictly formal is still not possible, because of the lack
		  of strictly formal protocol models with an associated
		  verification technique.In this diploma thesis, we
		  present a conservative embedding in Isabelle/HOL [20] of
		  the protocol model given by the operational semantics of
		  security protocols proposed in [11]. This formalization is
		  an important milestone towards the strictly formal
		  verification of security protocols. Its
		  benefits are twofold: First, it is an unambiguous
		  description of a protocol model, which greatly facilitates
		  communicating results. Second, it enables the development
		  of a protocol verification technique with machine
		  checkable proofs. This technique may make logically sound
		  use of specialized protocol logics as well as automation
		  provided by tools like Scyther. },
  author	= {Simon Meier},
  copyright	= {2007, Simon Meier},
  language	= {USenglish},
  month		= {August},
  pdf		= {papers/2007/meiersi07ossp.pdf},
  school	= {ETH Zurich},
  title		= {A Formalization of an Operational Semantics of Security
		  Protocols},
  url		= {\url{http://people.inf.ethz.ch/meiersi/fossp/index.html}},
  year		= 2007,
  user		= {meiersi}
}