# Graph-Embedded Rewrite Systems: Combination and Undecidability Results

Serdar Erbatur, Andrew Marshall, Paliath Narendran, Christophe Ringeissen

► To cite this version:

Serdar Erbatur, Andrew Marshall, Paliath Narendran, Christophe Ringeissen. Graph-Embedded Rewrite Systems: Combination and Undecidability Results. Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, FroCoS, Sep 2025, Reykjavik, Iceland. pp.209-227, 10.1007/978-3-032-04167-8_12. hal-05324986

HAL Id: hal-05324986

https://hal.science/hal-05324986v1

Submitted on 21 Oct 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Graph-Embedded Rewrite Systems: Combination and Undecidability Results*

Serdar Erbatur¹, Andrew M. Marshall², Paliath Narendran³, and Christophe Ringeissen⁴

¹ University of Texas at Dallas, Richardson, TX, USA
serdar.erbatur@utdallas.edu

² University of Mary Washington, Fredericksburg, VA, USA
marshall@umw.edu

³ University at Albany, SUNY, Albany, NY, USA
pnarendran@albany.edu

⁴ Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France
christophe.ringeissen@loria.fr

**Abstract.** In this paper, we consider the knowledge problems of *deduction* and *static equivalence* in the formal analysis of security protocols. We extend a recent result that developed a decision procedure for these problems in the non-disjoint combination $R \cup E$, where *R* is a subterm *E*-convergent term rewrite system (TRS) and *E* is a restricted form of permutative theory. Here, we consider the same combination problem but replace the subterm *E*-convergent TRS with a superclass of subterm *E*-convergent, called *contracting E*-convergent. We show that the previous decision procedure can be extended to obtain a new algorithm for this larger class of combined theories.

We also explore the gap between the contracting TRSs, for which deduction and static-equivalence are decidable, and a larger superclass called *graph-embedded* for which these problems are undecidable. This gap is of interest since one would like to get closer to graph-embedded and still maintain decidability of the above “knowledge problems.” We show that at least one way of weakening the restrictions of the contracting definition will not work, as it leads to undecidability results for deduction and static equivalence. We also show that a subset of the graph-embedded rules is still sufficient to obtain undecidability.

**Keywords:** Permutative Equational Theories · Term Rewriting · Combination

## 1 Introduction

In the formal analysis of security protocols, a number of tools have been developed that use constraint solving in term algebras ([10,11,29,25,15,20,30,3,8]).

<footnote>* Authors' version of a paper (DOI) published in *Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings. Lecture Notes in Computer Science 15979, Springer.*</footnote>
These tools implement algorithms and procedures to reason about the knowledge an adversary could gain by observing a protocol in execution. Two key measures of this knowledge are (intruder) deduction [28,24] and static equivalence [1], and there has been substantial work on developing decision procedures for these problems (e.g., [1,13,11,7,4,18]). These procedures typically model protocols symbolically, using rewrite systems or equational theories, and are often proven sound and complete for specific classes of theories.

One of the most common such classes is that of subterm convergent term rewrite systems. These are systems where the right-hand side of each rule is a strict subterm of the left-hand side or a constant (see, e.g., [1,11]). In recent work [9,16], an extension of this class, called *graph-embedded*, was introduced. This class leverages the graph minor relation in term graphs to define a super-class of subterm convergent systems. However, deduction and static equivalence problems are undecidable for graph-embedded systems. To address this, a sub-class called *contracting* was identified in [9,16], for which both problems remain decidable.

In this paper, we begin to explore the gap between the contracting and graph-embedded classes. This is of interest because narrowing this gap could allow for broader classes of theories to be analyzed while preserving decidability. We show that at least one natural weakening of the contracting definition leads to undecidability for both deduction and static equivalence. Furthermore, we examine restrictions of the graph-embedded definition, demonstrating that even a single rule from this definition can lead to undecidability. While it is plausible that the gap between contracting and graph-embedded systems can be reduced without sacrificing decidability, the best approach to achieving this remains an open question.

Another important aspect of many decision procedures is the ability to handle combinations of theories, particularly when some components cannot be oriented into a term rewrite system—for example, theories involving Associativity and Commutativity (AC). In recent work [19], decision procedures were developed for deduction and static equivalence in combined theories of the form $R \cup E$, where $R$ and $E$ are non-disjoint. In [19] $R$ is a subterm convergent term rewrite system, and $E$ several types of permutative theories.

In this paper, we again consider the same combination scenario $R \cup E$ but go beyond the restriction that $R$ is a subterm rewrite system. Rather, we investigate the case where $R$ is a contracting rewrite system and $R$ is convergent modulo a permutative theory $E$. We show that the procedure developed in [19] can be adapted to the larger class of theories where $R$ is contracting. Thus, we obtain decision procedures for deductions and static equivalence in this larger class of theories.

*Paper Outline:* Section 2 contains the preliminaries and background information. Section 3 presents several new combination results. In particular, it introduces the main result presented in Theorem 5. Section 4 presents several new undecidable results. First, for a contracting systems without depth restrictions, Theorem 6. Then, showing two subsets of the graph-embedded systems still have
undecidable knowledge problems, Theorem 7 and Theorem 8. Finally, Section 5
contains the conclusions and future work.

## 2 Preliminaries

We use the standard notation of equational unification [6] and term rewriting
systems [5]. Given a first-order signature $\Sigma$ and a (countable) set of variables $V$,
the $\Sigma$-terms over variables $V$ are built in the usual way by taking into account the
arity of each function symbol in $\Sigma$. Each $\Sigma$-term is well-formed: if it is rooted
by an $n$-ary function symbol in $\Sigma$, then it has necessarily $n$ direct subterms.
The set of $\Sigma$-terms over variables $V$ is denoted by $T(\Sigma, V)$. The set of variables
from $V$ occurring in a term $t \in T(\Sigma, V)$ is denoted by $Var(t)$. A term $t$ is ground
if $Var(t) = \emptyset$. A term $t$ is linear if each variable in $Var(t)$ occurs only once in
$t$. For any position $p$ in a term $t$ (including the root position $\varepsilon$), $t(p)$ is the
symbol at position $p$, $t|_p$ is the subterm of $t$ at position $p$, and $t[u]_p$ is the term $t$
in which $t|_p$ is replaced by $u$. A substitution is an endomorphism of $T(\Sigma, V)$
with only finitely many variables not mapped to themselves. A substitution is
denoted by $\sigma = \{x_1 \mapsto t_1, \dots, x_m \mapsto t_m\}$, where the domain of $\sigma$ is $Dom(\sigma) =
\{x_1, \dots, x_m\}$ and the range of $\sigma$ is $Ran(\sigma) = \{t_1, \dots, t_m\}$. Application of a
substitution $\sigma$ to $t$ is written $t\sigma$. A $\Sigma$-equation is a pair of $\Sigma$-terms denoted
by $s =^? t$ or simply $s = t$ when it is clear from the context that we do not
refer to an axiom. The size of a term $t$, denoted by $|t|$, is defined inductively as
follows: $|f(t_1, \dots, t_n)| = 1 + \sum_{i=1}^n |t_i|$ if $f$ is an $n$-ary function symbol with $n \ge 1$,
$|c| = 1$ if $c$ is a constant, and $|x| = 1$ if $x$ is a variable. The depth of a term $t$,
denoted by $depth(t)$, is defined inductively as follows: $depth(f(t_1, \dots, t_n)) =$
$1 + \max_{i=1,...,n} depth(t_i)$ if $f$ an $n$-ary function symbol with $n \ge 1$, $depth(c) = 1$
if $c$ is a constant, and $depth(x) = 0$ if $x$ is a variable.

