Welcome to the resource topic for 2006/068
Title:
Limits of the Reactive Simulatability/UC of Dolev-Yao Models with Hashes
Authors: Michael Backes, Birgit Pfitzmann, 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.
ePrint: https://eprint.iacr.org/2006/068
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .