Skip to Main content Skip to Navigation
New interface
Reports (Research report)

On the Reachability Problem in Cryptographic Protocols

Roberto M. Amadio 1 Denis Lugiez 1 
1 MIMOSA - Migration and mobility : semantics and applications
CRISAM - Inria Sophia Antipolis - Méditerranée , Université de Provence - Aix-Marseille 1, Mines Paris - PSL (École nationale supérieure des mines de Paris)
Abstract : We study the verification of secrecy and authenticity properties for cryptogra- phic protocols which rely on symmetric shared keys. The verification can be reduced to check whether a certain parallel program which models the protocol and the specification can reach an erroneous state while interacting with the environment. Assuming finite principals, we present a simple decision procedure for the reachability problem which is based on a symbolic' reduction system.
Document type :
Reports (Research report)
Complete list of metadata
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 10:46:05 AM
Last modification on : Wednesday, October 26, 2022 - 8:16:11 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:20:20 PM


  • HAL Id : inria-00072738, version 1


Roberto M. Amadio, Denis Lugiez. On the Reachability Problem in Cryptographic Protocols. [Research Report] RR-3915, INRIA. 2000, pp.33. ⟨inria-00072738⟩



Record views


Files downloads