## 2.1 Equational Theories

Given a set $E$ of $\Sigma$-axioms (i.e., pairs of terms in $T(\Sigma, V)$, denoted by $l = r$), the equational theory $=_{E}$ is the congruence closure of $E$ under the law of substitutivity (by a slight abuse of terminology, $E$ is often called an equational theory). Equivalently, $=_{E}$ can be defined as the reflexive transitive closure $\leftrightarrow_E^*$ of an equational step $\leftrightarrow_E$ defined as follows: $s \leftrightarrow_E t$ if there exist a position $p$ of $s$, $l = r$ (or $r = l$) in $E$, and substitution $\sigma$ such that $s|_p = l\sigma$ and $t = s[r\sigma]_p$. An equational theory $E$ is said to be *permutative* if for any $l = r$ in $E$, the number of occurrences of any (function or variable) symbol in $l$ is equal to the number of occurrences of that symbol in $r$. Well-known theories such as *Associativity* ($A = \{(x+y)+z = x+(y+z)\}$), *Commutativity* ($C = \{x+y=y+x\}$), and *Associativity-Commutativity* ($AC = A \cup C$) are *permutative theories*. A theory $E$ is *syntactic* if it has finite *resolvent presentation S*, defined as a finite set of axioms $S$ such that each equality $t =_{E} u$ has an equational proof $t \leftrightarrow_S^* u$ with at most one equational step $\leftrightarrow_S$ applied at the root position. The theories $C$ and $AC$ are *syntactic* [22].
## 2.2 Rewrite Relations

