Decidability of Equivalence of Symbolic Derivations
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.
symbolic derivation security protocol dolev-yao model observational equivalence subterm deduction system