@TechReport{	  modersheim:on:2006,
  abstract	= {We formally investigate the relationship between several
		  models that are widely-used in protocol verification,
		  namely variants of inductive message-trace models inspired
		  by Paulson’s approach based on the Isabelle theorem prover,
		  and models based on rewriting. More precisely, we prove
		  that some of these models are over-approximations of others
		  inthe sense that they allow strictly more traces or
		  reachable states. This is common in verification: often an
		  over-approximation is easier to prove correct than the
		  original model, and proving the over-approximation is safe
		  implies that the original model is safe—provided that the
		  models are indeed in an over-approximation relation. The
		  contributions of this paper are firstly to formally prove
		  such an over-approximation relation between models, and
		  secondly to give a precise account on the differentkinds of
		  over-approximations.},
  author	= {Sebastian M{\"o}dersheim},
  institution	= {Infsec, ETH Zuerich},
  language	= {USenglish},
  month		= 03,
  number	= 512,
  pdf		= {papers/2006/1_paper.pdf},
  title		= {On the Relationships between Models in Protocol
		  Verification (Extended Version)},
  year		= 2006,
  user		= {moederss}
}