Given a signature $\Sigma$, an oriented $\Sigma$-axiom is called a rewrite rule of the form $l \to r$ such that $l, r \in T(\Sigma, V)$, $l$ is not a variable and $Var(r) \subseteq Var(l)$. A finite set of rewrite rules is called a *term rewriting system* (TRS, for short). Let $R$ be any TRS. For any $\Sigma$-terms $s$ and $t$, $s$ $R$-rewrites to $t$, denoted by $s \to_R t$, if there exist a position $p$ of $s$, $l \to r \in R$, and substitution $\sigma$ such that $s|_p = l\sigma$ and $t = s[r\sigma]_p$. The term $s$ is said to be $R$-reducible, $s|_p$ is called a *redex*, and in the particular case where $s|_p = l\sigma$, $s$ $R$-rewrites to $t$, denoted by $s \to_R t$. A term is an *innermost redex* if none of its proper subterms is a redex. The symmetric relation $\leftarrow_R \cup \to_R$ is denoted by $\leftarrow_R$. The rewrite relation $\to_R$ is confluent if $\leftarrow_R^* \to_R$ is included in $\to_R^* \circ \leftarrow_R^*$. The rewrite relation $\to_R$ is convergent if $\to_R$ is both terminating and confluent. When $\to_R$ is convergent, we have that for any terms $t, t', t \leftarrow_R^* t'$ iff $t \downarrow_R = t' \downarrow_R$, where $t \downarrow_R$ (resp., $t' \downarrow_R$) denotes the unique normal form of $t$ (resp., $t'$) w.r.t. $\to_R$. A convergent TRS $R$ is said to be *subterm convergent* if for any $l \to r \in R$, $r$ is either a strict subterm of $l$ or a constant. We refer to [5] for the classical notions of overlap and critical pair. Hence, a trivial critical pair is obtained by an overlap at the root position of a rule with a renaming of the same rule. A TRS with no non-trivial critical pairs is *non-overlapping*.

Let us now introduce the notion of equational rewriting, also called class rewriting [21]. Given a TRS $R$ and an equational theory $E$, the rewrite relation of $R$ modulo $E$ is defined as follows: $s \to_{R,E} t$ if there exist some position $p$ in $s$, some rule $l \to r \in R$ and a substitution $\mu$ such that $s|_p =_E l\mu$ and $t = s[r\mu]_p$. The TRS $R$ is said to be *E-convergent* if the relation $=_E \circ \to_R \circ =_E$ is terminating and $\leftarrow_{R \cup E}^* \subseteq \to_{R,E}^* \circ =_E \circ \leftarrow_{R,E}^*$. In an E-convergent TRS $R$, any term $t$ admits a unique $R$-normal form modulo $E$ denoted by $t \downarrow_{R,E}$, and for any terms $s$ and $t$, we have $s \leftarrow_{R \cup E}^* t$ iff $(s \downarrow_{R,E}) =_E (t \downarrow_{R,E})$.

## 2.3 Knowledge Problems

The applied pi calculus and frames are used to model attacker knowledge [2]. In this model, the set of messages or terms which the attacker knows, and which could have been obtained from observing one or more protocol sessions, are the set of terms in $Ran(\sigma)$ of the frame $\phi = \nu\tilde{n} . \sigma$, where $\sigma$ is a substitution ranging over ground terms. We also need to model cryptographic concepts such as nonces, keys, and publicly known values. We do this by using *names*, which are essentially free constants. Here also, we need to track the names which the attacker knows, such as public values, and the names which the attacker does not know a priori, such as freshly generated nonces. $\tilde{n}$ consists of a finite set of restricted names; these names represent freshly generated names which remain secret from the attacker. The set of names occurring in a term $t$ is denoted by $fn(t)$. For any frame $\phi = \nu\tilde{n} . \sigma$, let $fn(\phi)$ be the set of names $fn(\sigma) \setminus \tilde{n}$ where $fn(\sigma) = \bigcup_{t \in Ran(\sigma)} fn(t)$; and for any term $t$, let $t\phi$ denote — by a slight abuse of notation — the term $t\sigma$. For any term $t$, we say that $t$ satisfies the name restriction of $\phi$ if $fn(t) \cap \tilde{n} = \emptyset$.
**Definition 1 (Deduction).** Let $\phi = \nu\tilde{n}.\sigma$ be a frame, and $t$ a ground term. We say that $t$ is deduced from $\phi$ modulo $E$, denoted by $\phi \vdash_E t$, if there exists a term $\zeta$ such that $\zeta\sigma =_E t$ and $fn(\zeta) \cap \tilde{n} = \emptyset$. The term $\zeta$ is called a *recipe* of $t$ in $\phi$ modulo $E$.

Another form of knowledge is the ability to tell if two frames are *statically equivalent* modulo $E$.

**Definition 2 (Static Equivalence).** Two terms $s$ and $t$ are equal in a frame $\phi = \nu\tilde{n}.\sigma$ modulo an equational theory $E$, denoted $(s =_E t)\phi$, if $s\sigma =_E t\sigma$, and $\tilde{n} \cap (fn(s) \cup fn(t)) = \emptyset$. The set of all equalities $s = t$ such that $(s =_E t)\phi$ is denoted by $Eq(\phi)$. Given a set of equalities $Eq$, the fact that $(s =_E t)\phi$ for all $s = t \in Eq$ is denoted by $\phi \models Eq$. Two frames $\phi = \nu\tilde{n}.\sigma$ and $\psi = \nu\tilde{n}.\tau$ are statically equivalent modulo $E$, denoted as $\phi \approx_E \psi$, if $Dom(\sigma) = Dom(\tau)$, $\phi \models Eq(\psi)$ and $\psi \models Eq(\phi)$.

Deduction and static equivalence are known to be decidable for subterm convergent rewrite systems [1].

## 2.4 Graph-Embedded Rewrite Systems

Let us now introduce the graph-embedded and contracting systems. These systems were introduced in [16] and then simplified in [9], where they are used to expand on the class of subterm convergent term rewrite systems. The idea behind the definitions was to capture the “near subterm” properties of many systems that model the properties of cryptographic protocols. Many systems were close but not fully subterm. That is, the right-hand side of some rules contain terms formed from the symbols and variable on the left but which are not strict subterms.

*Example 1 (Blind Signatures).* For example, the theory of blind signatures [11] is such a theory that is beyond subterm:

$$ 
\begin{align*}
\check{sign}(\mathit{sign}(x, y), \mathit{pk}(y)) &\rightarrow x \\
\mathit{unblind}(\mathit{blind}(x, y), y) &\rightarrow x \\
\mathit{unblind}(\mathit{sign}(\mathit{blind}(x, y), z), y) &\rightarrow \mathit{sign}(x, z)
\end{align*}
$$

Consider the rule $\mathit{unblind}(\mathit{sign}(\mathit{blind}(x, y), z), y) \rightarrow \mathit{sign}(x, z)$. Notice that while $\mathit{sign}(x, z)$ is not a strict subterm of $\mathit{unblind}(\mathit{sign}(\mathit{blind}(x, y), z), y)$ it can be formed from the function symbols and variables contained in this term.

The expanded definitions allowed these systems to be captured under one single definition. To begin, we need to define the components that will be used in the two definitions, this includes a type of restricted permutation.

**Definition 3 (Leaf and Subterm Permutations).** We define two types of permutations, $\approx_s$ and $\approx_l$:
1. For terms $t$ and $t'$, we say $t$ is subterm permutatively equal to $t'$, denoted $t \approx_s t'$, if one of the following is true:

(a) $t = t'$, where $t$ and $t'$ are constants or variables, or

(b) $t = f(u_1, \dots, u_n)$ and $t' = f(u_{\sigma(1)}, \dots, u_{\sigma(n)})$ where $f$ is an $n$-ary function symbol, $n \ge 1$, and $\sigma$ is a permutation of the indexes $(1, \dots, n)$.

2. For terms $t$ and $t'$, we say $t$ is leaf permutatively equal to $t'$, denoted $t \approx_l t'$, if $t'$ is obtained from $t$ by applying a permutation on the set of leaves (variables and constants) occurring in $t$.

The first type of permutation, $\approx_s$, allows for permutation inside the term but preserves the layer like structure of the function symbols in the term graph. The second type of permutation in the classical leaf permutability and is restricted to the leaf nodes, i.e., just the variables and constants of the term graph. Notice that the two types of permutations, $\approx_s$ and $\approx_l$, do not encompass all permutative theories since $\approx_s$ permutes subterms just below the root while $\approx_l$ permutes just the leaves. We will use a combination of the above two permutations in the definition employed for graph-embedded TRS.

**Definition 4 (Permutatively Equal).** For terms $t$ and $t'$, we say $t$ is permutatively equal to $t'$, denoted $t \approx t'$, if $t \approx_s t'' \approx_l t'$, for some term $t''$.

The class of contracting TRS first starts by modeling the graph minor relation in the TRS setting. This is done by a set of rewrite schemas. This set of rewrite schemata then induces a graph-embedded term rewrite system. Notice that this is very similar to what is often done when considering the homeomorphic embedding relation in TRSs.

**Definition 5 (Graph-Embedding).** Consider the following reduction relation, $\rightarrow_{R_{gemb}}^*$, where $R_{gemb}$ is the set of rules given by the instantiation of the following rule schema:

$$ \left\{ \begin{array}{l} \text{for any } f \in \Sigma \\ (1) \quad f(x_1, \dots, x_n) \rightarrow x_i \\ (2) \quad f(x_1, \dots, x_{i-1}, x_i, x_{i+1}, \dots, x_n) \rightarrow f(x_1, \dots, x_{i-1}, x_{i+1}, \dots, x_n) \\ \text{and for any } f, g \in \Sigma \\ (3) \quad f(x_1, \dots, x_{i-1}, g(\bar{z}), x_{i+1}, \dots, x_m) \rightarrow g(x_1, \dots, x_{i-1}, \bar{z}, x_{i+1}, \dots, x_m) \\ (4) \quad f(x_1, \dots, x_{i-1}, g(\bar{z}), x_{i+1}, \dots, x_m) \rightarrow f(x_1, \dots, x_{i-1}, \bar{z}, x_{i+1}, \dots, x_m) \end{array} \right\} $$

We say a term $t'$ is graph-embedded in a term $t$, denoted $t \succcurlyeq_{gemb} t'$, if $t'$ is a well formed term such that $t \rightarrow_{R_{gemb}}^* t'$.

A TRS $R$ is graph-embedded if for any $l \rightarrow r \in R$, $l \succcurlyeq_{gemb} r$ or $r$ is a constant.

The graph-embedded class is not sufficient to obtain decidability of static equivalence, so we next need to introduce a type of projection rule that ensure access to subterms and thus decidability of deduction and static equivalence.
**Definition 6 (Projecting Rule).** Let R be a TRS, x a variable and t a term with a single occurrence of x. A projecting rule in R over t leading to x is a rule in R which is a variant of t' → x where t' is a superterm of t with no additional occurrences of x.

Another way to view the projection rules of the above definition is that $t'$ is a context, $t'[ ]$, and there is a rule of the form $t'[t] \to x$. The way these projecting rules relate to the entire term rewrite system can now be defined.

**Definition 7 (Projection-Closed Derivation).** Let R be a TRS. A non-empty $R_{gemb}$-derivation is said to be projection-closed with respect to R if it has the form

$$s \to_{R_{gemb}}^{l \to r, \gamma} s' \to_{R_{gemb}}^{*} t$$

where

- $s$ is a linear term and $t$ is a well formed term,

- $l \to r$ is a $R_{gemb}$ rule among (1), (2) and (4),

- $\gamma$ is a variable renaming s.t.:

- if $l \to r$ is rule (1), $f(x_1, \dots, x_n) \to x_i$, then for any $x_i\gamma$ occurring in t there exists a projecting rule in R over $f(x_1, \dots, x_n)\gamma$ leading to $x_i\gamma$,

- if $l \to r$ is rule (4),

$$f(x_1, \dots, x_{i-1}, g(\bar{z}), x_{i+1}, \dots, x_m) \to f(x_1, \dots, x_{i-1}, \bar{z}, x_{i+1}, \dots, x_m)$$

then for any $z_i\gamma$ occurring in t there exists a projecting rule in R over $g(\bar{z})\gamma$ leading to $z_i\gamma$,

- $s' \to_{R_{gemb}}^{*} t$ is either projection-closed with respect to R or empty.

**Definition 8 (Projection-Closed Permutative Equality).** Let R be a TRS and $l = r$ a permutative equality obtained by one or zero applications of $\approx_s$ followed by one or zero applications of $\approx_l$. The equality $l = r$ is said to be projection-closed with respect to R if the following holds: for any variable $x$ occurring in a strict subterm $l' \neq x$ of $l$ and in a strict subterm $r'$ of $r$ such that $l' \neq r'$, there exists a projecting rule in R over $l'$ leading to $x$.

Based on Definitions 7 and 8, we can now introduce the subset of graph-embedded rules for which we can obtain decidability of the knowledge problems.

**Definition 9 (Contracting TRS).**

A TRS R is said to be contracting if for any non-subterm rule $l \to r$ in R one of the following holds:

- there exist a position $p$ of $l$, a substitution $\sigma$ ranging over variables, a projection-closed derivation $g \to_{R_{gemb}}^+$ $d$ with respect to R such that $l|_p = g\sigma$ and $r = d\sigma$ is of depth 1,

- $l = r$ is a permutative equality of depth 2 which is projection-closed with respect to R.
A contracting TRS, R, is strictly contracting if for any $l \to r \in R$, depth($l$) > depth($r$).

**Example 2.** Consider the theory of blind signatures from Example 1. This theory is contracting. Let's look at the rule: unblind(sign(blind($x, y$), $z$), $y$) $\to$ sign($x, z$). Let $l = \text{unblind}(\text{sign}(\text{blind}(x, y), z), y)$.

Then, $l = \text{unblind}(\text{sign}(\text{blind}(x, y), z), y) \to_{R_{gemb}}^{\epsilon, \text{rule 1}} \text{sign}(\text{blind}(x, y), z)$. We can start the projection-closed derivation at $l|_1 = \text{sign}(\text{blind}(x, y), z)$. This leads to $\text{sign}(\text{blind}(x, y), z) \to_{R_{gemb}}^{\text{rule 4}} \text{sign}(x, y, z) \to_{R_{gemb}}^{\text{rule 2}} \text{sign}(x, z)$. We also need the required projecting rule, given the above projection-closed derivation.

The step, $\text{sign}(\text{blind}(x, y), z) \to_{R_{gemb}}^{\text{rule 4}} \text{sign}(x, y, z)$, applied rule 4 below the root, to remove the blind() function symbol. Thus, there must be a projecting rule, which is the rule $\text{unblind}(\text{blind}(x, y), y) \to x$.

## 2.5 Restricted Classes of Permutative Theories

Leaf permutative theories are a further restriction on permutative theories where for each axiom, $l = r$, $r$ is a leaf permutation of $l$, i.e., $r = l\sigma$, where $\sigma$ is a permutation of the leaf nodes of $l$. It has already been shown in [9] that deduction is decidable in permutative theories but static equivalence is not [17].

**Definition 10 (Variable-Permuting Theory).** An axiom $l = r$ is said to be variable-permuting [26] if all the following conditions are satisfied:

1. the set of occurrences of $l$ is identical to the set of occurrences of $r$,

2. for any non-variable occurrence $p$ of $l$, $l(p) = r(p)$,

3. for any $x \in \text{Var}(l) \cup \text{Var}(r)$, the number of occurrences of $x$ in $l$ is identical to the number of occurrences of $x$ in $r$.

An equational theory $E$ is said to be separate variable-permuting (SVP, for short) if for any $l = r \in E$ we have:

- $l = r$ is a variable-permuting axiom,

- $l$ and $r$ are rooted by the same function symbol that does not occur elsewhere in $E$.

An inner constructor symbol of $E$ is a function symbol from $E$ that never occurs at the root of any equality in $E$.

**Example 3 (Intruder Theory with a Permutative Axiom).** Let us consider a theory used in practice to model a group messaging protocol [12]. For this protocol, the theory modeling the intruder can be defined [27] as a combination $R \cup K$ where $K = \{\text{keyexch}(x, pk(x'), y, pk(y')) = \text{keyexch}(x', pk(x), y', pk(y))\}$ and

$$R = \left\{ \begin{array}{ll} \text{adec}(\text{aenc}(m, pk(sk)), sk) & \to m \quad \text{getmsg}(\text{sign}(m, sk)) \to m \\ \text{checksign}(\text{sign}(m, sk), m, pk(sk)) & \to \text{ok} \quad \text{sdec}(\text{senc}(m, k), k) \to m \end{array} \right\}.$$

$R$ is a subterm convergent TRS and $K$ is a SVP theory such that the shared symbol $pk$ is an inner constructor of $K$ and a constructor of $R$.
An equational theory $\mathcal{E}$ is closed by paramodulation if $\mathcal{E}$ is a finite set of equalities saturated with respect to the classical paramodulation rule [23]. Thus, an equational theory is saturated by paramodulation when, after exhaustive applications of the paramodulation rule, no further non-redundant equalities.

**Lemma 1.** Any SVP theory is closed by paramodulation.

Critical for the results in this paper is the following from [17].

**Theorem 1 ([17]).** Static equivalence is undecidable in general for variable permuting theories.

**Theorem 2 ([17]).** Both deduction and static equivalence are decidable in any SVP theory.

It has already been shown in [9] that it is possible to combine $\approx$-free contracting convergent TRS with permutative theories to obtain decidability results for deduction. However, since static equivalence is undecidable in general for even variable permuting theories [17], there was no equivalent result for static equivalence.

**Theorem 3.** Let $R$ be any contracting convergent TRS and $\mathcal{E}$ any SVP theory such that the function symbols shared by $R$ and $\mathcal{E}$ are constructors for $R$ and inner constructors for $\mathcal{E}$. Then, both deduction and static equivalence are decidable in $R \cup \mathcal{E}$.

*Proof.* The combination result from [18] can be applied due to Theorem 2. □

Next, we consider going beyond the restriction of only sharing constructors.

# 3 Equational Rewriting Modulo Permutative Theories

In this section we start investigating the possibility to consider $\mathcal{E}$ is syntactic permutative, e.g., $\mathcal{E}$ is a permutative theory closed by paramodulation, and $R$ is $\mathcal{E}$-convergent. In this case, an additional finiteness assumption is required, as shown below. The investigated approach relies on the possibility of computing a finite representation of all the terms that are matched modulo $\mathcal{E}$ by the left-hand sides of the TRS $R$.

**Definition 11.** An $\mathcal{E}$-variant of a term $l$ is a pair $(t, \sigma)$ such that $t =_{\mathcal{E}} l \sigma$ and $\text{Dom}(\sigma)$ is included in $fv(l)$. Given two $\mathcal{E}$-variants $(u, \theta)$ and $(v, \gamma)$ of a term $l$, $(u, \theta)$ is more general than $(v, \gamma)$, denoted by $(u, \theta) \leq_{\mathcal{E}} (v, \gamma)$ if there exists a substitution $\tau$ such that $u\tau =_{\mathcal{E}} v$ and $\theta\tau =_{\mathcal{E}} \gamma$. A complete set of $\mathcal{E}$-variants of $l$, denoted by $CV_{\mathcal{E}}(l)$, is a set of $\mathcal{E}$-variants of $l$ such that for any $\mathcal{E}$-variant $(v, \gamma)$ of $l$, there exists $(u, \theta) \in CV_{\mathcal{E}}(l)$ such that $(u, \theta) \leq_{\mathcal{E}} (v, \gamma)$. The equational theory $\mathcal{E}$ is said to have the Finite Equational Variant Property (FEVP, for short) if any term admits a finite complete set of $\mathcal{E}$-variants.
Given a syntactic permutative theory $E$, we have developed in [19] a general procedure that, when terminating, computes a finite set of terms $E$-matched by $l$, denoted by $CMT_E(l)$ and such that $\{(t, \sigma) \mid t \in CMT_E(l), l\sigma =_E t\}$ is a finite $CV_E(l)$. This procedure, called MTG is defined as a rule-based system consisting of a matching procedure for syntactic permutative theories plus some additional rules to guide the instantiation of terms to be $E$-matched by $l$, in case the matching procedure fails when the terms are too small. The MTG procedure is not guaranteed to terminate for an arbitrary syntactic permutative theory $E$. However, the MTG procedure is guaranteed to terminate for permutative theories closed under paramodulation which are known to be syntactic [23], and so we have:

**Theorem 4.** Any permutative theory closed by paramodulation has the FEVP.

**Definition 12.** Assume $R$ is TRS such that for any $l \to r \in R$, $CMT_E(l)$ is finite. Under this assumption, the size of $R$ modulo $E$, denoted by $|R|$, is defined as follows: $|R| = \max\{|t| \mid t \in CMT_E(l), l \to r \in R\}$.

From now on, we assume that $E$ is a syntactic permutative theory and $R$ is a contracting $E$-convergent TRS such that $|R|$ is defined. We introduce below some notions defined with respect to $|R|$, such as the completion of a frame and a set of equalities generated by terms bounded by $|R|$.

**Definition 13.** Given a term $t$, $gst_E(t)$ denotes the set of terms $E$-equal to some term in $\bigcup_{\{t' \mid t'=_E t\}} gst(t')$, where $gst(t')$ is the set of (well-typed) terms reachable by $R_{gemb}$ from $t'$. For any normalized frame $\phi = \nu\tilde{n}.\sigma$, let $gst_E(\sigma)$ be the set of terms $\bigcup_{x \in Dom(\sigma)} gst_E(x\sigma)$. The set of terms $D_*(\phi)$ is the smallest set $D$ such that:

(1) $\mathrm{Ran}(\sigma) \subseteq D$,

(2) if $t_1, \dots, t_n \in D$ and $f(t_1, \dots, t_n) \in gst_E(\sigma)$ then $f(t_1, \dots, t_n) \in D$,

(3) if $t \in D$, $t' \in gst_E(\sigma)$, $t =_E t'$, then $t' \in D$,

(4) if there is a root reduction $s[\bar{d}] \to_{R,E} t$ where $|s| \le |R|$, $fn(s) \cap \tilde{n} = \emptyset$, $\bar{d} \in D$ and $t \in gst_E(\sigma)$, then $t \in D$.

Let $\sigma_* = \sigma\{\chi_u \mapsto u \mid u \in D_*(\phi)\setminus\mathrm{Ran}(\sigma)\}$ where $\chi_u$ is a fresh variable. The frame $\phi_* = \nu\tilde{n}.\sigma_*$ is called the completion of $\phi$ with respect to contexts bounded by $|R|$. Given a recipe $\zeta_u$ for each $u \in D_*(\phi)\setminus\mathrm{Ran}(\sigma)$, the substitution $\{\chi_u \mapsto \zeta_u \mid u \in D_*(\phi)\setminus\mathrm{Ran}(\sigma)\}$ is called a recipe substitution of $\phi$ and is denoted by $\zeta_\phi$. The set $Eq_\zeta^B(\phi)$ is the set of equalities $t\zeta_\phi = t'\zeta_\phi$ such that $(t\zeta_\phi =_R t'\zeta_\phi)\phi$ and $t, t'$ are terms such that $|t| \le |R|$, $|t'| \le |R|$ and $(fn(t) \cup fn(t')) \cap \tilde{n} = \emptyset$.

In the following, we present reduction methods from $RE = R \cup E$ to the combined theory $\emptyset \cup E$ where $\emptyset$ is the empty theory over the function symbols occurring in $R$ but not in $E$. In the next subsections, this combined theory is simply denoted by $E$.
**3.1 Deduction**

The decision procedure for the deduction problem in RE is based on the following reduction lemma.

**Lemma 2 (Deduction).** Let $RE = R \cup E$ where $E$ is any syntactic permutative theory and $R$ is any contracting $E$-convergent TRS such that $|R|$ is defined. For any normalized frame $\phi$ and any normalized term $t$, we have that $\phi \vdash_{RE} t$ if and only if $\phi_* \vdash_E t$.

**3.2 Static Equivalence**

In a way similar to what is done for disjoint combinations [14], we extend the input frames with the instantiation of recipes of all deducible terms occurring in the completions.

**Definition 14.** Let $\phi = \nu\tilde{n.}\sigma$ be a frame. Let $\Pi$ be a set of terms $t$ such that $t\sigma$ is ground and $t$ satisfies the name restriction of $\phi$. The $\Pi$-extension of $\phi$ is the frame $\Pi\phi = \nu\tilde{n.}\{\chi_t \mapsto t \mid t \in \Pi\}\sigma$.

Given any normalized frames $\bar{\phi} = \nu\tilde{n.}\sigma$ and $\bar{\psi} = \nu\tilde{n.}\tau$ such that $\text{Dom}(\sigma) = \text{Dom}(\tau)$, let $\bar{\phi} = (\Pi\bar{\phi})\downarrow_{R,E}$, and $\bar{\psi} = (\Pi\bar{\psi})\downarrow_{R,E}$ where $\Pi$ is the set of subterms in $\text{Ran}(\zeta_{\bar{\phi}}) \cup \text{Ran}(\zeta_{\bar{\psi}})$.

**Lemma 3.** We have $(\bar{\phi})_* = \bar{\phi}$, $(\bar{\psi})_* = \bar{\psi}$ and $\phi \approx_{RE} \psi$ if and only if $\bar{\phi} \approx_{RE} \bar{\psi}$.

The decision procedure for static equivalence in RE is based on the following reduction lemma:

**Lemma 4 (Static Equivalence).** Let $RE = R \cup E$ where $E$ is any syntactic permutative theory and $R$ is any contracting $E$-convergent TRS such that $|R|$ is defined. For any normalized frames $\bar{\phi}$ and $\bar{\psi}$, we have $\bar{\phi} \approx_{RE} \bar{\psi}$ iff $\bar{\psi} \models \text{Eq}^B(\bar{\phi})$ and $\bar{\phi} \models \text{Eq}^B(\bar{\psi})$ and $\bar{\phi} \approx_E \bar{\psi}$.

**3.3 Decidability Results and Correctness Proofs**

According to the above reduction lemmas, we get the following result.

**Theorem 5.** Let $RE = R \cup E$ where $E$ is any syntactic permutative theory and $R$ is any contracting $E$-convergent TRS such that $|R|$ is defined. If both deduction and static equivalence are decidable in $E$, then both deduction and static equivalence are decidable in $RE$.

**Corollary 1.** Let $RE = R \cup E$ where $E$ is any SVP theory and $R$ is any contracting $E$-convergent TRS. Then, both deduction and static equivalence are decidable in $RE$.

The proofs of the reduction lemmas rely on the following technical lemma:
**Lemma 5.** Let RE = R ∪ E where E is any syntactic permutative theory and R is any contracting E-convergent TRS such that |R| is defined. Assume $\bar{\phi} \approx_E \bar{\psi}$ and $\bar{\psi} \models Eq^B(\bar{\phi})$. For any term s satisfying the name restriction and for any term t such that $s\bar{\phi} \to_{R,E} t$, there exists a term u satisfying the name restriction such that $t =_E u\bar{\phi}$ and $s\bar{\psi} =_{RE} u\bar{\psi}$.

*Proof.* There are two possibilities.

(i) Let us first assume that the rewrite step occurs at the root position. Suppose $s\bar{\phi} =_E l_\mu$ with $l \to r \in R$. For any $x \in fv(l)$, $x\mu$ is possibly a term of the form $t\bar{\phi}$ where $t$ is a subterm of $s$. Consider a constant-abstraction mapping $\pi$ defined as follows: for any maximal subterm $s|_p\bar{\phi}$ occurring in $x\mu$ where $x \in fv(l)$, let $\pi(s|_p\bar{\phi}) = c_p$ where $c_p$ is a fresh free constant. For the term $s'\bar{\phi}$ obtained from $s\bar{\phi}$ by replacing each maximal subterm $s|_p\bar{\phi}$ by the constant $\pi(s|_p\bar{\phi})$, we have that $s'$ is a small context such that $|s'| \le |R|$ and $s'\bar{\phi} \to_{R,E} r\mu$ for $l \to r \in R$. By assumption, $R$ is contracting and so we have $r\mu =_E u'\bar{\phi}$ for some term $u'$. By replacing back the constants introduced by the constant abstraction, we have $(s'\bar{\phi})\pi^{-1} \to_{R,E} \circ =_E (u'\bar{\phi})\pi^{-1}$, where $(s'\bar{\phi})\pi^{-1} = s\bar{\phi}$ and $(u'\bar{\phi})\pi^{-1} = u\bar{\phi}$ for some term $u$. Consequently, $s'\bar{\phi} \to_{R,E} \circ =_E u\bar{\phi}$. By definition of Eq$^B$ and by assumption on $\bar{\psi}$, we have that $s'\bar{\psi} =_{RE} u'\bar{\psi}$. By replacing each constant $\pi(s|_p\bar{\phi})$ with $s|_p\bar{\psi}$, we get $s\bar{\psi} =_{RE} u\bar{\psi}$.

(ii) Let us now assume that the rewrite step occurs below the root position. There exists a position $p \neq \epsilon$ such that $s'\bar{\phi} = (s'\bar{\phi})[s\bar{\phi}]_p$ with $s\bar{\phi} \to_{R,E} t$. By the case (i) above, there exists a term $u$ such that $t =_E u\bar{\phi}$ and $s\bar{\psi} =_{RE} u\bar{\psi}$. Then, we have

$$s'\bar{\phi} \to_{R,E} (s'\bar{\phi})[t]_p =_E (s'\bar{\phi})[u\bar{\phi}]_p = (s'[u]_p)\bar{\phi}$$

