Serdar Erbatur

Andrew M Marshall

Christophe Ringeissen

Computing Knowledge in Equational Extensions of Subterm Convergent Theories

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.

Introduction

The formal analysis of security protocols is nowadays widely investigated. One of its starting points is the paradigm initiated by Dolev and Yao [START_REF] Dolev | On the security of public key protocols (extended abstract)[END_REF] where term algebras modulo some equational theories are used to represent messages built over cryptographic primitives.

Several automated tools for the analysis of security issues in protocols have been developed, including [START_REF] Cheval | The DEEPSEC prover[END_REF][START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and ProVerif[END_REF][START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF][START_REF] Ciobâcȃ | Computing knowledge in security protocols under convergent equational theories[END_REF][START_REF] Schmidt | Automated analysis of diffie-hellman protocols and advanced security properties[END_REF][START_REF] Mödersheim | The open-source fixed-point model checker for symbolic analysis of security protocols[END_REF][START_REF] Cremers | The Scyther tool: Verification, falsification, and analysis of security protocols[END_REF][START_REF] Escobar | Maude-NPA: Cryptographic protocol analysis modulo equational properties[END_REF][START_REF] Turuani | The CL-Atse protocol analyser[END_REF][START_REF] Armando | The AVISPA tool for the automated validation of internet security protocols and applications[END_REF][START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF]. All these tools make use of decision procedures related to constraint solving in term algebras.

Verifying the security of protocols requires the development of specific decision procedures to reason about the knowledge of an intruder. Two important measures of this knowledge are (intruder) deduction [START_REF] Paulson | The inductive approach to verifying cryptographic protocols[END_REF][START_REF] Millen | Constraint solving for bounded-process cryptographic protocol analysis[END_REF] and static equivalence [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]. The deduction problem is the question of whether an intruder, given their deductive capability and a sequence of messages representing their knowledge, can obtain some secret. This is a critical measure of the capability of the protocol to maintain secrets. Deducibility is needed for many questions about the security of protocols. However, there are some questions for which we need to be able to decide more than deducibility. For some protocols, in addition to deducibility, we would like to determine whether an intruder can distinguish between different runs of the protocol. For example, in protocols which attempt to transmit encrypted votes, we would like to know if, to the attacker, two different votes are indistinguishable. Static equivalence measures this property.

Much work has gone into investigating and developing decision procedures for the deduction and the static equivalence problems [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF][START_REF] Conchinha | FAST: an efficient decision procedure for deduction and static equivalence[END_REF][START_REF] Ciobâcȃ | Computing knowledge in security protocols under convergent equational theories[END_REF][START_REF] Baudet | YAPA: A generic tool for computing intruder knowledge[END_REF][START_REF] Ayala-Rincón | Intruder deduction problem for locally stable theories with normal forms and inverses[END_REF][START_REF] Erbatur | Notions of knowledge in combinations of theories sharing constructors[END_REF]. In this line of research, the security protocols are often represented by equational theories usually defined as unions of several simpler sub-theories. In this paper, we focus on decision procedures for the deduction problem and the static equivalence problem in equational theories T ∪ E where T and E are possibly non-disjoint. Until now, decision procedures for these problems have been obtained under the following assumptions:

-T is given by a subterm convergent term rewrite system, and E is empty [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]; -T and E are disjoint [START_REF] Cortier | Decidability and combination results for two notions of knowledge in security protocols[END_REF] and both deduction and static equivalence are decidable in T and in E; -T and E share only constructors [START_REF] Erbatur | Notions of knowledge in combinations of theories sharing constructors[END_REF] and both deduction and static equivalence are decidable in T and in E.

In this paper, we investigate a new scenario:

-T is given by a term rewrite system R which is both subterm and convergent modulo E, and E is an arbitrary equational theory.

We then have two cases, based on E. The first case follows our preliminary results in [START_REF] Erbatur | Knowledge problems in equational extensions of subterm convergent theories[END_REF] where we are able to show that the methods of [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] can be extended to rewrite systems that are both subterm and convergent modulo E for a simple but significant class of E theories. In the second case, the previous method is insufficient and a new approach is developed that extends to a broader class of E theories. We focus on permutative theories E, such as the Commutativity C = {x+y = y+x} or the Associativity-Commutativity AC = {(x+y)+z = x+(y+z), x+y = y + x}. Permutative theories are commonly used as background theories E in term rewrite systems modulo E. In a permutative theory, the number of occurrences of a symbol on the left-hand side of an axiom is equal to the number of occurrences on the right. These theories also have a number of nice properties, such as being finite, and having decidable word and matching problems. However, the unification problem in general is undecidable in permutative theories even if there are important particular permutative theories with a decidable unification problem, such as C and AC. We investigate the following two classes of permutative theories:

-The first class corresponds to shallow permutative theories. In that particular case, a permutative theory must be shallow, meaning that a variable can only occur at depth 1 in the axioms of the theory. Thus, C is a typical example of a shallow permutative theory. We show that this class of theories admits decision procedures for deduction and static equivalence which are based on some reductions to the empty theory. In that simple case, it is possible to reuse the same proof techniques as the ones developed for the case of subterm convergent term rewrite systems [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF][START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]. -The second class consists of syntactic permutative theories. A syntactic theory admits a complete unification procedure defined as a non-necessarily terminating extension of syntactic unification with finitely many additional mutation rules. According to [START_REF] Kirchner | Syntactic theories and unification[END_REF], any permutative theory with a finitary unification problem is indeed syntactic permutative. Thus, AC is syntactic permutative, but it is not shallow due to the Associativity axiom. For this general case of syntactic permutative theories, we develop a new approach based on the computation of a Complete set of E-Matched Terms, CMT for short. We show that E-matched terms relate to an appropriate notion of E-variant. Here, an E-variant is a generalization of a normalized variant, as defined in the literature, in the restricted case where E is given by a convergent rewrite system [START_REF] Comon-Lundh | The finite variant property: How to get rid of some algebraic properties[END_REF]. We present a method called MTG to generate a CMT . In general MTG is not necessarily terminating. However, we identify a class of syntactic permutative theories, namely the permutative theories closed by paramodulation, for which MTG always terminates by computing a finite CMT . Thus, MTG is instrumental in showing that any permutative theory closed by paramodulation has the Finite Equational Variant Property, defined here and denoted by FEVP. Even if the MTG procedure does not terminate it may still be possible to find a finite CMT for all the lefthand sides of a rewrite system R. In this case it is then possible to define an appropriate notion of size of R modulo E, which is of prime interest to solve the knowledge problems in R ∪ E. Actually we show that both deduction and static equivalence in R ∪ E are decidable if they are decidable in E, the size of R modulo E is computable, and R is subterm and convergent modulo E. Compared to the shallow case, this second approach substantially differs from the ones developed in [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF][START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]. However, we are able to reuse some combination techniques introduced for solving the knowledge problems in unions of theories [START_REF] Cortier | Decidability and combination results for two notions of knowledge in security protocols[END_REF][START_REF] Erbatur | Notions of knowledge in combinations of theories sharing constructors[END_REF]. Indeed, our reduction methods require that we implement decision procedures for deduction and static equivalence in the combination of E with additional free function symbols. Thankfully, this is always possible due to the combination result in [START_REF] Cortier | Decidability and combination results for two notions of knowledge in security protocols[END_REF].

Main Contributions

The primary contributions of this paper are:

-A new method that solves both the deduction and static equivalence problems in R ∪ E where R is a subterm rewrite system and R is convergent modulo a shallow permutative theory E (cf. Theorem 1).

-The introduction of the notion of complete set of E-matched terms (CMT ) and a method called MTG generating a CMT for the case E is syntactic permutative. If MTG always terminates by computing a finite CMT , then there are two important consequences: (1) E has the Finite Equational Variant Property (FEVP) considered in this paper, and (2) the size of R modulo E is computable for any rewrite system R. We show that MTG is terminating for the class of permutative theories closed by paramodulation, and so all these theories have the FEVP (cf. Theorem 2). -A new method that solves both the deduction and static equivalence problems in R ∪ E if R is a subterm rewrite system, R is convergent modulo a syntactic permutative theory E, the size of R modulo E is computable, and both deduction and static equivalence are decidable in E (cf. Theorem 3). Compared to the simple case of a shallow permutative theory E, notice that the general case of a syntactic permutative theory E requires some additional assumptions: the computability of the size of R modulo E and the decidability of both deduction and static equivalence in E.

Plan of the Paper

The paper is organized as follows. The concepts and notations used in this paper can be found in Section 2. The equational theories we focus on are exemplified in Section 3. These theories are of the form R ∪ E, where the rewrite system R is both subterm and convergent modulo a syntactic permutative theory E. Section 4 presents the decision procedures for deduction and static equivalence in R ∪ E for the particular case in which E is shallow permutative. Starting from Section 5, we investigate the general case in which E is syntactic permutative. At the beginning of Section 5, we introduce the notion of complete set of Ematched terms (CMT ) and discuss how a (finite) CMT can be related to a (finite) complete set of E-variants. The MTG method for generating a CMT is presented in Section 5.1. As shown in Section 5.2, MTG terminates and generates a finite CMT for the class of permutative theories closed by paramodulation. Section 6 introduces the key notion of size of R modulo E, which is well-defined when each left-hand side of R admits a finite CMT . Then we show how to reduce any deduction (resp., static equivalence) problem in R ∪ E into a deduction (resp., static equivalence) problem in E, provided that the size of R modulo E is computable. For both classes of permutative theories, shallow (Section 4) and syntactic (Section 6), we detail the correctness proofs of the related decision procedures. Finally, we discuss in Section 7 some possible lines of future work.

Preliminaries

We assume that the reader is familiar with equational logic and term rewriting. We use the standard notations as presented in [START_REF] Baader | Term rewriting and all that[END_REF]. In addition, as in [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF], we use some concepts, such as names and frames, borrowed from the applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF].

Terms and Substitutions

Given a first-order signature Σ, a set of names is a countable set of (free) constants N , such that Σ ∩ N = ∅. Given a (countable) set of variables X, the set of (Σ ∪ N )-terms over X is denoted by T (Σ ∪ N, X). The set of variables in a term t is denoted by f v(t) and the set of names in t is denoted by f n(t).

