Soundness Limits of Dolev-Yao Models

Michael Backes, Birgit Pfitzmann, and Michael Waidner.
Workshop on Formal and Computational Cryptography (FCC'06), affiliated with ICALP'06, June 2006.

Abstract

Automated tools such as model checkers and theorem provers for the analysis of security protocols typically abstract from cryptography by Dolev-Yao models, i.e., they replace real cryptographic operations by term algebras. The soundness of Dolev-Yao models with respect to real cryptographic security definitions has received significant attention in the last years. Until recently, all published results were positive, i.e., they show that various classes of Dolev-Yao models are indeed sound with respect to various soundness definitions.

Here we discuss impossibility results. In particular, we present such results for Dolev-Yao models with hash functions, and for the strong security notion of blackbox reactive simulatability (BRSIM)/UC. We show that the impossibility even holds if no secrecy (only collision resistance) is required of the Dolev-Yao model of the hash function, or if probabilistic hashing is used, or certain plausible protocol restrictions are made. We also survey related results for XOR. In addition, we start to make some impossibility results explicit that tacitly underly prior soundness results in the sense of motivating unusual choices in the Dolev-Yao models or the realizations. We also start to discuss which of the problems known for BRSIM/UC soundness extend to weaker soundness notions.

Files available online

This publication is accompanied by links to downloadable versions of this publication. These documents do not necessarily correspond exactly to the cited version. Instead, in most cases full or updated versions are provided.