Rewriting for Cryptographic Protocol Verification - Extended Version -

Thomas Genet 1 Francis Klay 2
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : On a case study, we present a new approach for verifying cryptographic protocols, based on rewriting and on tree automata techniques. Protocols are operationally described using Term Rewriting Systems and the initial set of communication requests is described by a tree automaton. Starting from these two representations, we automatically compute an over-approximation of the set of exchanged messages (also recognized by a tree automaton). Then, proving classical properties like confidentiality or authentication can be done by automatically showing that the intersection between the approximation and a set of prohibited behaviors is the empty set. Furthermore, this method enjoys a simple and powerful way to describe intruder work, the ability to consider an unbounded number of parties, an unbounded number of interleaved sessions, and a theoretical property ensuring safeness of the approximation.
Type de document :
Rapport
[Research Report] RR-3921, INRIA. 2000
Liste complète des métadonnées

https://hal.inria.fr/inria-00072731
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 10:43:07
Dernière modification le : mercredi 16 mai 2018 - 11:23:03
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:19:59

Fichiers

Identifiants

  • HAL Id : inria-00072731, version 1

Citation

Thomas Genet, Francis Klay. Rewriting for Cryptographic Protocol Verification - Extended Version -. [Research Report] RR-3921, INRIA. 2000. 〈inria-00072731〉

Partager

Métriques

Consultations de la notice

174

Téléchargements de fichiers

212