Random Polynomial-Time Attacks and Dolev-Yao Models

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 operations 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.

• Type: Journal
• Year: 2006
• Where: JALC
• Authors: Mathieu Baudet
• Keywords: Dolev-Yao Models, Extended Models, JALC 2006, Transition Systems