Cryptographically Sound Theorem Proving

13 years 11 months ago
Cryptographically Sound Theorem Proving
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 blackbox 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 guaranreduce 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...
Christoph Sprenger, Michael Backes, David A. Basin
Added 10 Jun 2010
Updated 10 Jun 2010
Type Conference
Year 2006
Where CSFW
Authors Christoph Sprenger, Michael Backes, David A. Basin, Birgit Pfitzmann, Michael Waidner
Comments (0)