Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives

Yohan Boichut (1) , Pierre-Cyrille Heam (2, 3) , Olga Kouchnarenko (2)

1 LIFO - Laboratoire d'Informatique Fondamentale d'Orléans
2 CASSIS - Combination of approaches to the security of infinite states systems
3 LSV - Laboratoire Spécification et Vérification [Cachan]

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 protocols; Verification; Algebraic properties

Domaines: Cryptographie et sécurité [cs.CR]

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⟩