Paper 2006/068

Limits of the Reactive Simulatability/UC of Dolev-Yao Models with Hashes

Michael Backes, Birgit Pfitzmann, and Michael Waidner

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., abstract term algebras replace the real cryptographic operations. Recently it was shown that in essence this approach is cryptographically sound for certain operations like signing and encryption. The strongest results show this in the sense of blackbox reactive simulatability (BRSIM)/UC with only small changes to both Dolev-Yao models and natural implementations. This notion essentially means the preservation of arbitrary security properties under active attacks in arbitrary protocol environments. We show that it is impossible to extend the strong BRSIM/UC results to usual Dolev-Yao models of hash functions in the general case. These models treat hash functions as free operators of the term algebra. In contrast, we show that these models are sound in the same strict sense in the random oracle model of cryptography. For the standard model of cryptography, we also discuss several conceivable restrictions to the Dolev-Yao models and classify them into possible and impossible cases.

Note: PDF version added

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. Unknown where it was published
Keywords
Dolev-Yao modelssymbolic hash functionssimulatabilityUCimpossibility
Contact author(s)
backes @ cs uni-sb de
History
2007-05-01: revised
2006-02-23: received
See all versions
Short URL
https://ia.cr/2006/068
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2006/068,
      author = {Michael Backes and Birgit Pfitzmann and Michael Waidner},
      title = {Limits of the Reactive Simulatability/UC of Dolev-Yao Models with Hashes},
      howpublished = {Cryptology ePrint Archive, Paper 2006/068},
      year = {2006},
      note = {\url{https://eprint.iacr.org/2006/068}},
      url = {https://eprint.iacr.org/2006/068}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.