Cryptographically-Sound Protocol-Model Abstractions

The authors present a formal theory for cryptographically-sound theorem proving. Their 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. They present a series of cryptographically-sound abstractions of the original BPW model that bring it much closer to standard Dolev-Yao style models.