A Computational Interpretation of Dolev-Yao Adversaries
| Title | A Computational Interpretation of Dolev-Yao Adversaries |
| Publication Type | Journal Article |
| Year of Publication | 2005 |
| Authors | Herzog, Jonathan |
| Journal | Theoretical Computer Science |
| Volume | 340 |
| Pagination | 57–81 |
| Date Published | June |
| Abstract | The Dolev-Yao model is a simple and useful framework in which to analyze security
protocols, but it assumes that the adversary is extremely limited. We show that
it is possible for the results of this model to remain valid even if the adversary is
given additional power. In particular, we show that there exist situations in which
Dolev-Yao adversary can be viewed as a valid abstraction of all realistic adversaries.
We do this in a number of steps:
- The Dolev-Yao model places strong assumptions on the adversary. We capture those assumptions in the computational model (an alternate framework
with a very powerful adversary) as a non-malleability property of public-key
encryption.
- We prove an Abadi-Rogaway-style indistinguishability property [3] for the
public-key setting. That is, we show that if two Dolev-Yao expressions are
indistinguishable to the Dolev-Yao adversary, then their computational interpretations (via a chosen-ciphertext secure encryption scheme) are computationally indistinguishable.
- We show that any encryption scheme that satisfies the indistinguishability
property also satisfies our (more natural) non-malleability property.
|
| URL | http://files.jonathanherzog.com/herzog_computational_journal.pdf |
