## CryptoDB

### Paper: Cryptographically Sound Theorem Proving

Authors: Christoph Sprenger Michael Backes David Basin Birgit Pfitzmann Michael Waidner URL: http://eprint.iacr.org/2006/047 Search ePrint Search Google We describe a faithful embedding of the Dolev-Yao model of Backes, Pfitzmann, and Waidner (CCS 2003) in the theorem prover Isabelle/HOL. This model is cryptographically sound in the strong sense of reactive simulatability/UC, which essentially entails the preservation of arbitrary security properties under active attacks and in arbitrary protocol environments. The main challenge in designing a practical formalization of this model is to cope with the complexity of providing such strong soundness guarantees. We reduce this complexity by abstracting the model into a sound, light-weight formalization that enables both concise property specifications and efficient application of our proof strategies and their supporting proof tools. This yields the first tool-supported framework for symbolically verifying security protocols that enjoys the strong cryptographic soundness guarantees provided by reactive simulatability/UC. As a proof of concept, we have proved the security of the Needham-Schroeder-Lowe protocol using our framework.
##### BibTeX
@misc{eprint-2006-21540,
title={Cryptographically Sound Theorem Proving},
booktitle={IACR Eprint archive},
keywords={foundations / formal methods, cryptographic soundness, Dolev-Yao, simulatability, UC, theorem proving},
url={http://eprint.iacr.org/2006/047},
note={ sprenger@inf.ethz.ch 13188 received 9 Feb 2006},
author={Christoph Sprenger and Michael Backes and David Basin and Birgit Pfitzmann and Michael Waidner},
year=2006
}