eprint.iacr.org will be offline for approximately an hour for routine maintenance at 11pm UTC on Tuesday, April 16. We lost some data between April 12 and April 14, and some authors have been notified that they need to resubmit their papers.

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.