and

$$s'\bar{\psi} = (s'\bar{\psi})[s\bar{\psi}]_p =_{RE} (s'\bar{\psi})[u\bar{\psi}]_p = (s'[u]_p)\bar{\psi}$$

□

# 4 Undecidability Results

One approach that could be investigated to expand the above results would be to try to weaken the definition of projection-closed equality (Definition 8) so that more permutative theories could be considered in the framework of contracting TRS. However, we show that if we weaken the definition of contracting, Definition 9, by relaxing the type of permutations allowed, we quickly run into undecidability results.

It turns out that while the above restrictions detailed in Definition 9 may be able to be weakened slightly, one still requires restrictions on both the rule applications and the permutations allowed or undecidability results follow. Indeed, we next show that we can consider subsets of the rules from the graph-embedded definition and these subsets still lead to the undecidability of the knowledge problems.
## 4.1 A Weaker Contracting Definition

Let us first consider removing the depth restriction from the definition of contracting TRS (Definition 8). We show that by removing this restriction we run into undecidability. To prove this result we start with a construction developed in [17] showing that a Linear Bounded Automaton's (LBA) transition function can be simulated by a leaf permuting TRS. This in turn is used to show that static equivalence is undecidable in leaf permuting theories. However, the resulting TRS, simulating the LBA, from [17] is permutative but not contracting. The TRS is missing the required projection rules of Definition 8. These rule cannot just be added since they will have overlaps with the existing rules and thus interfere with the LBA simulation. We can however, modify slightly the construction from [17] to prevent these overlaps when adding the required projection rules.

