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 ParisTech - É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.
Type de document :
Rapport
[Research Report] RR-3915, INRIA. 2000, pp.33
Liste complète des métadonnées

https://hal.inria.fr/inria-00072738
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 10:46:05
Dernière modification le : samedi 27 janvier 2018 - 01:31:00
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:20:20

Fichiers

Identifiants

  • HAL Id : inria-00072738, version 1

Citation

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

Partager

Métriques

Consultations de la notice

209

Téléchargements de fichiers

392