Skip to Main content Skip to Navigation
Journal articles

Computing Knowledge in Equational Extensions of Subterm Convergent Theories

Abstract : We study decision procedures for two knowledge problems critical to the verification of security protocols, namely the intruder deduction and the static equivalence problems. These problems can be related to particular forms of context matching and context unification. Both problems are defined with respect to an equational theory and are known to be decidable when the equational theory is given by a subterm convergent term rewrite system. In this work we extend this to consider a subterm convergent term rewrite system defined modulo an equational theory, like Commutativity. We present two pairs of solutions for these important problems. The first solves the deduction and static equivalence problems in systems modulo shallow theories such as Commutativity. The second provides a general procedure that solves the deduction and static equivalence problems in subterm convergent systems modulo syntactic permutative theories, provided a finite measure is ensured. Several examples of such theories are also given.
Document type :
Journal articles
Complete list of metadatas

Cited literature [52 references]  Display  Hide  Download

https://hal.inria.fr/hal-02966957
Contributor : Christophe Ringeissen <>
Submitted on : Wednesday, October 14, 2020 - 3:44:27 PM
Last modification on : Thursday, October 15, 2020 - 4:10:19 AM

File

permut-subterm-know.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Serdar Erbatur, Andrew Marshall, Christophe Ringeissen. Computing Knowledge in Equational Extensions of Subterm Convergent Theories. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2020, 30 (6), pp.683-709. ⟨10.1017/S0960129520000031⟩. ⟨hal-02966957⟩

Share

Metrics

Record views

17

Files downloads

21