A term t is ground if f v(t) = ∅.
For any position p in a term t (including the root position ), t(p) denotes the symbol at position p, t| p denotes the subterm of t at position p, and t[u] p denotes the term t in which t| p is replaced by u.

The size of a term t is denoted by |t| and defined in the usual way as follows:

|f (t 1 , . . . , t n )| = 1+ n i=1 |t i | if f is a n-ary function symbol with n ≥ 1, |c| = 1 if c ∈ N , and |x| = 0 if x ∈ X. Given any Σ ⊆ Σ, a term t is said to be Σ -rooted if t( ) ∈ Σ . A context,
s, is a first-order term with "holes", or distinguished variables that occur only once. We may write s [x 1 , . . . , x n ], to illustrate that the context s contains n distinguished variables.

A substitution σ is an endomorphism of T (Σ ∪ N, X) with only finitely many variables not mapped to themselves, denoted by σ = {x 1 → t 1 , . . . , x m → t m }. Application of a substitution σ to a term t is written as tσ. Given two substitutions θ and σ, the composition σ • θ is the substitution denoted here by θσ and defined such that x(θσ) = (xθ)σ for any x ∈ X. The domain of σ is

Dom(σ) = {x ∈ X | xσ = x}. The range of σ is Ran(σ) = {xσ | x ∈ Dom(σ)}.
When θ and σ are two substitutions with disjoint domains and only ground terms in their ranges, then θσ = θ ∪ σ. Given a substitution σ and a finite set of variables V ⊆ X, the restriction of σ to V is the substitution denoted by σ |V such that xσ |V = xσ for any x ∈ V and xσ |V = x for any x ∈ X\V .

Equational Theories

Given a set E of Σ-axioms (i.e., pairs of Σ-terms, denoted by l = r), the equational theory = E is the congruence closure of E under the law of substitutivity. For any Σ-term t, the equivalence class of t with respect to = E is denoted by [t] E . Since Σ ∩ N = ∅, the Σ-equalities in E do not contain any names in N . A theory E is trivial if x = E y, for two distinct variables x and y. In this paper, all the considered theories are assumed non-trivial.

An E-unification problem with free constants in N is a set of Σ ∪N -equations P = {s 1 = ? t 1 , . . . , s m = ? t m }. The set of variables in P is denoted by f v(P ). A solution to P , called an E-unifier , is a substitution σ such that s i σ = E t i σ for all 1 ≤ i ≤ m. A substitution σ is more general modulo E than θ on a set of variables V , denoted as σ ≤ V E θ, if there is a substitution τ such that xστ = E xθ for all x ∈ V . A Complete Set of E-Unifiers of P , denoted by CSU E (P ), is a set of substitutions such that each σ ∈ CSU E (P ) is an E-unifier of P , and for each E-unifier θ of P , there exists σ ∈ CSU E (P ) such that σ ≤ f v(P ) E θ. E-unification is said to be finitary if any E-unification problem P admits a finite CSU E (P ). An E-unification problem P = {x 1 = ? t 1 , . . . , x m = ? t m } is a solved form if x 1 , . . . , x m are variables occurring once in P , and in that case the corresponding substitution µ P = {x 1 → t 1 , . . . , x m → t m } is an E-unifier of P such that {µ P } is a CSU E (P ). When E is empty, E-unification is called syntactic unification and has the property of being unitary: if two terms s and t are syntactically unifiable, then there exists a CSU E (s = ? t) of cardinality 1 whose element is called a most general unifier of s = ? t denoted by mgu(s, t).

A match-equation over Σ∪N is a Σ∪N -equation s = ? t such that t is ground, also denoted by s ≤ ? t. An E-matching problem (with free constants in N ) is a set of match-equations over Σ ∪ N . An E-word problem (with free constants in N ) is a set of ground Σ ∪ N -equations. Thus, any E-matching problem and any E-word problem is defined as a particular E-unification problem with free constants. As a usual practice, a variable x may also occur in the right-hand side of a match-equation. In that case, the variable x is said to be a subject variable, which is considered as a free constant in the related unification problem, meaning that any E-unifier σ must satisfy the additional constraint xσ = x.

Let us introduce the different classes of theories considered in the paper. An axiom l = r is regular if l and r have the same set of variables. An axiom l = r is collapse-free if l and r are non-variable terms. An equational theory is regular (resp., collapse-free) if all its axioms are regular (resp., collapse-free). An equational theory E is finite if for each term t, there are only finitely many terms s such that t = E s. Matching in finite theories is finitary. A finite theory is necessarily regular and collapse-free. A sufficient condition to get a finite theory is to assume that E is permutative. An equational theory E is permutative if for each axiom l = r in E, l and r contain the same symbols with the same number of occurrences. Well-known theories such as Associativity (A = {(x + y) + z = x + (y + z)}), Commutativity (C = {x + y = y + x}), and Associativity-Commutativity (AC = A ∪ C) are permutative theories. The word problem and matching are both decidable in finite theories, and so in permutative theories. However, unification in permutative theories is undecidable in general [START_REF] Schmidt-Schauß | Unification in permutative equational theories is undecidable[END_REF].

Notions of Knowledge

