@InProceedings{ sprengerCsf2008,
 abstract	= {We present a formal theory for cryptographically-sound
		  theorem proving. Our starting point is the
		  Backes-Pfitzmann-Waidner (BPW) model, which is a symbolic protocol model that is cryptographically
                  sound in the sense of blackbox reactive simulatability. To achieve
		  cryptographic soundness, this model is substantially more
		  complex than standard symbolic models and the main
		  challenge in formalizing and using this model is overcoming
		  this complexity. We present a series of
		  cryptographically-sound abstractions of the original BPW
		  model that bring it much closer to standard Dolev-Yao style
		  models. We present a case study showing that our
		  abstractions enable proofs of complexity comparable to
		  those based on more standard models. Our entire development
		  has been formalized in Isabelle/HOL.},
 address	= {Los Alamitos, CA, USA},
 author	= {Christoph Sprenger and David Basin},
 booktitle	= {Computer Security Foundations (CSF 08)},
 copyright	= {Copyright (c) 2008, IEEE, Inc.},
 isbn		= {978-0-7695-3182-3},
 language	= {USenglish},
 pages		= {115--129},
 publisher	= {IEEE Computer Society},
 title		= {Cryptographically-sound Protocol-Model Abstractions},
 year		= 2008
}