Cryptographically Sound Theorem Proving

Speaker: Christoph Sprenger

Abstract:

Tools for security protocol verification are traditionally based on Dolev-Yao models, which give the adversary complete control over the network and assume cryptography to be perfect. Recently, much research has been devoted to underpinning such symbolic protocol models with sound cryptographic foundations (possibly relaxing the perfect cryptography assumption).

In this talk, I will describe a faithful embedding of the Dolev-Yao-style model of Backes, Pfitzmann, and Waidner (CCS 2003) in the theorem prover Isabelle/HOL. This model provides strong soundness guarantees in the sense of reactive simulatability: essentially arbitrary security properties proved in the symbolic model carry over to the cryptographic realization and this holds 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 guarantees. We have reduced 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.