The applied pi calculus and frames are used to model attacker knowledge [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. 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(σ) of the frame φ = ν ñ.σ, where σ is a substitution such that the terms of Ran(σ) are ground. 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. We need to track the names the attacker knows, such as public values, as well as the names the attacker does not know, such as freshly generated nonces. In a frame φ = ν ñ.σ, ñ consists of a finite set of restricted names and represents names which remain secret from the attacker. The set of names occurring in a term t is denoted by f n(t).

Given a frame φ = ν ñ.σ and a term t, tφ denotes by a slight abuse of notation the term tσ. We say that a term t satisfies the name restriction (of φ) if f n(t) ∩ ñ = ∅. In this paper we start with the Abadi and Cortier notation, introduced below, for deduction and static equivalence. However, deduction and related problems have been studied before [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF], see for example [START_REF] Amadio | On the reachability problem in cryptographic protocols[END_REF].

Definition 1 (Deduction). Let φ = ν ñ.σ be a frame, and t a ground term. We say that t is deduced from φ modulo E, denoted by φ E t, if there exists a term s such that sσ = E t and f n(s) ∩ ñ = ∅. The term s is called a recipe of t in φ modulo E. When φ and E are clear from the context, a recipe of t is usually denoted by ζ t .

Another form of knowledge is the ability to tell if two frames are statically equivalent modulo E, sometimes also called indistinguishability.

Definition 2 (Static Equivalence). Two terms s and t are equal in a frame φ = ν ñ.σ modulo an equational theory E, denoted (s = E t)φ, if sσ = E tσ, and ñ ∩ (f n(s) ∪ f n(t)) = ∅. The set of all equalities s = t such that (s = E t)φ is denoted by Eq(φ). Given a set of equalities Eq, the fact that (s = E t)φ for any s = t ∈ Eq is denoted by φ |= Eq. Two frames φ = ν ñ.σ and ψ = ν ñ.τ are statically equivalent modulo E, denoted as φ ≈ E ψ, if Dom(σ) = Dom(τ ), φ |= Eq(ψ) and ψ |= Eq(φ).

Both deduction and static equivalence are known to be decidable in subterm convergent rewrite systems [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]. In this paper, we lift these results to term rewrite systems that are subterm convergent modulo some permutative theories.

Term Rewrite Systems

A term rewrite system (TRS) is a pair (Σ, R), where Σ is a signature and R is a finite set of rewrite rules of the form l → r, such that l, r are Σ-terms, l is not a variable and f v(r) ⊆ f v(l). When the signature is clear from the context, a TRS is simply denoted by R. A term s rewrites to a term t, denoted by s → R t (or simply s → t), if there exists a position p of s, a rule l → r ∈ R, and a substitution σ such that s| p = lσ and t = s[rσ] p . A term s is a normal form with respect to the relation → R (or simply a normal form), if there is no term t such that s → R t. This notion is lifted to substitutions as follows: a substitution σ is normalized if, for every variable x in the domain of σ, xσ is a normal form. A TRS R is terminating if there are no infinite reduction sequences with respect to → R . A TRS R is confluent if, whenever t → * R s 1 and t → * R s 2 , there exists a term w such that s 1 → * R w and s 2 → * R w. A confluent and terminating TRS is called convergent. In a convergent TRS R, any term t admits a unique R-normal form denoted by t↓ R . A TRS R is said to be subterm if for any l → r ∈ R, r is either a strict subterm of l or a ground R-irreducible term. A TRS is subterm convergent if it is both subterm and convergent. An equational theory E is subterm convergent if there exists a subterm convergent TRS R such that = E is ↔ * R . The size of a TRS R is denoted by |R| and defined as follows: |R| = max {l→r∈R} |l|. Since a variable cannot occur as the left-hand side of any rule in R, we have that |R| ≥ 1 for any non-empty TRS R. When R is empty, we define |R| = 1.

Let us now introduce the notion of equational rewriting, also called class rewriting [START_REF] Jouannaud | Completion of a set of rules modulo a set of equations[END_REF]. Given a TRS R and an equational theory E, the rewrite relation of R modulo E is defined as follows: s → R,E t if there exist some position p in s, some rule l → r ∈ R and a substitution µ such that s| p = E lµ and t

= s[rµ] p . The TRS R is said to be E-convergent if the relation = E • → R • = E is terminating and ←→ * R∪E ⊆ → * R,E • = E • ← * R,E .
In an E-convergent TRS R, any term t admits a unique R-normal form modulo E denoted by t ↓ R,E , and for any terms s and t, we have s

←→ * R∪E t iff (s ↓ R,E ) = E (t ↓ R,E
). In this paper, we focus on the following E-convergent TRSs. Definition 3. A subterm E-convergent TRS is a TRS which is both subterm and E-convergent.

A reduction ordering is a well-founded ordering on terms closed under context and substitution. Consider an inference system I whose each inference rule is of the form e 1 , . . . , e n e n+1 where both the premises e 1 , . . . , e n and the conclusion e n+1 are equalities. Let us assume a reduction ordering < with the additional property of being total on ground terms. To define a notion of redundancy with respect to <, we extend < to an ordering on equalities using the multiset extension of < to compare equalities viewed as multisets of terms. In a set of ground equalities E, an inference with premises in E is said to be redundant if its conclusion follows from the equalities of E that are smaller than its largest premise. In an arbitrary set of equalities E, an inference with premises in E is redundant if it is redundant in the set of all ground instances of E. A set of equalities is saturated with respect to I if all the inferences of I with premises in E are redundant.

Syntactic Theories

A theory E is syntactic if it has a finite resolvent presentation S, that is a finite set of equational axioms S such that each equality t = E u has an equational proof t ↔ * S u with at most one step ↔ S applied at the root position. The theory C and AC are permutative and syntactic [START_REF] Kirchner | Syntactic theories and unification[END_REF].

The interest of syntactic theories is to admit a mutation-based unification procedure that bears similarities with the standard syntactic unification procedure. In addition to the classical decomposition rule, additional mutation rules are needed. This leads to a mutation-based unification procedure which is not necessarily terminating for all syntactic theories. When restricting to the matching problem, it is possible to get termination for a large class of theories of practical interest. Actually, a mutation-based matching algorithm for the class of syntactic permutative theories has been presented in [START_REF] Nipkow | Proof transformations for equational theories[END_REF]. In Fig. 1, we consider a rule-based description of this matching algorithm borrowed from [START_REF] Ringeissen | Building and combining matching algorithms[END_REF]. It will be applied in Section 6 to possibly compute a finite representation of terms matched by the left-hand sides of a term rewrite system. Lemma 1. Assume S is a finite resolvent presentation of any syntactic permutative theory E. The MSP inference system given in Fig. 1 provides a sound, complete and terminating E-matching procedure: the set of computed solved forms corresponds to a complete set of solutions.

MatchDec {f (s1, . . . , sm) ≤ ? f (t1, . . . , tm)} ∪ P {s1 ≤ ? t1, . . . , sm ≤ ? tm} ∪ P MatchMut {f (s1, . . . , sm) ≤ ? g(t1, . . . , tn)} ∪ P {r1 ≤ ? t1, . . . , rn ≤ ? tn, s1 = ? l1, . . . , sm = ? lm} ∪ P where f (l1, . . . , lm) = g(r1, . . . , rn) is a fresh variant of an axiom in S.

Rep { x ≤ ? u, t = ? t } ∪ P { x ≤ ? u, t = ? t {x → u} } ∪ P where x ∈ f v(t ).
RemEq {t = ? t } ∪ P {t ≤ ? t } ∪ P where t is ground.

Merge {x ≤ ? t, x ≤ ? s} ∪ P {x ≤ ? t, s ≤ ? t} ∪ P Notice that all possible derivations must be explored when MatchMut is applicable in the case f = g or when both MatchDec and MatchMut are applicable on the same match-equation in the case f = g. Mutation-based unification algorithms are known for some important subclasses of syntactic theories, such as shallow theories [START_REF] Comon | Syntacticness, cyclesyntacticness, and shallow theories[END_REF], and theories closed by paramodulation [START_REF] Lynch | Basic syntactic mutation[END_REF]. These particular syntactic theories play a central role in the paper and are defined as follows.

A theory E is shallow if variables can only occur at a depth at most 1 in axioms of E. For instance, C is a shallow theory but AC is not.

To define the property of being closed by paramodulation, we rely on the notion of saturation introduced at the end of Section 2.4 with respect to a reduction ordering < which is assumed to be total on ground terms. An equational theory E is closed by paramodulation if E is a finite set of equalities saturated with respect to the inference system including the single rule

Paramodulation s[l ] = t, l = r s[r]σ = tσ
where l = r is a fresh instance of an equality in E, σ = mgu(l , l), lσ < rσ and l is not a variable. Applying the paramodulation rule to an equality in E produces a new equality which is then added to the set. Thus, an equational theory is saturated by paramodulation when, after exhaustive applications of the above rule, no further non-redundant equalities are added (see Section 2.4 for the description of redundant). The set is finitely saturated by paramodulation if only a finite number of new, non-redundant equalities are added. The theory C is closed by paramodulation, while AC is not. The following permutative theories are not shallow but closed by paramodulation:

-{i(x) + y = i(y) + x}, -{i(x) + y = i(y) + x, x * i(y) = y * i(x)}.
As shown in [START_REF] Lynch | Basic syntactic mutation[END_REF], the class of theories closed by paramodulation admits a terminating mutation-based unification procedure. For these theories applying mutation on terms previously introduced by mutation will only generate superfluous unifiers. To take into account this property, the idea initiated in [START_REF] Lynch | Basic syntactic mutation[END_REF] is to consider a marking notation, terms boxing, such that terms generated by mutation are boxed and no further mutations are applied on boxed terms. Thus, any mutation reduces a complexity measure counting the number of unboxed symbols, where a symbol is said to be boxed if it occurs in a boxed term. This complexity measure is used to prove termination of a mutation-based unification procedure for theories closed by paramodulation [START_REF] Lynch | Basic syntactic mutation[END_REF]. Along the lines of [START_REF] Lynch | Basic syntactic mutation[END_REF] it is possible to obtain a matching algorithm for permutative theories closed by paramodulation called MSP B and defined in the same way as MSP except MatchMut which is replaced by its boxed version:

MatchMut B {f (s 1 , . . . , s m ) ≤ ? g(t 1 , . . . , t n )} ∪ P { r 1 ≤ ? t 1 , . . . , r n ≤ ? t n , s 1 = ? l 1 , . . . , s m = ? l m } ∪ P where f (s 1 , . . . , s m ) is unboxed and f (l 1 , . . . , l m ) = g(r 1 , . . . , r n ) is a fresh vari- ant of an axiom in S.
Compared to MSP, the interest of MSP B is to generate a reduced search space without loss of completeness for permutative theories closed by paramodulation.

Subterm Equational Convergent Rewrite Systems

From now on, let us consider (Ω ∪Σ, RE) = (Ω ∪Σ, R ∪E) where (Ω ∪Σ, R) is a TRS modulo a permutative theory (Σ, E) such that Ω ∩ Σ = ∅ and R is subterm E-convergent. Hence, E can be a permutative theory such as C or AC. The fact that R is E-convergent implies the uniqueness of normal forms modulo E and the decidability of the word problem modulo RE: for any terms s and t, we have

s = RE t iff (s ↓ R,E ) = E (t ↓ R,E
). In the following, a term or a substitution is said to be normalized if it is normalized w.r.t → R,E , and a frame is normalized if its substitution is normalized.

In the rest of this section, we present some examples of theories RE such that R is subterm E-convergent (Section 3.1), and we introduce the notion of subterms modulo E (Section 3.2).

Examples

A Theory for a Messaging Protocol

Let us start with a theory used in practice to model a group messaging protocol. The Asynchronous Racheting Tree protocol specified in [START_REF] Cohn-Gordon | On endsto-ends encryption: Asynchronous group messaging with strong security guarantees[END_REF] has been studied in [START_REF] Nguyen | Formal verification of a messaging protocol[END_REF] using ProVerif [START_REF] Cheval | A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif[END_REF][START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and ProVerif[END_REF]. The goal of this protocol is to provide encrypted group messaging by maintaining some strong security guarantees. For this protocol, the theory modeling the intruder is defined in [START_REF] Nguyen | Formal verification of a messaging protocol[END_REF] as a combination R ENC ∪ K where R ENC and K are as follows:

R ENC =        adec(aenc(m, pk (sk)), sk) → m getmsg(sign(m, sk)) → m checksign(sign(m, sk), m, pk (sk)) → ok sdec(senc(m, k), k) → m        K = keyexch(x, pk (x ), y, pk (y )) = keyexch(x , pk (x), y , pk (y))
The combination R ENC ∪ K is non-disjoint since the function symbol pk is shared by R ENC and K. More precisely, pk satisfies an appropriate notion of shared constructor, and so the combination method described in [START_REF] Erbatur | Notions of knowledge in combinations of theories sharing constructors[END_REF] applies to R ENC ∪ K. Another possibility is to apply the reduction method presented in Section 6 using the fact that R ENC is subterm K-convergent and K is a permutative theory closed by paramodulation.

Non-Associative Sub-Theories of Abelian Groups and Combinations

The theory of Abelian groups is AG = R AG ∪ AC( * ) where R AG denotes the following AC( * )-convergent TRS:

R AG =                x * e → x x * i(x) → e x * (y * i(x)) → y i(i(x)) → x i(e) → e i(x * y) → i(x) * i(y)
R AG is not subterm due to the rule i(x * y) → i(x) * i(y). Note that AG is an example of monoidal theory. Hence, the decidability of deduction and static equivalence in AG follows from the fact that these problems are decidable in monoidal theories [START_REF] Cortier | Decidability and combination results for two notions of knowledge in security protocols[END_REF].

The theory of Abelian Pre-Groups is APG = R APG ∪ C( * ) where R APG denotes the following subterm C( * )-convergent T RS:

R APG = {x * e → x, x * i(x) → e, i(i(x)) → x, i(e) → e}
In [START_REF] Yang | Theories of homomorphic encryption, unification, and the finite variant property[END_REF], APG was considered as an approximation to deal with unification in homomorphic encryption over Abelian groups.

We can actually extend the definition of APG to include an approximation of associativity in the following way. Define the theory of Abelian Pre-Groups with Associative Approximation by APGAA = R APGAA ∪ C( * ) where R APGAA is the following subterm C( * )-convergent T RS:

R APGAA = R AP G ∪ {(i(n) * x) * n → x, (n * x) * i(n) → x}
This theory is a mono-sorted version of the theory of Abelian Pre-Groups with Associative Approximation studied in [START_REF] Yang | Theories of homomorphic encryption, unification, and the finite variant property[END_REF]. As with APG, the motivation of studying APGAA in [START_REF] Yang | Theories of homomorphic encryption, unification, and the finite variant property[END_REF] is to approximate the theory of homomorphic encryption over Abelian groups in order to solve the unification problem using a variant-based approach (modulo C( * )). Note that APG and APGAA are not monoidal theories despite the fact that AG is.

The modular exponentiation theory can be defined as an extension of AG with two additional axioms:

exp(exp(x, y), z) = exp(x, y * z), exp(x, e) = x.
This theory is motivated by the Diffie-Hellman exponentiation and has been studied in [START_REF] Chevalier | Deciding the security of protocols with diffie-hellman exponentiation and products in exponents[END_REF]. The corresponding TRS

{exp(exp(x, y), z) → exp(x, y * z), exp(x, e) → x} ∪ R AG
is AC( * )-convergent but not subterm. It is possible to get interesting subterm approximations of modular exponentiation by considering APG and APGAA instead of AG. In that direction, the following two TRSs:

{exp(exp(x, y), i(y)) → x, exp(x, e) → x} ∪ R APG , {exp(exp(x, y), i(y)) → x, exp(x, e) → x} ∪ R APGAA are subterm C( * )-convergent.
To take into account more equational properties of modular exponentiation, these last two TRSs are more generally convergent modulo the enlarged background theory {exp(exp(x, y), z) = exp(exp(x, z), y)}∪ C( * ), which is actually a syntactic permutative theory and more precisely a permutative theory closed by paramodulation.

Exclusive Or, its Non-Associative Sub-Theories, and Combinations The theory of Exclusive Or is ACUN = R ⊕ ∪ AC(⊕) where R ⊕ denotes the following subterm AC(⊕)-convergent TRS:

R ⊕ = {x ⊕ 0 → x, x ⊕ x → 0, x ⊕ (x ⊕ y) → y}
ACUN is another example of monoidal theory, and so it follows that both deduction and static equivalence are decidable in ACUN [START_REF] Cortier | Decidability and combination results for two notions of knowledge in security protocols[END_REF]. Interestingly, the decidability of these problems was already shown in [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] for ACUN by using some ad-hoc decision procedures. The deduction problem for ACUN was also successfully studied in [START_REF] Comon-Lundh | Intruder deductions, constraint solving and insecurity decision in presence of exclusive or[END_REF][START_REF] Chevalier | An NP decision procedure for protocol insecurity with XOR[END_REF]. By omitting the Associativity axiom, we get that

{x ⊕ 0 → x, x ⊕ x → 0} is subterm C(⊕)-convergent.
Exclusive Or often appears as a sub-theory in the axiomatization of protocols. For example the following TRS is an axiomatization for the Needham-Schroeder-Lowe protocol:

R NSL = {pk(x, sk(x, y)) → y, sk(x, pk(x, y)) → y} ∪ R ⊕
Here the operators pk and sk are used to model public key encryption. The unification problem in R NSL ∪ AC(⊕) was studied in [START_REF] Sasse | Protocol analysis modulo combination of theories: A case study in Maude-NPA[END_REF]. Notice that R NSL is subterm AC(⊕)-convergent. Other examples of a disjoint combination of R ⊕ with a subterm convergent TRS have been considered in [START_REF] Dreier | Automated unbounded verification of stateful cryptographic protocols with exclusive OR[END_REF].

Quasigroups and Loops

A quasigroup is a binary groupoid, (Q, * ), such that every equation of the form x * y = z has a unique solution whenever two of the elements x, y, and z are specified. These have been axiomatized by the following identities [START_REF] Hullot | Canonical forms and unification[END_REF]:

x \ (xy) = y, x(x \ y) = y, (yx)/x = y, (y/x)x = y where \ and / are the left and right division operations and are used to denote the unique solutions of the equation x * y = z, i.e, y = x \ z and x = z/y. A loop is a quasigroup with a unit element. When the commutative axiom is added for multiplication, we do not need two unique divisors and can replace them by a system with a single divisor, here denoted by x|y. For example, with the following axiomatization:

{(x * y)|x = y, x * (y|x) = y} ∪ {x * y = y * x} the corresponding subterm C( * )-convergent rewrite system is {(x * y)|x → y, x * (y|x) → y, y|(y|x) → x}.
If we add a unit element to obtain a loop we could start with the following axiomatization:

{(x * y)|x = y, x * (y|x) = y, x * 1 = x} ∪ {x * y = y * x}
and the corresponding subterm C( * )-convergent rewrite system is

{(x * y)|x → y, x * (y|x) → y, x * 1 → x, y|1 → y, x|x → 1, y|(y|x) → x}.

Rewrite Systems with E-constructors

Some classical examples of subterm rewrite systems can be easily adapted to model theories including commutative or associative-commutative symbols. For instance, let us briefly mention the following rewrite systems:

(i) {occ(x + k, k) → ok} (ii) {rm(x + k, k) → x} (iii) {dec(enc(x, k + y), k) → x} (iv) {dec(enc(x, k), k + y) → x}
For any of these four rewrite systems one can check that the symbol + is a constructor, i.e., it does not appear at the root of any left-hand side; the system is subterm AC(+)-convergent; the system is subterm C(+)-convergent.

Subterms Modulo

In the case of subterm convergent TRSs (modulo the empty theory), it is sufficient for the deduction decision procedure to compute deducible terms just from the set of subterms occurring in the set of terms of the frame. That is, no new terms need to be added. When considering a non-empty theory E, we have to introduce an extended notion of subterm to capture the fact that matching modulo E is now performed when applying a rewrite step modulo E. Recall that E is assumed to be permutative. While this may seem somewhat restrictive it allows for the consideration of theories such as AC and C which are found in a large number of security protocols.

Given a term t, St(t) is the smallest set of terms including t such that

-if u = E u and u ∈ St(t), then u ∈ St(t), -if u ∈ St(t)
and p is a non-root position of u, then u| p ∈ St(t).

Notice that St(t) is finite since E is permutative. For a set of terms T , St(T ) =

t∈T St(t), and for a substitution σ, St(σ) = St(Ran(σ)). Example 1. Consider the theory APG defined in Section 3.1 and the following frames where ñ = {k 1 , k 2 }:

φ = ν ñ.{x 1 → i(k 1 * a), x 2 → a * k 2 } ψ = ν ñ.{x 1 → k 1 * a, x 2 → a * k 2 } φ = ν ñ.{x 1 → i(k 1 * a), x 2 → a * k 1 } ψ = ν ñ.{x 1 → i(k 1 ), x 2 → i(k 1 * k 2 )}
According to the above definition of St, we get the following set of terms.

St(φ) = {i(k 1 * a), i(a * k 1 ), a * k 1 , k 1 * a, a, k 1 , a * k 2 , k 2 * a, k 2 } St(ψ) = {k 1 * a, a * k 1 , a * k 2 , k 2 * a, k 1 , k 2 , a} St(φ ) = {i(k 1 * a), i(a * k 1 ), a * k 1 , k 1 * a, k 1 , a} St(ψ ) = {i(k 1 ), i(k 1 * k 2 ), i(k 2 * k 1 ), k 1 * k 2 , k 2 * k 1 , k 1 , k 2 } Proposition 1.
For any terms t, t , t = E t implies St(t) = St(t ), and for any position p in t, St(t| p ) ⊆ St(t).

The following result states that we cannot generate a new term outside St(t) by rewriting terms in St(t) (except the ground right-hand sides of R).

Lemma 2. If lσ = E t, then for any position p of l, (l| p )σ ∈ St(t).

Proof. By structural induction on l.

If l is a variable, this is trivial since the only possible position is and l| = l. Assume l = f (l 1 , . . . , l m ) and σ is a substitution such that f (l 1 , . . . , l m )σ = E t.

If there is an equational step at the root position, then there exist some terms g 1 , . . . , g m such that l 1 σ = E g 1 , . . . , l m σ = E g m and f (g 1 , . . . , g m ) = E t.

By definition of St(t) and Proposition 1, the terms g 1 , . . . , g m are in St(t), and so l 1 σ, . . . , l m σ ∈ St(t).

If there is no equational step at the root position, then t is of the form f (t 1 , . . . , t m ) and l 1 σ = E t 1 , . . . , l m σ = E t m . By definition of St(t) and Proposition 1, the terms t 1 , . . . , t m are in St(t), and so l 1 σ, . . . , l m σ ∈ St(t).

Decision Procedures for Shallow Permutative Theories

In this section we construct new decision procedures for deduction and static equivalence where E is a shallow permutative theory, e.g., E is Commutativity. We start by considering deduction which will also be needed when considering the problem of static equivalence.

Deduction

The decision procedure for the deduction problem requires the computation of some finite deducible terms defining the so-called completion of a given frame. Definition 4. Let φ = ν ñ.σ be a normalized frame. The set of terms D * (φ) is the smallest set D such that:

(1) Ran(σ) ⊆ D, (2) if t 1 , . . . , t n ∈ D and f (t 1 , . . . , t n ) ∈ St(σ) then f (t 1 , . . . , t n ) ∈ D, (3) if t ∈ D, t ∈ St(σ), t = E t , then t ∈ D, (
(φ) = {i(k 1 * a), a * k 2 , a, i(a * k 1 ), k 2 * a, k 1 * a, a * k 1 } and D * (ψ) = {k 1 * a, a * k 2 , a, a * k 1 , k 2 * a}.
The symbol a ∈ St(σ) is contained in these sets due to the second item of Definition 4. However, we cannot use this rule for elements of ñ, which rules out k 1 and k 2 . In addition, e is not contained in these sets since e ∈ St(φ). Therefore, for φ = ν ñ.σ, we get:

σ * = σ{x 3 → i(a * k 1 ), x 4 → k 2 * a, x 5 → a, x 6 → k 1 * a, x 7 → a * k 1 } ζ φ = {x 3 → x 1 , x 4 → x 2 , x 5 → a, x 6 → i(x 1 ), x 7 → i(x 1 )}
For the frame ψ = ν ñ.τ , we obtain:

τ * = τ {x 3 → a * k 1 , x 4 → k 2 * a, x 5 → a} ζ ψ = {x 3 → x 1 , x 4 → x 2 , x 5 → a}
The decision procedure is based on the following reduction lemma, using the facts that the completion is computable and the deduction problem is decidable in the empty equational theory.

Lemma 3 (Deduction). Let RE = R∪E where R is any subterm E-convergent TRS and E is any shallow permutative theory. For any normalized frame φ and any normalized term t, we have that φ RE t if and only if φ * t.

Proof. See Section 4.3. -The term k 1 is deduced from ψ modulo AP G, thanks to the recipe i(x 1 ).

-The term k 1 * (k 2 * k 1 ) is deduced from ψ modulo APG, thanks to the recipe i(x 1 ) * i(x 2 ).

Static Equivalence

The decision procedure for the static equivalence is based on the computation of small equalities bounded by the size of R. Example 4. Let us look at Eq B ζ for some of the frames from Example 1. Since these sets can be large, but finite, we will not list every equation in the set. Let us consider Eq B ζ (φ). First are all the equalities that consist of terms, t and t , of size 0, i.e., variables:

x 1 = x 1 , x 2 = x 2 , x 1 = x 3 , x 2 = x 4 . . .
Notice that each of these satisfies Definition 5. For example, (

x 2 ζ φ )σ = a * k 2 = RE k 2 * a = σ(ζ φ x 4
). We also have equalities between size 1 terms:

i(x 1 ) = i(x 1 ), i(x 2 ) = i(x 2 ), . . . i(x 1 ) = i(x 3 ), . . . x 1 * x 1 = x 1 * x 1 , . . . , x 1 * x 2 = x 3 * x 4 . . .
The same applies for these equalities. For example, ((

x 1 * x 2 )ζ φ )σ = i(k 1 * a) * (a * k 2 ) = RE i(a * k 1 ) * (k 2 * a) = ((x 3 * x 4 )ζ φ )σ.
We need to also include mixed sized equalities such as between size 0 and size 1 terms:

x 3 = i(x 5 ), i(x 3 ) = x 1 , i(x 3 ) = x 5 , e * x 7 = x 7 . . .
Note that equalities such as x 7 * k 1 = x 1 are not included since f n(x 7 * k 1 )∩ñ = ∅. |R| = 2 thus the final and largest, in terms of term size, set of equalities is between two terms of size 2: e * x 1 = e * x 1 , e * x 1 = e * x 3 , . . . , i(i(x 1 )) = i(i(x 3 )), . . . To get a decision procedure, it remains to show that checking small equalities defined by Eq B ζ is sufficient to prove the static equivalence of the two input frames. Note that the check of each of these equalities is effective since the REequality is decidable. According to the above reduction lemmas (Lemma 3 and Lemma 4) we obtain the following result: Theorem 1. Let RE = R ∪ E where E is any shallow permutative theory and R is any subterm E-convergent TRS. Then, deduction and static equivalence are decidable in RE.

Lemma 4 (Static Equivalence). Let RE = R ∪ E
To prove both reduction lemmas (Lemma 3 and Lemma 4) and so Theorem 1, we reuse the same approach as in [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF][START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF], by applying two technical lemmas introduced in Section 4.3, namely Lemma 7 for E and Lemma 9 for R modulo E. To prove these lemmas, we use some properties satisfied by a shallow permutative theory E. With shallow permutative theories, we have identified a class of theories E for which we can apply exactly the same approach as in [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF][START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] to get new decidability results for equational rewrite systems which are both subterm and E-convergent.

Theorem 1 applies to the subterm C-convergent rewrite systems, such as the ones listed in Section 3.1. The rewrite system can be empty, which means that the deduction and the static equivalence problems are decidable in shallow permutative theories. Commutativity is perhaps the most popular shallow permutative axiom but obviously it is not the only one, for example f (x, y, z) = f (z, x, y) and x + 0 = 0 + x are also shallow permutative. Moreover, a union of shallow permutative theories remains shallow permutative, and so Theorem 1 can be directly applied to this union of theories, for instance to handle a union of several commutative symbols.

Correctness Proofs

Recall that, given a frame φ = ν ñ.σ and a term t, tφ denotes by a slight abuse of notation the term tσ.

Remark 1. When we use the notation tφ, we assume that a variable x does not occur in t if xφ is a ground term occurring in the axioms of E. This can be assumed without loss of generality since that term, say t , can be used as a subterm of t since t satisfies the name restriction of φ. Lemma 5. Assume E is shallow permutative. For any term s satisfying the name restriction, if sφ * = E u then there exists a term t satisfying the name restriction of φ * such that u = tφ * and |s| = |t|.

Proof. Let us focus on an equational step sφ * ↔ E u. Then, the generalization to sφ * ↔ * E u can be easily proved by induction on the length of the derivation. If the equational step ↔ E is applied at a position of a non-variable term s, then φ * belongs to the substitution of the equational step because E is shallow permutative, and the term u can be expressed as a term tφ * with |t| = |s|. Note that, due to the restrictions on E, an equational step ↔ E will not increase the size of a term.

Otherwise, the equational step ↔ E is necessarily applied in φ * , which means that there exists a variable x at a position p of s such that xφ * ↔ E u| p . By definition of φ * , there exists a variable y such that yφ * = u| p . Therefore, we have sφ * ↔ E u = (s[y] p )φ * and we can choose t = (s[y] p ). The following lemma corresponds to Lemma 3 in the appendix of [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]. (A) Consider s = f (s) and t = g( t). By applying Lemma 6, two cases are possible: (i) f = g and sφ * = E tφ * . By applying the induction hypothesis, we get (sζ φ )ψ = E ( tζ φ )ψ, and so (sζ φ )ψ = f ((sζ φ )ψ) = E f (( tζ φ )ψ) = (tζ φ )ψ. (ii) By Lemma 6, we have sφ * = E ūφ * = lµ and tφ * = E vφ * = rµ such that f ( l) ←→ E g(r). By applying the induction hypothesis, we get (sζ φ )ψ = RE (ūζ φ )ψ and ( tζ φ )ψ = RE (vζ φ )ψ. The terms l, r are either variables or ground terms, and so u i φ * = xµ = v j φ * for each variable x in l, r. By the induction hypothesis, we get (

Lemma 7. Let RE = R ∪ E where R is any subterm E-convergent
u i ζ φ )ψ = RE (v j ζ φ )ψ.
Hence, there exists a substitution µ such that

• (sζ φ )ψ = RE (ūζ φ )ψ = RE lµ • ( tζ φ )ψ = RE (vζ φ )ψ = RE rµ Consequently, we have • (sζ φ )ψ = f ((sζ φ )ψ) = RE f ((ūζ φ )ψ) = RE f ( lµ ) • (tζ φ )ψ = g(( tζ φ )ψ) = RE g((vζ φ )ψ) = RE g(rµ ) where f ( lµ ) = E g(rµ ). (B) Consider s = f (s 1 , . . . , s r ) and t is a variable x. Assume xφ * = E sφ * .
We have that f (s The Lemma 4 given in the appendix of [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] can be adapted as follows:

1 φ * , . . . , s r φ * ) = E xφ * . Let N i = s i φ * for i = 1, . . . , r, and M = xφ * . Since f (N 1 , . . . , N r ) = E M and M ∈ St(φ), then N i ∈ St(φ). Since N i = s i φ * and N i ∈ St(φ), we have that N i ∈ Ran(φ * ),
Lemma 8. Let RE = R ∪ E where R is any subterm E-convergent TRS and E is any shallow permutative theory. For any term s satisfying the name restriction and any term t such that sφ * → R t, there exists a term u satisfying the name restriction such that t = uφ * and for any frame

ψ such that ψ |= Eq B ζ (φ), (sζ φ )ψ = RE (uζ φ )ψ.
Proof. (i) Let us first assume that the rewrite step occurs at the root position.

Suppose sφ * = lµ with l → r ∈ R. There are two possibilities:

-Assume there exists some substitution µ such that s = lµ . The substitution µ satisfies the name restriction of φ since s satisfies it. We have µ = µ φ * , and so sφ * = lµ φ * → R rµ φ * , where rµ satisfies the name restriction of φ thanks to the form of rules in R. Moreover, for any frame ψ with the same name restriction as the one of φ, the same rewrite step applies on sζ φ ψ = lµ ζ φ ψ and we get

sζ φ ψ = lµ ζ φ ψ → R rµ ζ φ ψ.
-Otherwise, it is impossible to have |s| > |R| and sφ * = lµ. Consequently, |s| ≤ |R| and only two cases are possible for the rewrite rule l → r since R is subterm E-convergent: There exists a position p = such that s φ * = (s φ * )[sφ * ] p with sφ * → R t. By the case (i) above, there exists a term u such that t = uφ * and (sζ φ )ψ = RE (uζ φ )ψ. Then, we have

• If r is a ground term, then (sζ φ )φ = RE sφ * → R r = rφ * = RE (rζ φ )φ (
s φ * → R (s φ * )[t] p = (s φ * )[uφ * ] p = (s [u] p )φ * and (s ζ φ )ψ = (s ζ φ ψ)[sζ φ ψ] p = RE (s ζ φ ψ)[uζ φ ψ] p = (s [u] p )ζ φ ψ
This lemma can now be extended as follows using Lemma 7.

Lemma 9. Let RE = R∪E where R is any subterm E-convergent TRS and E is any shallow permutative theory. For any term s satisfying the name restriction and any term t with sφ * → R,E t, there exists a term u satisfying the name restriction such that t = E uφ * . In addition, for any frame ψ such that ψ |= Eq B ζ (φ), (sζ φ )ψ = RE (uζ φ )ψ.

Proof. If sφ * → R,E t then (according to Lemma 5) there exists a term s satisfying the name restriction such that sφ * = E s φ * and s φ * → R t. By Lemma 7, we have (sζ φ )ψ = RE (s ζ φ )ψ. By Lemma 8, there exists a term u satisfying the name restriction such that (s ζ φ )ψ = RE (uζ φ )ψ. Consequently, we get (sζ φ )ψ = RE (uζ φ )ψ.

We are now ready to prove the two reduction lemmas, namely Lemma 3 and Lemma 4. For both lemmas, we prove the non-obvious direction:

-Lemma 3.
Proof. (Only if direction) Assume sφ * = RE t where t is normalized. According to Lemma 9, there exists a rewrite proof of the form

sφ * → R,E • = E • • • → R,E • = E s φ * = E t
where s satisfies the name restriction of φ * , equivalently the name restriction of φ.

-Lemma 4.

Proof. (If direction) Let Eq ζ (φ) be the set of all equalities sζ φ = tζ φ such that (sζ φ = RE tζ φ )φ. Consider any sζ φ = tζ φ ∈ Eq ζ (φ). According to Lemma 9, there exists a rewrite proof of the form

(sζ φ )φ = RE sφ * → R,E • = E • • • → R,E • = E s φ * (tζ φ )φ = RE tφ * → R,E • = E • • • → R,E • = E t φ *
where s φ * = E t φ * and s , t satisfy the name restriction of φ * (equivalently, the name restriction of φ). By Lemma 9, we have (sζ

φ )ψ = RE (s ζ φ )ψ and (tζ φ )ψ = RE (t ζ φ )ψ. By Lemma 7, we have (s ζ φ )ψ = RE (t ζ φ )ψ. Hence, (sζ φ )ψ = RE (tζ φ )ψ, which means that ψ |= Eq ζ (φ).
In a symmetric way, we can show that φ |= Eq ζ (ψ). Then, we can conclude since φ ≈ RE ψ iff ψ |= Eq ζ (φ) and φ |= Eq ζ (ψ)

Equational Variants in Syntactic Permutative Theories

In this section we start investigating the possibility to go beyond the case E is shallow permutative, by considering E is syntactic permutative, e.g., E is Associativity-Commutativity, and R is E-convergent. In this general case, we need to consider an additional finiteness assumption introduced below. The investigated approach relies on the possibility of computing a finite representation of all the terms that are matched modulo E by the left-hand sides of the TRS R.

Definition 6. An E-variant of a term l is a pair (t, σ) such that t = E lσ and Dom(σ) is included in f v(l). Given two E-variants (u, θ) and (v, γ) of a term l, (u, θ) is more general than (v, γ), denoted by (u, θ) ≤ E (v, γ) if there exists a substitution τ such that uτ = E v and θτ = E γ. A complete set of E-variants of l, denoted by CV E (l), is a set of E-variants of l such that for any E-variant (v, γ) of l, there exists (u, θ)

∈ CV E (l) such that (u, θ) ≤ E (v, γ).
The equational theory E is said to have the Finite Equational Variant Property (FEVP, for short) if any term admits a finite complete set of E-variants.

Equational variants are analogous to variants defined with respect to a convergent TRS [START_REF] Comon-Lundh | The finite variant property: How to get rid of some algebraic properties[END_REF][START_REF] Escobar | Folding variant narrowing and optimal variant termination[END_REF][START_REF] Meseguer | Variant-based satisfiability in initial algebras[END_REF]. When R denotes a convergent TRS, a R-variant of l is defined in the literature as a pair (t, σ) such that t = (lσ)↓ R and t, σ are both R-normalized. Given two R-variants (u, θ) and (v, γ) of l, (u, θ) is said to be more general than (v, γ) if there exists a substitution τ such that uτ = v and θτ = γ. A complete set of R-variants of l is defined in the same way as in Definition 6: it is a set CV R (l) of R-variants of l such that for any R-variant (v, γ) of l, there exists (u, θ) ∈ CV R (l) such that (u, θ) is more general than (v, γ). Then, R is said to have the Finite Variant Property (FVP, for short) if any term admits a finite complete set of R-variants.

Proposition 2. If a convergent TRS has the FVP, then its equational theory has the FEVP.

The following notion of complete set of E-matched terms is instrumental to show the FEVP. Definition 7. A term t is said to be E-matched by l if there exists some substitution σ such that (t, σ) is an E-variant of l. The set of terms E-matched by l is denoted by M T E (l). A complete set of terms E-matched by l is a subset of M T E (l) denoted by CMT E (l) such that for any t ∈ M T E (l) there exist t ∈ CMT E (l) and a substitution µ satisfying the following property: t = E t µ and for any E-variant (t, σ) of l there exists an E-variant (t , σ ) of l such that σ = E σ µ.

Given a non-empty TRS R, a complete set of terms

E-matched by R is CMT E (R) = {t | t ∈ CMT E (l), l → r ∈ R}.
Unsurprisingly, the finiteness of CMT E (l) for each term l suffices to show the FEVP:

Proposition 3. Assume E is permutative. For any term l, if CMT E (l) is finite, then {(t, σ) | t ∈ CMT E (l), lσ = E t} is a finite CV E (l).
Proof. Since E is assumed to be permutative, the set of substitutions σ such that lσ = E t is finite for any terms l, t.

When E is the empty theory and l is any term, the singleton {l} is a CMT E (l). When E is an arbitrary theory, the singleton {l} can be a CMT E (l) for some particular terms l, e.g., CMT E (x + 0) = {x + 0} for E = AC(+). As stated below, the singleton {l} is always a CMT E (l) under a simple assumption that bears some similarities with the unique matching property used in [START_REF] Chevalier | Hierarchical combination of intruder theories[END_REF] to get decidability of ground intruder systems corresponding to deduction problems in a hierarchical combination of theories. Proposition 4. If l is any variable, then {l} is a CMT E (l). If l is any nonvariable term and for any term t in M T E (l) the match-equation l ≤ ? E t admits a unique solution modulo E, then {l} is a CMT E (l).

Proof. Consider the identity substitution ε. For any term l, lε = l, and so (l, ε) is an E-variant of l.

-Let l be any variable. For any E-variant (t, σ) of l, we have t = E lσ and σ = E εσ where (l, ε) is an E-variant of l. -Let l be any non-variable term. By assumption, for any term t in M T E (l), there exists a unique substitution σ such that t = E lσ and σ = E εσ.

By definition of a complete set of E-matched terms, this implies in both cases that {l} is a CMT E (l).

The case of a variable l being easily solved, we focus below on the case where l is a non-variable term. We now study a general procedure that, when terminating, computes a finite CMT E (l). Consider the inference system MTG defined by the set of rules in MSP given in Figure 1 plus the two additional rules Merge SV , Inst SV given in Figure 2.

Lemma 10. Let l be an arbitrary non-variable term and x a fresh variable. Assume that any MTG-derivation starting from {l ≤ ? x} is terminating. Then a CMT E (l) is given by the finite set M T of terms xσ P where -P is a solved form such that {l ≤ ? x} * MTG P , σ P is the composition of all substitutions applied by Inst SV or Merge SV in the derivation {l ≤ ? x} * MTG P .

Proof. Given any solved form P such that {l ≤ ? x} * MTG P , let µ P be the corresponding substitution and µ P |f v(l) the restriction of µ P to f v(l). For any term xσ P ∈ M T , (xσ P , µ P |f v(l) ) is an E-variant of l. Consequently, M T ⊆ M T E (l).

To show that M T is a complete set of E-matched terms, consider any term t ∈ M T and the set SF of solved forms computed by MSP with {l ≤ ? t} as input. For any substitution θ, {P θ | P ∈ SF } corresponds to the set of solved forms computed by MSP with {l ≤ ? tθ} as input. Since MSP is an

E-matching algorithm, {σθ | σ ∈ CSU E (l ≤ ? t)} is a CSU E (l ≤ ? tθ). Therefore, M T is a CMT E (l).
We show in the following example that MTG may not terminate when E is the Associativity-Commutativity. Example 6. It is difficult to get terminating MTG-derivations when E = AC(+). Let us consider l = (a + x). Starting from a + x ≤ ? x 0 , the only possibility is to apply Inst SV , leading to a + x ≤ ? x 1 + x 2 . The theory E = AC(+) admits a resolvent presentation that consists of seven axioms. One of these axioms is w 1 + (w 2 + w 3 ) = (w 1 + w 2 ) + w 3 . By applying MatchMut with this axiom, we get a = ? w 1 , x = ? w 2 + w 3 , w 1 + w 2 ≤ ? x 1 , w 3 ≤ ? x 2

The repeated application of RemEq and Rep leads to

w 1 ≤ ? a, x = ? w 2 + x 2 , a + w 2 ≤ ? x 1 , w 3 ≤ ? x 2 .
It contains a + w 2 ≤ ? x 1 which is a renaming of the input, and so the MTG procedure loops in that case.

Termination of MTG and Closure Under Paramodulation

As stated above, the MTG procedure is not guaranteed to terminate for an arbitrary E. However, there are classes of permutative theories for which the MTG procedure is guaranteed to terminate. One such class of permutative theories are those closed under paramodulation, which we prove below.

Lemma 11. Consider MTG B = MSP B ∪ {Merge SV , Inst SV } where MSP B is defined in Section 2.5 and Merge SV , Inst SV are given in Fig. 2. Let E be any permutative theory closed by paramodulation. For any non-variable term l and any fresh variable x, any MTG B -derivation starting from {l ≤ ? x} is terminating, and MTG B provides a CMT E (l) in the same way as the one described in Lemma 10 for MTG.

Proof. To prove termination, let us analyze the interaction between MSP B and the additional rules Merge SV and Inst SV :

-After the application of Merge SV , no MSP B rule can be fired. Only Inst SV can be possibly fired after the exhaustive application of Merge SV . -After the application of Inst SV on s ≤ ? x, some MSP B rule may be fired, and there are two possible cases:

• If s is rooted by an unboxed symbol occurrence, then MatchDec or MatchMut B applies and in both cases the number of unboxed symbol occurrences is strictly decreasing. • If s is rooted by a boxed symbol occurrence, then necessarily MatchDec applies and the number of unboxed symbol occurrences is not increasing but the multiset of sizes of terms is strictly decreasing.

The completeness follows from the proof of Lemma 10 and the fact that MSP B is an E-matching algorithm.

According to Lemma 11 and Proposition 3, we get the following result: Theorem 2. If E is a permutative theory closed by paramodulation, then E has the FEVP. Example 7. Let us consider a small example of computing a CMT E (l), where l is x+i(a) and E = {x+i(y) = i(y)+x}. We start by applying the MTG B procedure on the input {x + i(a) ≤ ? x 0 }. Initially, no rules from MSP apply and only Inst SV applies, resulting in three substitutions: {x 0 → x 1 + x 2 }, {x 0 → i(x 1 )}, and {x 0 → a}. Thus, each substitution causes a branch in the computation of the procedure. The branches generated by {x 0 → i(x 1 )}, and {x 0 → a} lead to a failure. Let us follow the branch corresponding to {x 0 → x 1 + x 2 } and the match-equation x + i(a) ≤ ? x 1 + x 2 . Now rules from MSP apply, including as a first rule MatchDec resulting in {x ≤ ? x 1 , i(a) ≤ ? x 2 }. Continuing in this fashion we reach a solved form corresponding to the E-matched term x 1 + i(a) where x 1 + i(a) = x 0 {x 0 → x 1 + x 2 }{x 2 → i(x 3 )}{x 3 → a}. In addition to MatchDec, MatchMut B also applies on x + i(a) ≤ ? x 1 + x 2 and leads to

x = ? x , i(a) = ? i(y ) , i(y ) ≤ ? x 1 , x ≤ ? x 2 .
Then Inst SV can be applied on i(y ) ≤ ? x 1 with the substitution {x 1 → i(x 3 )}. Following this branch, we get another solved form corresponding to the E-matched term i(a)+x 2 where i(a)+x 2 = x 0 {x 0 → x 1 +x 2 }{x 1 → i(x 3 )}{x 3 → a}.

Decision Procedures for Syntactic Permutative Theories

From now on, we assume that E is syntactic permutative and R is a subterm Econvergent TRS admitting a finite CMT E (R), where CMT E (R) is introduced in Definition 7. Under this finiteness assumption, it is possible to define an appropriate notion of size for R modulo E.

Definition 8. Given a non-empty TRS R admitting a finite CMT E (R), the size of R modulo E, denoted by |R|, is defined as follows:

|R| = max{|t| | t ∈ CMT E (R)}.
We refer below to some notions introduced in Section 4 with respect to |R|, such as the completion of a frame (Definition 4) and a set of terms of size bounded by |R| (Definition 5). These notions are defined in the same way in the context of this section, using now the size |R| given in Definition 8.

Remark 2. The size of R modulo E is computable if and only if there exists a finite and computable CMT E (R). Remark 3. When E is the empty theory, the size of R modulo E coincides with the size of R defined in Section 2 since {l | l → r ∈ R} is a CMT E (R).

In the following, we present reduction methods from RE = R ∪ E to the combined theory ∅ ∪ E where ∅ denotes the empty Ω-theory. According to the combination result in [START_REF] Cortier | Decidability and combination results for two notions of knowledge in security protocols[END_REF] it is always possible to obtain decision procedures for both deduction and static equivalence in ∅ ∪ E from the ones existing in E alone. This explains why ∅ ∪ E is often simply denoted by E in the following two subsections. In [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF], it has been observed that the decidability of static equivalence entails the decidability of deduction, provided that the signature includes a unary free function symbol. In fact, the encoding presented in [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] can be easily generalized to any non-constant free function symbol. Usually Ω contains at least a non-constant function symbol, and so the decidability of static equivalence in ∅ ∪ E implies the decidability of deduction in E. Thus, we could be tempted to focus our attention on static equivalence only. However, as illustrated in [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF][START_REF] Cortier | Decidability and combination results for two notions of knowledge in security protocols[END_REF], a decision procedure for the static equivalence usually requires a decision procedure for the deduction. In an analogous way, we first focus on deduction as a first step towards a decision procedure for the static equivalence.

Deduction

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

Lemma 12 (Deduction). Let RE = R ∪ E where E is any syntactic permutative theory and R is any subterm E-convergent TRS with a computable size of R modulo E. For any normalized frame φ and any normalized term t, we have that φ RE t if and only if φ * E t.

Proof. See Section 6.3.

Example 8. Consider R = {i(x) + i(a) → x}, E = {i(x) + i(y) = i(y) + i(x)}. Let φ = ν{k}.{x 1 → i(a), x 2 → a + i(k)} and ψ = ν{k}.{x 1 → i(a), x 2 → i(k)}.
One can check that D * (φ) = {i(a), a + i(k), a} and D * (ψ) = {i(a), i(k), a, k}. Once these sets of deducible terms are computed, the frames can be completed and used to reduce the deduction problem modulo RE to the deduction problem modulo E. For example, notice that the term i(k) + k is deducible from ψ * but not from φ * .

Static Equivalence

In a way similar to what is done for disjoint combinations [START_REF] Cortier | Decidability and combination results for two notions of knowledge in security protocols[END_REF], we extend the input frames with the instantiation of recipes of all deducible terms occurring in the completions. Definition 9. Let φ = ν ñ.σ be a frame. Let Π be a set of terms t such that tσ is ground and t satisfies the name restriction of φ. The Π-extension of φ is the frame Πφ = ν ñ.{χ t → t | t ∈ Π}σ. Lemma 14 (Static Equivalence). Let RE = R ∪ E where E is any syntactic permutative theory and R is any subterm E-convergent TRS with a computable size of R modulo E. For any normalized frames φ and ψ introduced in Lemma 13, we have φ ≈ RE ψ iff ψ |= Eq B ( φ) and φ |= Eq B ( ψ) and φ ≈ E ψ.

Proof. See Section 6.3.

Example 12. Continuing Example 11, notice that x 4 = x 2 + x 1 ∈ Eq B ( ψ). However, x 4 = x 2 +x 1 ∈ Eq B ( φ). In other words, φ |= Eq B ( ψ). Therefore, the frames are not statically equivalent. This is due to the fact that in the second frame, ψ, the adversary would have knowledge of k but not so in the first frame, φ. Thus the adversary is able to use this knowledge to distinguish the frames.

According to the above reduction lemmas, we get the following result. Theorem 3. Let RE = R ∪ E where E is any syntactic permutative theory, R is any subterm E-convergent TRS with a computable size of R modulo E, and both deduction and static equivalence are decidable in E. Then, both deduction and static equivalence are decidable in RE.

The proof of Theorem 3 is given below.

Correctness Proofs

Let us first rephrase the Lemma 4 proved in the appendix of [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] by using the frames φ and ψ. One can notice that we use a definition for Eq B which is more refined than the rough one considered in [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]. Instead of considering contexts whose sizes are bounded by the maximal size of the left-hand sides in R as in [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF], our definition takes into account only the contexts for which the frame is needed for being matched by some left-hand side.

Lemma 15. Let RE = R ∪ E where E is any syntactic permutative theory and R is any subterm E-convergent with a computable size of R modulo E. Assume φ ≈ E ψ and ψ |= Eq B ( φ). For any term s satisfying the name restriction and for any term t such that s φ → R,E t, there exists a term u satisfying the name restriction such that t = E u φ and s ψ = RE u ψ.

Proof. The structure of the proof is similar to the one developed for Lemma 8.

(i) Let us first assume that the rewrite step occurs at the root position. Suppose s φ = E lµ with l → r ∈ R. There are two possibilities:

-Assume there exist some term s c in CMT E (l) and a substitution θ such that s = E s c θ. Both s c and θ satisfy the name restriction of φ since s satisfies it. By definition of a CMT E (l), for the E-variant (s φ, µ) of l there exists some E-variant (s c , θ ) of l such that µ = E θ (θ φ). The substitution θ satisfies the name restriction of φ since s c satisfies it. Let µ = θ θ. We have µ = E µ φ where µ satisfies the name restriction of φ. Thus, we have s φ = E lµ φ → R rµ φ, where rµ satisfies the name restriction of φ thanks to the form of rules in R. Moreover, for any frame ψ with the same name restriction as the one of φ, the same rewrite step applies and we get lµ ψ → R rµ ψ, where rµ satisfies the name restriction. If φ ≈ E ψ, then s φ = E lµ φ implies s ψ = E lµ ψ. Consequently, s ψ = E lµ ψ → R rµ ψ. -Otherwise, if |s| > |R| and s φ = E lµ, then there would be a contradiction with the fact that CMT E (l) is a complete set of terms E-matched by l. Thus, we have necessarily |s| ≤ |R|, and only two cases are possible for the rewrite rule l → r since R is subterm E-convergent:

• If r is a ground term, then s φ → R,E r = r φ (where r satisfies the name restriction of φ). By definition of Eq B and by assumption on ψ, we have s ψ = RE r = r ψ. • If r is a subterm of l, then by definition of φ, there exists some variable x such that s φ → R,E x φ. By definition of Eq B and by assumption on ψ, we have s ψ = RE x ψ. (ii) Let us now assume that the rewrite step occurs below the root position.

There exists a position p = such that s φ = (s φ)[s φ] p with s φ → R,E t. By the case (i) above, there exists a term u such that t = E u φ and s ψ = RE u ψ. Then, we have We are now ready to prove the two reduction lemmas, namely Lemma 12 and Lemma 14. For both lemmas, we prove the non-obvious direction:

-Lemma 12.

Proof. (Only if direction) Assume s φ = RE t where t is normalized. According to Lemma 15, there exists a rewrite proof of the form

s φ → R,E • = E • • • → R,E • = E s φ = E t
where s satisfies the name restriction of φ. By choosing ψ = φ, we have φ = E φ * and so

sφ * = E s φ → R,E • = E • • • → R,E • = E s φ = E s φ * = E t -Lemma 14.
Proof. (If direction) Assume s φ = RE t φ. According to Lemma 15, there exists a rewrite proof of the form

s φ → R,E • = E • • • → R,E • = E s φ t φ → R,E • = E • • • → R,E • = E t φ
where s φ = E t φ and s , t satisfy the name restriction of φ. By Lemma 15, we have s ψ = RE s ψ and t ψ = RE t ψ. By assumption, we have φ ≈ E ψ, and so s φ = E t φ implies s ψ = E t ψ. Consequently, s ψ = RE t ψ.

Conclusion

We have shown how to lift the existing decidability results on knowledge in subterm convergent rewrite systems to rewrite systems defined modulo certain equational theories E. In particular, we have lifted the decidability results to the case in which E is shallow permutative, e.g., the Commutativity theory C. Furthermore, we have studied a notion of complete set of E-matched terms, CMT for short, such that if a subterm convergent equational rewrite system R admits a finite CMT for each of its left-hand sides, then the size of R modulo E can be defined. In addition, the knowledge problems in R ∪ E are decidable if they are decidable modulo E and the size of R modulo E is computable. We have also developed a procedure (MTG) such that if the procedure terminates, a finite CMT is guaranteed. The MTG procedure is terminating for a large class of syntactic permutative theories, namely permutative theories closed by paramodulation. Even if the MTG procedure is not terminating, it is possible to have a finite CM T . For example, in general the AC case does not produce a terminating MTG procedure. However, a particular subterm AC-convergent rewrite system can admit a computable size of R modulo AC and consequently the knowledge problems are decidable in R ∪ AC. The next step would be to explore a relaxing of the notion of subterm convergent while maintaining the decidability results for the knowledge problems. This would be useful since many axiomatizations of protocols are close but not completely subterm convergent. For example, consider the following set of axioms: Notice that this theory is not completely subterm convergent. However it is close in that all the right-hand sides are either subterms or homeomorphic embeddings of the left-hand sides. If the notion of subterm could be extended to such cases, then it may be possible to solve the knowledge problem in the C(&)-convergent form of this theory.

More generally, a natural continuation of this work is to study the use of equational (E-convergent) rewrite systems for extending the complete but nonnecessarily terminating procedures that have been designed for the knowledge problems in standard (convergent) rewrite systems [START_REF] Ciobâcȃ | Computing knowledge in security protocols under convergent equational theories[END_REF][START_REF] Baudet | YAPA: A generic tool for computing intruder knowledge[END_REF]. Due to the interest of AC in protocol verification, it would be useful to develop such an engine with the capability to handle AC-convergent rewrite systems.

Another challenge is to study the knowledge problems in combinations of the form R ∪ E ∪ T where R is an E-convergent TRS and T is an arbitrary theory sharing with R only the function symbols of E, like for instance R is AC(+)convergent and T = {h(x + y) = h(x) + h(y)}. In this direction, it would be interesting to extend our combination results [START_REF] Erbatur | Notions of knowledge in combinations of theories sharing constructors[END_REF] on theories sharing absolutely free constructors to the case of theories sharing constructors modulo a theory E such as AC.

Fig. 1 .

 1 Fig. 1. MSP matching procedure for syntactic permutative theories

  4) if there is a root reduction s[ d] → R,E t where |s| ≤ |R|, f n(s) ∩ ñ = ∅, d ∈ D and t ∈ St(σ), then t ∈ D. Let σ * = σ{χ u → u | u ∈ D * (φ)\Ran(σ)} where χ u is a fresh variable. The frame φ * = ν ñ.σ * is called the completion of φ with respect to contexts bounded by |R|. Given a recipe ζ u for each u ∈ D * (φ)\Ran(σ), the substitution {χ u → ζ u | u ∈ D * (φ)\Ran(σ)} is called a recipe substitution of φ and is denoted by ζ φ . Example 2. Consider the frames φ and ψ from Example 1. Now let us compute the sets D * (φ) and D * (ψ), and recipe substitutions ζ φ and ζ ψ . One can check that D *

Example 3 .-

 3 (Example 1 continued.) The term (k 2 * a) * (k 1 * a) is deduced from φ modulo AP G since it is deduced from φ * thanks to the recipe x 4 * x 6 .

Definition 5 .

 5 Let φ = ν ñ.σ be a normalized frame. Consider the following sets of terms:Bt(R) = {t | |t| ≤ |R|}; and Gr(R) = {r | l → r ∈ R, r is ground }.Given a recipe substitution ζ φ of φ as introduced in Definition 4, the set Eq B ζ (φ) is the set of equalities tζ φ = t ζ φ such that (tζ φ = RE t ζ φ )φ and t, t ∈ Bt(R) ∪ Gr(R).

Lemma 6 .

 6 Assume E is shallow permutative. For any non-variable terms s = f (s) and t = g( t) satisfying the name restriction, if sφ * = E tφ * then f = g and sφ * = E tφ * , or there exist terms l, r, ū, v and a substitution µ such that l, r are either variables or ground terms, ū, v satisfy the name restriction of φ, |ū| = |s|, |v| = | t|, sφ * = E ūφ * = lµ, tφ * = E vφ * = rµ, and f ( l) ←→ E g(r). Proof. Since E is a shallow theory, it has a resolvent presentation which remains shallow. Therefore, if sφ * = E tφ * then sφ * = f (sφ * ), tφ * = f ( tφ * ), and sφ * = E tφ * , or sφ * = f (sφ * ), tφ * = g( tφ * ) and there exist terms l, r and a substitution µ such that l, r are either variables or ground terms, sφ * = E lµ, tφ * = E rµ, and f ( l) ←→ E g(r). By Lemma 5, there exist terms ū and v satisfying the name restriction such that |ū| = |s|, |v| = | t| and ūφ * = lµ, vφ * = rµ.

  and so there exists some recipeζ Ni . Since M = E f (N 1 , . . . , N r ), we have ζ M φ = E f ((ζ N1 φ), . . . , (ζ Nr φ)),and ζ M ψ = RE f ((ζ N1 ψ), . . . , (ζ Nr ψ)) by assumption on ψ. Since N i = E s i φ * , we have that ζ Ni ψ = RE (s i ζ φ )ψ by the induction hypothesis. Then, (xζ φ )ψ = ζ M ψ = RE (f (s 1 , . . . , s r )ζ φ )ψ = (sζ φ )ψ

  where r satisfies the name restriction of φ). By definition of Eq B ζ and by assumption on ψ, we have (sζ φ )ψ = RE r = RE (rζ φ )ψ. • If r is a subterm of l, then by definition of φ * (cf. Definition 4(4)), there exists some variable x such that (sζ φ )φ = RE sφ * → R xφ * = RE (xζ φ )φ. By definition of Eq B ζ and by assumption on ψ, we have (sζ φ )ψ = RE (xζ φ )ψ. (ii) Let us now assume that the rewrite step occurs below the root position.

Fig. 2 .

 2 Fig. 2. MTG additional rules

Lemma 13 .

 13 Given any normalized frames φ = ν ñ.σ and ψ = ν ñ.τ such that Dom(σ) = Dom(τ ), let φ = (Πφ)↓ R,E , ψ = (Πψ)↓ R,E where Π = St(Ran(ζ φ )∪ Ran(ζ ψ )). Then, we have (i) ( φ) * = φ and ( ψ) * = ψ; (ii) φ ≈ RE ψ if and only if φ ≈ RE ψ.

s

  φ → R,E (s φ)[t] p = E (s φ)[u φ] p = (s [u] p ) φ and s ψ = (s ψ)[s ψ] p = RE (s ψ)[u ψ] p = (s [u] p ) ψ

4

 4

  d(e(x, y), y) → x d(e(x, y&z), y) → e(x, z) d(e(x, y), y&z) → d(x, z) d(e(x, y&z), y&v) → d(e(x, z), v)

  where R is any subterm E-convergent TRS and E is any shallow permutative theory. For any normalized frames φ and ψ, we have that φ ≈ RE ψ iff ψ |= Eq B ζ (φ) and φ |= Eq B ζ (ψ). Consider the frames φ, φ , and ψ from Example 1. We have φ ≈ RE φ since i(x 1 ) = RE x 2 ∈ Eq B ζ (φ ) and i(x 1 )φ = RE x 2 φ. For the two frames φ and ψ, we can show φ ≈ RE ψ by checking that ψ |= Eq B

	Proof. See Section 4.3.
	Example 5.

ζ (φ) and φ |= Eq B ζ (ψ).

  TRS and E is any shallow permutative theory. For any terms s and t satisfying the name restriction, if sφ * = E tφ * and ψ |= Eq B ζ (φ) then (sζ φ )ψ = RE (tζ φ )ψ. Proof. By induction on |s| + |t|. -Base case: if |s| and |t| are less than |R|, then it is true by definition of Eq B ζ . -Inductive step:

  5.1 The MTG Procedure for Computing a Complete Set of Matched Terms Merge SV {x ≤ ? y} ∪ P P σ where x, y are subject variables, σ = {x → y}, if no rule from MSP is applicable. InstSV {s ≤ ? x} ∪ P ({s ≤ ? x} ∪ P )σ where x is a subject variable and s is rooted by a function symbol, σ = {x → f (x1, . . . , xn)}, f is a function symbol, x1, . . . , xn are fresh pairwise distinct variables, if no rule from MSP ∪ {Merge SV } is applicable.

These axioms are a fragment of a larger theory studied in[START_REF] Yang | Theories of homomorphic encryption, unification, and the finite variant property[END_REF], modeling encryption and decryption in a multiset of keys

Acknowledgments: We are very grateful to the reviewers: the paper has been significantly improved thanks to their suggestions. We would like to thank Véronique Cortier and Steve Kremer for fruitful comments and discussions. This work has received funding from the European Research Council (ERC) under the H2020 research and innovation program (grant agreement No 645865-SPOOC).

Proof.

(i) Notice that (σ * ) * = σ * . This is due to the fact that St(σ * ) = St(σ).

Therefore, completing the frame φ (or ψ) does not add new terms. (ii) Consider φ = ν ñ.σ, ψ = ν ñ.τ and the substitution π = {χ t → t | t ∈ Π}.

By definition, σ = πσ and τ = πτ . Let us now prove the two directions:

-Assume φ ≈ RE ψ. Consider any terms s and t satisfying the name restriction of φ. We can assume without loss of generality that

The decision procedure for the static equivalence computes small equalities obtained by considering a finite set of contexts derived from the left-hand sides of R. Definition 10. Let φ = ν ñ.σ be a normalized frame. Consider the sets of terms Bt(R) = {t | |t| ≤ |R|} where |R| is given in Definition 8 and Gr(R) introduced in Definition 5. The set Eq B (φ) is the set of equalities t = t such that (t = RE t )φ and t, t ∈ Bt(R) ∪ Gr(R).

Example 11. Continuing Example 10, we obtain Eq B ( φ) = {i(a) = i(a), i(x 1 ) = i(x 1 ), i(x 3 ) = i(x 3 ), a = a, a + a = a + a, . . .} and Eq B ( ψ

To get a decision procedure, it remains to show that checking small equalities defined by Eq B are sufficient to prove the static equivalence of the two input frames. Note that the check of each of these equalities is effective since the REequality is decidable.

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