To detail the modification, we first give a brief overview of the construction. Given a LBA $M = (Q, \Sigma, \Gamma, q_0, a_1, q_r, \delta)$, assume $\Sigma = \{a_1, a_2, \dots, a_n\}$ and $\Gamma = \{<, >, \sqcup\} \cup \Sigma$, where $<, >$ are the left and right end caps respectively, and $\sqcup$ is the blank symbol. Terms can be constructed that simulate the state of the LBA by introducing three function symbols, $f, g, h$ and three constants, $a, b$, and $P$. $h$ is used to represent the state of the LBA. To represent state $q_i$, a constant $b$ is placed at the $i^{th}$ position with the remaining positions containing $a$ constants. There is an extra position in $h$, one more than $|Q|$ and it is used to represent a dummy or default state. $g$ has arity $|\Gamma|$ and is used to encode the alphabet characters. A constant $b$ at position $i$ in $g$ with $a$ constants placed at all other positions to encode $a_i$. $f$ is used to form terms which consist of an encoding of a state, an encoding of a single character, and an $f$-rooted subterm or the constant $P$. The subterm is used to encode the rest of the string. The constant $P$ is used to stop the encoding. For example, suppose you have a state $<q_0, 0>$ of the LBA, $|Q| = 2$, and $\Gamma = \{<, >, 0, \sqcup\}$. Then the term representation of this would be:

$$f(h(b, a, a), g(b, a, a, a), f(h(a, a, b), g(a, a, b, a), f(h(a, a, b), g(a, b, a, a), P)))$$

Then, the left and right moves of the LBA can be simulated by a permutative TRS. For example, if the LBA has a move $\delta(q_0, <) = (q_1, <, R)$ one of the rules for this transition would then be:

$$f(h(b, a, a), g(b, a, a, a), f(h(a, a, b), g(a, a, b, a), x)) \rightarrow \\ f(h(a, a, b), g(b, a, a, a), f(h(a, b, a), g(a, a, b, a), x))$$

Notice that there would be several versions of this rule, since this is the version with the 0 symbol encoded as the next symbol to read, right of $<$. Likewise for a LBA transition $\delta(q_0, >) = (q_1, >, L)$, one of the rules would be:

$$f(h(a, a, b), g(a, a, b, a), f(h(b, a, a), g(a, b, a, a), x)) \rightarrow \\ f(h(a, b, a), g(a, a, b, a), f(h(a, a, b), g(a, a, b, a), x))$$
Now, notice we can't just add projection rules to this TRS. The required projection rule for the above right-move example transition would be:

$$f(h(a, a, b), g(a, a, b, a), x) \to x$$

However, notice that this overlaps with the above left-move transition.

**Theorem 6.** *Static equivalence is undecidable in general for contracting TRSs without a depth restriction.*

*Proof.* We can fix the above issue with overlapping projection rules by introducing two dummy states instead of one, a left-dummy state, $q_{ld}$, and a right-dummy state, $q_{rd}$. This can be done by increasing the arity of $h$ by one. The second to last position being the left-dummy state and the final position the right dummy-state. Thus if $|Q| = n$, $h$ has arity of $n+2$. For example, in the above case with $|Q| = 2$, the left-dummy state $q_{ld} = h(a, a, b, a)$ and the right $q_{rd} = h(a, a, a, b)$.

The initial state of the LBA tape has just right-dummy states with the LBA tape head to the left of all the dummy states. Right moves by the LBA change the dummy states, that are now left of the LBA tape head, to left-dummy states. Likewise, left rule moves of the LBA change left-dummy states back to right-dummy states.

We illustrate these modifications with the two rule examples from above. The right moves are now modified as follows:

$$ \begin{aligned} f(h(b, a, a, a), g(b, a, a, a), f(h(a, a, a, b), g(a, a, b, a), x)) &\to \\ f(h(a, a, b, a), g(b, a, a, a), f(h(a, b, a, a), g(a, a, b, a), x)) &\to \end{aligned} $$

The left moves are modified as follows:

