Loading...
Please wait, while we are loading the content...
Similar Documents
Cryptographically-sound protocol-model abstractions (2008)
| Content Provider | CiteSeerX |
|---|---|
| Author | Sprenger, Christoph |
| Abstract | We present a formal theory for cryptographically-sound theorem proving. Our starting point is the Backes-Pfitzmann-Waidner (BPW) model, which is a symbolic protocol model that is cryptographically sound in the sense of blackbox reactive simulatability. To achieve cryptographic soundness, this model is substantially more complex than standard symbolic models and the main challenge in formalizing and using this model is overcoming this complexity. We present a series of cryptographically-sound abstractions of the original BPW model that bring it much closer to standard Dolev-Yao style models. We present a case study showing that our abstractions enable proofs of complexity comparable to those based on more standard models. Our entire development has been formalized in Isabelle/HOL. 1. |
| File Format | |
| Journal | CSF |
| Language | English |
| Publisher Date | 2008-01-01 |
| Access Restriction | Open |
| Subject Keyword | Cryptographically-sound Protocol-model Abstraction Main Challenge Isabelle Hol Symbolic Protocol Model Formal Theory Cryptographically-sound Abstraction Cryptographically-sound Theorem Proving Case Study Cryptographic Soundness Standard Symbolic Model Entire Development Dolev-yao Style Model Standard Model Abstraction Enable Proof Original Bpw Model Blackbox Reactive Simulatability |
| Content Type | Text |
| Resource Type | Article |
