Paper 2006/047

Cryptographically Sound Theorem Proving

Christoph Sprenger, Michael Backes, David Basin, Birgit Pfitzmann, and Michael Waidner

Abstract

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.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. Unknown where it was published
Keywords
formal methodscryptographic soundnessDolev-YaosimulatabilityUCtheorem proving
Contact author(s)
sprenger @ inf ethz ch
History
2006-02-10: received
Short URL
https://ia.cr/2006/047
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2006/047,
      author = {Christoph Sprenger and Michael Backes and David Basin and Birgit Pfitzmann and Michael Waidner},
      title = {Cryptographically Sound Theorem Proving},
      howpublished = {Cryptology ePrint Archive, Paper 2006/047},
      year = {2006},
      note = {\url{https://eprint.iacr.org/2006/047}},
      url = {https://eprint.iacr.org/2006/047}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.