Skip to Main content Skip to Navigation
New interface
Conference papers

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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 metadata
Contributor : Pierre-Cyrille Heam Connect in order to contact the contributor
Submitted on : Monday, November 2, 2009 - 3:57:17 PM
Last modification on : Saturday, June 25, 2022 - 10:10:56 AM


  • HAL Id : inria-00429356, version 1


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⟩



Record views