HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

On name generation and set-based analysis in Dolev-Yao model

Roberto M. Amadio 1 Witold Charatonik
1 MIMOSA - Migration and mobility : semantics and applications
CRISAM - Inria Sophia Antipolis - Méditerranée , Université de Provence - Aix-Marseille 1, MINES ParisTech - École nationale supérieure des mines de Paris
Abstract : We study the control reachability problem in the Dolev-Yao model of cryptograp- hic protocols when principals are represented by tail recursive processes with generated names. We propose a conservative approximation of the problem by reduction to a non-standard collapsed operational semantics and we introduce checkable syntactic conditions entailing the equivalence of the standard and the collapsed semantics. Then we introduce a conservative and decidable set-based analysis of the collapsed operational semantics and we characterize a situation where the analysis is exact. Finally, we describe how our framework can be used to specify secrecy and freshness properties of cryptographic protocols.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 8:05:25 PM
Last modification on : Friday, February 4, 2022 - 3:19:58 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:58:33 PM


  • HAL Id : inria-00072209, version 1


Roberto M. Amadio, Witold Charatonik. On name generation and set-based analysis in Dolev-Yao model. RR-4379, INRIA. 2002. ⟨inria-00072209⟩



Record views


Files downloads