Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives

Yohan Boichut 1 Pierre-Cyrille Heam 2, 3 Olga Kouchnarenko 2
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper extends a rewriting approximations-based theoretical framework in which the security problem -- secrecy preservation against an active intruder -- may be semi-decided through a reachability analysis. In a recent paper, we have shown how to semi-decide whether a security protocol using algebraic properties of cryptographic primitives is safe. In this paper, we investigate the dual - insecurity - problem: we explain how to semi-decide whether a protocol using cryptographic primitive algebraic properties is unsafe. This improvement offers us to draw automatically a complete diagnostic of a security protocol with an unbounded number of sessions. Furthermore, our approach is supported by the tool TA4SP successfully applied for analysing the NSPK-xor protocol and the Diffie-Hellman protocol.
Type de document :
Communication dans un congrès
9th International Workshop on Verification of Infinite-State Systems - INFINITY'07, 2007, Lisbonnes, Portugal. 239, pp.57-72, 2009
Liste complète des métadonnées

https://hal.inria.fr/inria-00429356
Contributeur : Pierre-Cyrille Heam <>
Soumis le : lundi 2 novembre 2009 - 15:57:17
Dernière modification le : jeudi 15 février 2018 - 08:48:09

Identifiants

  • HAL Id : inria-00429356, version 1

Citation

Yohan Boichut, Pierre-Cyrille Heam, Olga Kouchnarenko. Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives. 9th International Workshop on Verification of Infinite-State Systems - INFINITY'07, 2007, Lisbonnes, Portugal. 239, pp.57-72, 2009. 〈inria-00429356〉

Partager

Métriques

Consultations de la notice

250