|
Published Articles >> Table of Contents >> Abstract
19th IEEE Computer Security Foundations Workshop (CSFW'06)
pp. 153-166
Cryptographically Sound Theorem Proving
Christoph Sprenger, ETH Zurich, Switzerland
Michael Backes, Saarland University, Germany
David Basin, ETH Zurich, Switzerland
Birgit Pfitzmann, IBM Zurich Research Laboratory, Switzerland
Michael Waidner, IBM Zurich Research Laboratory, Switzerland
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSFW.2006.10
Send link to a friend
| 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.
|
 Additional Information
|
Citation:
Christoph Sprenger, Michael Backes, David Basin, Birgit Pfitzmann, Michael Waidner,
"Cryptographically Sound Theorem Proving,"
csfw,
pp. 153-166,
19th IEEE Computer Security Foundations Workshop (CSFW'06),
2006
|
|
