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: