A computational interpretation of Dolev-Yao adversaries

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: (1) 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 nonmalleability property of public-key encryption. (2) We prove an Abadi-Rogaway-style indistinguishability property (J. Cryptol. 15(2) (2002) 103-127) 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. (3) We show that any encryption scheme that satisfies the indistinguishability property also satisfies our (more natural) non-malleability property.