Welcome to the resource topic for 2006/047
Title:
Cryptographically Sound Theorem Proving
Authors: Christoph Sprenger, Michael Backes, David Basin, Birgit Pfitzmann, 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.
ePrint: https://eprint.iacr.org/2006/047
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .