Random Polynomial-Time Attacks and Dolev-Yao Models
Mathieu Baudet · 2006
In this paper we present an extension of DoleV-Yao models for security protocols with a notion of random polynomial-time (Las Vegas) computability. First we notice that Dolev-Yao models can be seen as transition systems, possibly infinite. We then extend these transition systems with computation times and probabilities. The extended models can account for normal Dolev-Yao transitions as well as nonstandard opera- tions such as inverting a one-way function. Our main contribution consists of showing that under reasonable assumptions the extended models are equivalent to standard Dolev-Yao models as far as (safety) security properties are concerned.