Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives

Yohan Boichut (1, 2) , Pierre-Cyrille Héam (2) , Olga Kouchnarenko (2, 3)

1 LIFO - Laboratoire d'Informatique Fondamentale d'Orléans
2 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)
3 CASSIS - Combination of approaches to the security of infinite states systems

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.

Mots clés: Security protocol; algebraic properties; automatic approximation

Domaines: Génie logiciel [cs.SE]; Modélisation et simulation

Yohan Boichut, Pierre-Cyrille Héam, Olga Kouchnarenko. Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives. Electronic Notes in Theoretical Computer Science, 2009, 239, pp.57--72. ⟨10.1016/j.entcs.2009.05.030⟩. ⟨hal-00561374⟩