$$ \begin{aligned} f(h(a, a, b, a), g(a, a, b, a), f(h(b, a, a, a), g(a, b, a, a), x)) &\to \\ f(h(a, b, a, a), g(a, a, b, a), f(h(a, a, a, b), g(a, a, b, a), x)) &\to \end{aligned} $$

Now when we add the projection rules for right LBA moves we have rules of the form:

$$f(h(a, a, b, a), g(a, a, b, a), x) \to x$$

However, this now doesn't overlap the left move rules of the LBA since they include the subterm for the right-dummy state $h(a, a, a, b)$ instead of the left-dummy that is now included in the projection rules, $h(a, a, b, a)$. The same occurs for the left LBA moves. □

## 4.2 Subset of Graph-Embedded

Next, let us consider subsets of the rules from the graph-embedded definition.

**Definition 15.** A rule-4 graph-embedded term rewrite system is any TRS, $R$, such that for all $l \to r \in R$, $l \to_{R_{gemb}}^+$ $r$, using only rules (4) and (2) of Definition 5. Denote this set of graph-embedded rules as $R_4$.

Likewise, a rule-3 graph-embedded term rewrite system is any TRS, $R$, such that for all $l \to r \in R$, $l \to_{R_{gemb}}^+$ $r$, using only rules (3) and (2) of Definition 5.
**Rule-4 Graph-Embedded:** First, we can consider the restricted rule-4 graph-embedded TRSs and use a result previously developed for homeomorphic embedded TRSs.

**Theorem 7.** *Deduction is undecidable in general for rule-4 graph-embedded TRS.*

*Proof.* Assume for each $l \to r \in R$, for some TRS $R$, that $l \to_{R_{emb}}^* r$, $r$ is homeomorphically embedded in $l$, and the root symbol of $l$ remains the root symbol for $r$, $l(\epsilon) = r(\epsilon)$. Then, $l \to_{R_4}^* r$. Notice that any homeomorphic rewrite step below the root can be emulated by several applications of rule (4) and (2). If $t = f(\bar{t}_1, g(x_1, \dots, x_i, \dots, x_n), \bar{t}_2) \to_{R_{gemb}} f(\bar{t}_1, x_i, \bar{t}_2)$ then,

$$ 
\begin{aligned}
t &= f(\bar{t}_1, g(x_1, \dots, x_i, \dots, x_n), \bar{t}_2) \to_{(4)} \\
  & f(\bar{t}_1, x_1, \dots, x_i, \dots, x_n, \bar{t}_2) \to_{(4)}^{n-1} f(\bar{t}_1, x_i, \bar{t}_2).
\end{aligned}
$$

In [9] it is shown that deduction is undecidable in general for homeomorphic embedded TRS. The proof uses a reduction from the Modified Post Correspondence Problem (MPCP). The TRS developed in that reduction was the following:

$$ B = \bigcup_{i=1}^{n} \{ f(\tilde{\alpha}_i(x), g_i(y), \tilde{\beta}_i(z), unlocked(z)) \to f(x, y, z, unlocked(z)) \}, $$

$$ U = \{ f(x, y, x, locked(unlocked(z))) \to f(x, y, x, unlocked(z)) \}. $$

Notice that each of these rules is both homeomorphic embedded and root symbol preserving. Thus, each of these rules is also rule-4 graph-embedded. □

**Rule-3 Graph-Embedded:** Next, consider the rule-3 graph-embedded TRSs. For this reduction we will use the Modified Post Correspondence Problem (MPCP) an undecidable version of the well known undecidable Post Correspondence Problem (PCP). Let $\Gamma = \{a, b\}$ be the alphabet of the MPCP problem. Then, an instance of the problem is a finite set of string pairs, $S = \{(\alpha_i, \beta_i) | i \in [1, n]\} \subseteq \Gamma^+ \times \Gamma^+$, and an input string $\alpha_0 \in \Gamma^*$. A solution is a sequence of indexes $i_1, \dots, i_k \in [1, n]$ such that $\alpha_{i_1} \alpha_{i_2} \dots \alpha_{i_k} = \beta_{i_1} \beta_{i_2} \dots \beta_{i_k}$, $\alpha_0$ is a suffix of $\alpha_{i_1} \alpha_{i_2} \dots \alpha_{i_k}$, and $\alpha_0$ is a suffix of $\beta_{i_1} \beta_{i_2} \dots \beta_{i_k}$. That is, there is a string $\alpha' \in \Gamma^*$ s.t. $\alpha_{i_1} \alpha_{i_2} \dots \alpha_{i_k} = \alpha' \cdot \alpha_0 = \beta_{i_1} \beta_{i_2} \dots \beta_{i_k}$. Notice that the standard MPCP is easily reducible to this MPCP by setting $\alpha_0$ to the empty string.

**Theorem 8.** *Deduction is undecidable in general for rule-3 graph-embedded TRS.*

*Proof.* Let $P = \{(\alpha_i, \beta_i) | i \in [1, n]\}$ be an instance of MPCP over the alphabet $\Gamma = \{a, b\}$ with the input string $\alpha_0 \in \Gamma^*$. We can convert this MPCP problem into the TRS setting. First, let $f$ be a binary function symbol and let $a$ and $b$ be constants, and let $d_1, \dots, d_n$, be public constants, one for each string pair of the MPCP. We can convert a string over $\Gamma$ into a term using $f$, $a$ and $b$ in a recursive fashion. For $\gamma \in \Gamma^+$ and $x \in V$, let $\tilde{\gamma}(x)$ denote the term version defines as follows: If $\gamma = a$ (or $b$) then $\tilde{\gamma}(x) = f(a, x)$ (likewise $\tilde{\gamma}(y) = f(b, y)$). If
$\gamma = a \cdot \gamma'$ then $\tilde{\gamma}(x) = f(a, \tilde{\gamma}(x))$. Let $lck$ (for locked), $ulck$ (for unlocked), and $d$, $d_i$ ($0 \le i \le n$) be public constants. Now, construct a TRS, $R$, as follows: for each pair $\{ (\alpha_i, \beta_i) | i \in [1, n] \}$ we create the rule

$$f(f(f(ulck, v), f(d_i, x)), f(\tilde{\alpha}_i(y), \tilde{\beta}_i(z))) \rightarrow f(f(f(ulck, v), x), f(y, z))$$

Add one final “locking” rule to $R$:

$$f(f(f(ulck, f(lck, v)), f(d_0, x)), f(y, y)) \rightarrow f(f(f(ulck, v), x), f(y, y)).$$

The $d_i$ ensure there are no critical pairs between rules and thus we have a convergent TRS. In addition, note that each rule in $R$ can be obtained by using just rule-3 (and rule-2 to remove extra terms). That is, $\forall l \rightarrow r \in R, l \rightarrow_{(3),(2)}^+ r$.

Now for the MPCP instance, construct the frame $\phi = \nu \tilde{n} \cdot \sigma$ with $\tilde{n} = \{c, e\}$ and $\sigma = \{v \mapsto f(ulck, f(lck, e)), x \mapsto \tilde{\alpha}_0(c)\}$. Likewise, construct a deduction problem with the target term $M = f(f(ulck, e), d), f(c, c)$.

First, suppose there exists a recipe term, $t$, such that $t\sigma \downarrow_R = M$. Then the first rule that must be applied is the unlocking rule, since it is required before any of the other rules can be applied. The unlocking rule also ensures that the two strings are equal. Next, each remaining rewrite step corresponds to a single string pair from the MPCP, ensuring the recipe corresponds to a solution. The solution can be extracted from the indexes of each of the $d_i$ constants occurring in the rewrite derivation.

