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 (UMR 6174), 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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00429356
Contributor : Pierre-Cyrille Heam <>
Submitted on : Monday, November 2, 2009 - 3:57:17 PM
Last modification on : Thursday, January 17, 2019 - 3:06:04 PM

Identifiers

  • 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. pp.57-72. ⟨inria-00429356⟩

Share

Metrics

Record views

319