Decidability of Equivalence of Symbolic Derivations

Yannick Chevalier (1, 2) , Michael Rusinowitch (3)

1 IRIT-LILaC - Logique, Interaction, Langue et Calcul
2 UT3 - Université Toulouse III - Paul Sabatier
3 CASSIS - Combination of approaches to the security of infinite states systems

We give in this paper an alternative, and we believe simpler, proof of a deep result by Mathieu Baudet, namely that the equivalence of symbolic constraints is decidable for deduction systems on a finite signature modulo a subterm convergent equational theory.

Mots clés: Security protocol; Dolev-Yao model; Observational equivalence; Symbolic derivation; Subterm deduction system

Domaines: Logique en informatique [cs.LO]

Yannick Chevalier, Michael Rusinowitch. Decidability of Equivalence of Symbolic Derivations. Journal of Automated Reasoning, 2012, 48 (2), pp.263-292. ⟨10.1007/s10817-010-9199-5⟩. ⟨inria-00527630⟩