Second, it also easy to see that if there is a solution to the MPCP we can from that solution construct a recipe to deduce $M$. For example, if the solution is $i_1, \dots, i_k \in [1, n]$. Then, a recipe would be:

$$t = f(f(v, f(d_0, f(d_{i_1}, f(\dots, f(d_{i_k}, d))))), f(\tilde{\alpha}(x), \tilde{\beta}(x)))$$

where $\alpha_{i_1} \alpha_{i_2} \dots \alpha_{i_k} = \alpha' \cdot \alpha_0 = \beta' \cdot \alpha_0 = \beta_{i_1} \beta_{i_2} \dots \beta_{i_k}$ □

# 5 Conclusions

In this paper, we have extended the combination result from [19], providing decision procedures for the problems of deduction and static equivalence in the combination $R \cup E$, where $R$ is contracting and $E$-convergent. This improves upon the previous result, which required $R$ to be subterm $E$-convergent.

We also examined the gap between two extensions of subterm TRSs, contracting and graph-embedded, with respect to the decidability of knowledge problems. We showed that several natural attempts to narrow this gap while preserving decidability fail, leading to TRSs with undecidable knowledge problems. Nevertheless, it remains plausible that a class of systems closer to graph-embedded than contracting could be defined in a way that maintains decidability. Identifying the best approach to achieve this remains an open question.

Regarding the undecidability proof for deduction in rule-3 TRSs, we note that since the terms involve a single non-constant function symbol, rule-3 behaves similarly to rule-4. It would be interesting to investigate whether this proof could be adapted to avoid relying on the presence of a single function symbol.
References

1. Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367(1-2), 2-32 (2006)

2. Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Hankin, C., Schmidt, D. (eds.) Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001. pp. 104–115. ACM (2001)

3. Armando, A., Basin, D.A., Boichut, Y., Chevalier, Y., Compagna, L., Cuéllar, J., Drielsma, P.H., Héam, P., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, Proceedings. Lecture Notes in Computer Science, vol. 3576, pp. 281–285. Springer (2005)

4. Ayala-Rincón, M., Fernández, M., Nantes-Sobrinho, D.: Intruder deduction problem for locally stable theories with normal forms and inverses. Theor. Comput. Sci. 672, 64–100 (2017)

5. Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, New York, NY, USA (1998)

6. Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445–532. Elsevier and MIT Press (2001)

7. Baudet, M., Cortier, V., Delaune, S.: YAPA: A generic tool for computing intruder knowledge. ACM Trans. Comput. Log. 14(1), 4 (2013)

8. Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada. pp. 82–96. IEEE Computer Society (2001)

9. Bunch, C., Satterfield, S.D., Erbatur, S., Marshall, A.M., Ringeissen, C.: Knowledge problems in protocol analysis: Extending the notion of subterm convergent (2025), https://arxiv.org/abs/2401.17226

10. Chadha, R., Cheval, V., Ciobâcă, S., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log. 17(4), 23:1–23:32 (2016)

11. Ciobâcă, S., Delaune, S., Kremer, S.: Computing knowledge in security protocols under convergent equational theories. J. Autom. Reasoning 48(2), 219–262 (2012)

12. Cohn-Gordon, K., Cremers, C., Garratt, L., Millican, J., Milner, K.: On ends-to-ends encryption: Asynchronous group messaging with strong security guarantees. In: Lie, D., Mannan, M., Backes, M., Wang, X. (eds.) Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018. pp. 1802–1819. ACM (2018)

13. Conchinha, B., Basin, D.A., Caleiro, C.: FAST: an efficient decision procedure for deduction and static equivalence. In: Schmidt-Schauß, M. (ed.) Proceedings of RTA 2011, Novi Sad, Serbia. LIPIcs, vol. 10, pp. 11–20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)

14. Cortier, V., Delaune, S.: Decidability and combination results for two notions of knowledge in security protocols. Journal of Automated Reasoning 48(4), 441–487 (2010). https://doi.org/10.1007/s10817-010-9208-8, http://dx.doi.org/10.1007/s10817-010-9208-8
15. Cremers, C.J.F.: The Scyther tool: Verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings. Lecture Notes in Computer Science, vol. 5123, pp. 414-418. Springer (2008)

16. Dwyer Satterfield, S., Erbatur, S., Marshall, A.M., Ringeissen, C.: Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories. In: Gaboardi, M., van Raamsdonk, F. (eds.) 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol. 260, pp. 30:1–30:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2023). https://doi.org/10.4230/LIPIcs.FSCD.2023.30, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.30

17. Erbatur, S., Marshall, A.M., Narendran, P., Ringeissen, C.: Deciding knowledge problems modulo classes of permutative theories. In: Bowles, J., Søndergaard, H. (eds.) Logic-Based Program Synthesis and Transformation - 34th International Symposium, LOPSTR 2024, Milan, Italy, September 9-10, 2024, Proceedings. Lecture Notes in Computer Science, vol. 14919, pp. 47–63. Springer (2024). https://doi.org/10.1007/978-3-031-71294-4_3, https://doi.org/10.1007/978-3-031-71294-4_3

18. Erbatur, S., Marshall, A.M., Ringeissen, C.: Notions of knowledge in combinations of theories sharing constructors. In: de Moura, L. (ed.) Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, Proceedings. LNCS, vol. 10395, pp. 60–76. Springer (2017)

19. Erbatur, S., Marshall, A.M., Ringeissen, C.: Computing knowledge in equational extensions of subterm convergent theories. Math. Struct. Comput. Sci. 30(6), 683–709 (2020)

20. Escobar, S., Meadows, C.A., Meseguer, J.: Maude-NPA: Cryptographic protocol analysis modulo equational properties. In: Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures. Lecture Notes in Computer Science, vol. 5705, pp. 1–50. Springer (2007)

21. Jouannaud, J., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986). https://doi.org/10.1137/0215084, http://dx.doi.org/10.1137/0215084

22. Kirchner, C., Klay, F.: Syntactic theories and unification. In: Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on Logic in Computer Science. pp. 270–277 (Jun 1990). https://doi.org/10.1109/LICS.1990.113753

23. Lynch, C., Morawska, B.: Basic syntactic mutation. In: Voronkov, A. (ed.) Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2392, pp. 471–485. Springer (2002)

24. Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proceedings of the 8th ACM Conference on Computer and Communications Security. pp. 166–175. CCS'01, ACM, New York, NY, USA (2001). https://doi.org/10.1145/501983.502007, http://doi.acm.org/10.1145/501983.502007

25. Mödersheim, S., Viganò, L.: The open-source fixed-point model checker for symbolic analysis of security protocols. In: Foundations of Security Analysis and Design
V, FOSAD 2007/2008/2009 Tutorial Lectures. Lecture Notes in Computer Science, vol. 5705, pp. 166–194. Springer (2009)

26. Narendran, P., Otto, F.: Single versus simultaneous equational unification and equational unification for variable-permuting theories. J. Autom. Reason. **19**(1), 87–115 (1997)

27. Nguyen, K.: Formal verification of a messaging protocol. Internship report (2019), work done under the supervision of Vincent Cheval and Véronique Cortier

28. Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Computer Security **6**, 85–128 (1998)

29. Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties. In: Chong, S. (ed.) 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012. pp. 78–94. IEEE Computer Society (2012)

30. Turuani, M.: The CL-Atse protocol analyser. In: Pfenning, F. (ed.) Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings. Lecture Notes in Computer Science, vol. 4098, pp. 277–286. Springer (2006)