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...

• Type: Conference
• Year: 2006
• Where: CSFW
• Authors: Christoph Sprenger, Michael Backes, David A. Basin, Birgit Pfitzmann, Michael Waidner
• Keywords: CSFW 2006, Model, Reactive Simulatability/UC, Security Privacy, Theorem Prover Isabelle/hol