Title :
Cryptographically sound theorem proving
Author :
Sprenger, Christoph ; Basin, David ; Backes, Michael ; Pfitzmann, Birgit ; Waidner, Michael
Author_Institution :
ETH Zurich
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 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 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
Keywords :
cryptography; formal verification; protocols; theorem proving; Dolev-Yao model; Needham-Schroeder-Lowe protocol; arbitrary protocol environments; arbitrary security properties; blackbox reactive simulatability; cryptographically sound theorem proving; light-weight formalization; model formalization; proof tools; security protocol verification; theorem prover Isabelle; Automation; Carbon capture and storage; Computer security; Conferences; Cryptographic protocols; Cryptography; Error probability; Information security; Laboratories; State-space methods;
Conference_Titel :
Computer Security Foundations Workshop, 2006. 19th IEEE
Conference_Location :
Venice
Print_ISBN :
0-7695-2615-2
DOI :
10.1109/CSFW.2006.10