Pith. sign in

REVIEW 3 major objections 4 minor 31 references

Right Divisibility in Erasing Semi-Thue Systems: A Minimal View of Intruder Deduction

T0 review · 3 major / 4 minor · reviewed 2026-08-08 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proves right-divisibility is decidable for finite convergent prefix-erasing and suffix-erasing semi-Thue systems, and undecidable for a convergent simultaneous variable-lifting system.

desk verdict The suffix-erasing decidability proof is solid and worth a look, but the advertised undecidability boundary (Theorem 6.16) does not hold as stated: the constructed TRS is not confluent, and the reduction is delegated to [BSE+24]. read the letter →

arxiv 2608.03274 v2 pith:CNJKCR4Y submitted 2026-08-04 cs.LO cs.CRcs.FL

Raja O. P. Damanik , Alwen Tiu This is my paper · ORCID
classification cs.LOcs.CRcs.FL MSC 68Q4203D3520M05
keywords intruderdeductionsemi-Thuesystemsrightdivisibilityprefix-erasingsuffix-erasingdwindlingtermrewritingconvergentrewrite
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper studies intruder deduction in the minimal setting where all function symbols are unary, so terms become words and deduction becomes a right-divisibility question: given words $u$ and $v$, is there a word $w$ such that $wu \equiv_S v$ under a string-rewriting system $S$? It proves that this problem is decidable for every finite convergent prefix-erasing system and every finite convergent suffix-erasing system (the latter also called dwindling systems), even though rule right-hand sides may be arbitrarily long. For prefix-erasing systems the decision procedure is linear time after normalization, while the suffix-erasing algorithm is exponential in $|u|$ in the worst case. The paper then moves beyond words and shows that deduction is already undecidable for a convergent simultaneous variable-lifting term rewriting system, drawing a boundary between simple context-erasing rules and simultaneous variable erasure.

What carries the argument

The main positive tool is the set of suffix multiples $\mathrm{SufMul}_S(u)$, the irreducible suffixes of $u$ that are still right-divisible from $u$, together with its shortest element $u_{\min}$. In the prefix-erasing case, $u_{\min}$ alone characterises right divisibility: $u$ is right-divisible from $v$ exactly when $u_{\min}$ is a suffix of $v$, and $u_{\min}$ is computable by a recursive algorithm or a jump-accelerated variant. In the suffix-erasing case that characterisation fails, so the paper uses the Cayley-graph predecessor function $\delta(c,u)$, the finite set of irreducible words $v$ with $vc \equiv_S u$; iterating $\delta$ backwards over the letters of $u$ decides right divisibility. For the undecidability result, the machinery is a simultaneous variable-lifting rule $f(\alpha_i(x),\beta_i(y),\mathsf{locked}(z)) \to f(x,y,\mathsf{locked}(z))$ together with an unlocking rule $f(x,x,\mathsf{locked}(z)) \to f(x,x,z)$, which encodes MPCP pairs as contexts erased around variables.

What would settle it

Take the Theorem 6.16 TRS with an MPCP instance containing the pair $(a,a)$ and inspect the ground term $f(a(a),a(a),\mathsf{locked}(c))$. The pair rule rewrites it to $f(a,a,\mathsf{locked}(c))$, which then rewrites to $f(a,a,c)$, while the unlocking rule rewrites the original term directly to $f(a(a),a(a),c)$. If these two resulting terms are distinct and irreducible, the system is not confluent, contradicting convergence and falsifying the undecidability theorem as stated.

Watch

Extended reading notes

Core claim

The central claim is that in the word-level fragment of intruder deduction, decidability aligns with the side from which contexts are erased. A prefix-erasing rule $xy \to y$ deletes a nonempty prefix, and the paper shows that in a finite convergent system of this kind right divisibility reduces to computing a shortest suffix multiple $u_{\min}$ and testing whether it is a suffix of the target; this gives a linear-time decision procedure. A suffix-erasing rule $xy \to x$ deletes a nonempty suffix, and here the paper shows that right divisibility remains decidable by a backward search through finite predecessor sets $\delta(c,u)$ over irreducible words, yielding an exponential-time procedure. Dual left-divisibility results follow by reversal. Beyond the unary setting, the paper defines variable-lifting and simultaneous variable-lifting term rewriting systems and proves that there exists a convergent simultaneous variable-lifting TRS for which the deduction problem is undecidable, via a reduction to MPCP whose correctness is delegated to earlier work.

Load-bearing premise

The undecidability theorem depends on the constructed simultaneous variable-lifting TRS being convergent and on the cited MPCP reduction being correct; if that system is not confluent, the theorem's claimed boundary does not follow from the presented argument.

Editorial extensions

If this is right

  • In any unary-signature equational theory, the intruder deduction problem reduces to right divisibility, so the two decidability theorems provide decision procedures for that fragment of symbolic protocol analysis.
  • For a fixed finite convergent prefix-erasing system, the right-divisibility test runs in linear time in the combined length of the input words, making the procedure practical enough for tool integration.
  • The suffix-erasing result settles right divisibility for dwindling systems, a class previously considered mostly in connection with dual unification problems.
  • By reversal, left divisibility is decidable for finite convergent prefix-erasing and suffix-erasing systems, giving a symmetric pair of positive results.
  • The undecidability of a convergent simultaneous variable-lifting system shows that allowing more than one context to be erased at once marks a real boundary beyond the decidable unary cases.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • An implicit consequence of the prefix-erasing result is that the saturated-set technique from subterm-convergent theories has a purely word-level counterpart, which may be liftable back to larger signatures for other context-erasing classes.
  • The undecidability theorem suggests that the open question for ordinary (single-variable) lifting may hinge on forbidding simultaneous erasures; testing the same MPCP encoding with $n=1$ lifting would isolate where the undecidability enters.
  • A concrete testable extension is to implement the backward suffix-erasing algorithm on random finite convergent dwindling systems and check whether the exponential worst-case bound is pessimistic in practice or whether the $\delta$ sets stay small.
  • The paper's undecidability proof depends on a cited reduction and on an asserted convergence property, so a natural next step is to construct full confluence and reduction details for the simultaneous variable-lifting system.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. This paper studies the right-divisibility problem for semi-Thue systems as a minimal model of intruder deduction: given words u and v, decide whether some w satisfies wu ≡_S v. The authors prove decidability for finite convergent prefix-erasing systems (Section 4, Theorem 4.6) and for finite convergent suffix-erasing systems (Section 5, Theorem 5.5), the latter by a backward-search algorithm using finite sets δ(c,u). They then introduce variable-lifting, subterm-lifting, and simultaneous variants over arbitrary term signatures, prove that simultaneous subterm-lifting systems are homeomorphic-embedded, exhibit a convergent variable-lifting theory that is not locally stable, and claim in Theorem 6.16 that deduction is undecidable for a convergent simultaneous variable-lifting TRS via a reduction from MPCP. The abstract presents the undecidability theorem as the boundary of the decidability landscape.

Significance. If the positive results hold, they are a useful contribution: Section 5 appears to be a genuinely new decidability result beyond the monadic boundary, and the backward-search algorithm is concrete and effectively implementable. Section 4 is honestly presented as a specialization of the Abadi--Cortier subterm-convergent decidability result, and its value lies in making the string-rewriting connection explicit and in the linear-time analysis. Section 6 also contains a helpful comparison of lifting classes with homeomorphic-embedded systems. The negative result, however, is not established: the constructed TRS in Theorem 6.16 is not confluent, and the reduction from MPCP is not actually described. Since the introduction and abstract advertise the undecidability result as the main boundary of the decidability landscape, this gap is load-bearing and not merely a presentation issue.

major comments (3)
  1. [Section 6.3, Theorem 6.16] The TRS constructed in the proof is not convergent. For an MPCP instance containing the pair (a,a), the rules include f(a(x),a(y),locked(z)) -> f(x,y,locked(z)) and f(x,x,locked(z)) -> f(x,x,z). The ground term t = f(a(a),a(a),locked(c)) rewrites via the first rule to f(a,a,locked(c)) and then via the unlock rule to f(a,a,c); it also rewrites via the unlock rule directly to f(a(a),a(a),c). Both target terms are irreducible and distinct, so the system has a non-joinable critical pair and is not confluent. Since the theorem asserts that the constructed system is convergent, this counterexample directly invalidates the proof as written.
  2. [Section 6.3, proof of Theorem 6.16] The undecidability claim is delegated rather than proved. The proof does not specify the encoding from an MPCP instance to a deduction instance: it gives no frame, no target term, and no argument that the MPCP instance has a solution exactly when the target is deducible. The sentence 'the correctness of reduction can be seen in [BSE+24]' is not sufficient, because [BSE+24] concerns graph-embedded and contracting TRSs, not the SVL class introduced here, and no transfer argument is supplied. Consequently, the abstract's claim of an undecidability boundary for convergent SVL systems rests on an unverified external assertion.
  3. [Theorem 4.6 and Appendix A.4] The complexity statements are internally inconsistent. Theorem 4.6 states a fixed-system running time of O(|u|+|v|), and the first combined bound in Appendix A.4 supports this. However, Corollary A.5 states that the procedure using the jump computation runs in O(ρL m^2 + ρL^2 m), which is O(m^2) for fixed S, while Proposition A.4 gives only O(ρL^2 n), also linear. The manuscript never reconciles these analyses, and the proof of Theorem 4.6 asserts linear-time normalization by citing [Boo82] while Appendix A.4 elsewhere charges O(ρL m^2) for normalization in a straightforward implementation. At least one of these analyses is wrong or refers to a different algorithm; the claimed linear-time theorem needs a single, coherent complexity analysis.
minor comments (4)
  1. [Section 5] In the paragraph after the statement of the decision problem, 'if u ⪯l_S v' should be 'if u ⪯r_S v'; the subscript is the wrong divisibility direction.
  2. [Proposition 6.7] 'local stabile' should be 'locally stable', and in the induction step the term denoted S'_1 is written as f(a,f(a,b)) instead of f(a,t_k), which makes the induction harder to follow.
  3. [Remark 6.11] The phrase 'TheinclusionofSVLinSSLisstrict: forexample' is missing spaces; there are also typos such as 'establishe' and 'right-divisbility' in Sections 1 and 5. A careful proofreading pass is needed.
  4. [Theorem 6.16] The proof describes the unlock rule f(x,x,locked(z)) -> f(x,x,z) as a simultaneous variable-lifting rule with n=2, but that rule erases only one context (n=1); the pair rules are the SVL rules with n=2. The union is still an SVL TRS, so this is only a misstatement.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the prefix- and suffix-erasing decidability proofs are self-contained, and the undecidability theorem's load-bearing reference is external, not a self-citation.

full rationale

No significant circularity found. Sections 4 and 5 supply self-contained decision procedures. Theorem 4.6 is proved from the suffix-multiple characterization (Lemmas 4.3-4.5) together with standard normalization for finite length-reducing systems; although the text notes that the result also follows from Abadi-Cortier [AC06], the proof does not import that result. Theorem 5.5 is proved directly via the finite backward sets delta(c,u) of Lemma 5.4, with no fitted parameters and no self-citation in the derivation. The only self-citations, [DT26] and [TNH16], appear in background or tool-survey remarks and are not load-bearing for the main decidability theorems. The proof of Theorem 6.16 delegates the MPCP reduction correctness to the external reference [BSE+24] and asserts convergence of the constructed simultaneous variable-lifting TRS without proof; this is a support and correctness gap rather than circularity, because [BSE+24] is not the present authors' work and no parameter is fitted and then renamed as a prediction. The paper's central positive claims are therefore not equivalent to their inputs by construction.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No free parameters or invented entities appear; the paper is a pure mathematical analysis. The axioms list the external results and unproved assumptions that the central claims depend on, especially the convergence and reduction correctness for Theorem 6.16.

assumptions (4)
  • standard math Undecidability of the modified Post correspondence problem (MPCP)
    Used in the reduction for Theorem 6.16.
  • domain assumption Decidability of deduction for subterm-convergent theories (Abadi-Cortier)
    Used to justify the prefix-erasing right-divisibility result in Section 4.
  • ad hoc to paper Correctness of the MPCP-to-deduction reduction from BSE+24
    The proof of Theorem 6.16 states the correctness can be seen in BSE+24 without reproducing it; this is an unproved assumption in the present paper.
  • ad hoc to paper Confluence of the constructed SVL TRS in Theorem 6.16
    The theorem asserts the TRS is convergent, but confluence is not proven and actually fails for instances with a matching first symbol.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Right Divisibility in Erasing Semi-Thue Systems: A Minimal View of Intruder Deduction." pith.science (2026). https://pith.science/paper/CNJKCR4Y

@misc{pith2026260803274,
  author       = {Pith},
  title        = {Pith review of: Right Divisibility in Erasing Semi-Thue Systems: A Minimal View of Intruder Deduction},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CNJKCR4Y}},
  note         = {Machine review of arXiv:2608.03274}
}
abstract

The intruder deduction problem is central to symbolic security-protocol analysis: it asks whether an attacker can derive a target message from observed messages using (cryptographic) operators available to the attacker. Although convergent rewrite systems provide canonical normal forms, deduction modulo convergent theories remains undecidable in general, and existing decidable fragments are often shaped by practical cryptographic examples. In this paper, we study deduction from a minimal structural perspective. When all function symbols are unary, terms collapse to words and deduction becomes a right-divisibility problem for semi-Thue systems: given words $u$ and $v$ decide whether there exists $w$ such that $wu \equiv_S v$. We investigate this problem for several classes of semi-Thue systems and prove, to the best of our knowledge, new decidability results for convergent prefix-erasing and convergent suffix-erasing systems. We then extend this perspective to term rewriting systems whose rules erase contexts while lifting selected subterms or variables. Although these classes suggest possible decidable generalisations beyond the unary setting, we show that deduction is already undecidable for a convergent simultaneous variable-lifting system. This exposes both the potential and the limits of extending the right-divisibility results to richer equational theories.

Figures

Figures reproduced from arXiv: 2608.03274 by the authors.

Figure 1
Figure 1. Relations between different TRS classes. [PITH_FULL_IMAGE:figures/full_fig_p016_1.png] view at source ↗

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

31 extracted references · 3 linked inside Pith

  1. [1]

    Theoretical Computer Science , volume=

    Deciding knowledge in security protocols under equational theories , author=. Theoretical Computer Science , volume=. 2006 , publisher=

    2006

  2. [2]

    Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or , booktitle =

    Hubert Comon. Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or , booktitle =. 2003 , url =. doi:10.1109/LICS.2003.1210067 , timestamp =

    arXiv 2003

  3. [4]

    International Conference on Logic for Programming Artificial Intelligence and Reasoning , pages=

    Deciding knowledge in security protocols for monoidal equational theories , author=. International Conference on Logic for Programming Artificial Intelligence and Reasoning , pages=. 2007 , organization=

    2007

  4. [5]

    arXiv preprint arXiv:2401.17226 , year=

    Knowledge problems in protocol analysis: Extending the notion of subterm convergent , author=. arXiv preprint arXiv:2401.17226 , year=

    arXiv

  5. [6]

    International Symposium on Logic-Based Program Synthesis and Transformation , pages=

    Deciding knowledge problems modulo classes of permutative theories , author=. International Symposium on Logic-Based Program Synthesis and Transformation , pages=. 2024 , organization=

    2024

  6. [7]

    IEEE Transactions on information theory , volume=

    On the security of public key protocols , author=. IEEE Transactions on information theory , volume=. 2003 , publisher=

    2003

  7. [8]

    Foundations and Trends

    Modeling and verifying security protocols with the applied pi calculus and ProVerif , author=. Foundations and Trends. 2016 , publisher=

    2016

  8. [9]

    Asian Symposium on Programming Languages and Systems , pages=

    SPEC: an equivalence checker for security protocols , author=. Asian Symposium on Programming Languages and Systems , pages=. 2016 , organization=

    2016

Show all 31 references
  1. [10]

    International Conference on Computer Aided Verification , pages=

    The DEEPSEC prover , author=. International Conference on Computer Aided Verification , pages=. 2018 , organization=

    2018

  2. [11]

    International conference on computer aided verification , pages=

    The TAMARIN prover for the symbolic analysis of security protocols , author=. International conference on computer aided verification , pages=. 2013 , organization=

    2013

  3. [12]

    ACM Transactions On Computational Logic (TOCL) , volume=

    YAPA: A generic tool for computing intruder knowledge , author=. ACM Transactions On Computational Logic (TOCL) , volume=. 2013 , publisher=

    2013

  4. [13]

    Journal of Automated Reasoning , volume=

    Computing knowledge in security protocols under convergent equational theories , author=. Journal of Automated Reasoning , volume=. 2012 , publisher=

    2012

  5. [14]

    Theoretical Computer Science , volume=

    Some undecidability results for non-monadic Church-Rosser Thue systems , author=. Theoretical Computer Science , volume=. 1984 , publisher=

    1984

  6. [15]

    International Conference on Rewriting Techniques and Applications , pages=

    Deciding algebraic properties of monoids presented by finite Church-Rosser Thue systems , author=. International Conference on Rewriting Techniques and Applications , pages=. 1985 , organization=

    1985

  7. [16]

    Semigroup Forum , volume=

    On two problems related to cancellativity , author=. Semigroup Forum , volume=. 1986 , organization=

    1986

  8. [17]

    Theoretical Computer Science , volume=

    Decidable sentences of Church-Rosser congruences , author=. Theoretical Computer Science , volume=. 1983 , publisher=

    1983

  9. [18]

    Semigroup Forum , volume=

    The word problem for one-relation monoids: a survey , author=. Semigroup Forum , volume=. 2021 , organization=

    2021

  10. [19]

    Acta Informatica , volume=

    Decision problems for finite special string-rewriting systems that are confluent on some congruence class , author=. Acta Informatica , volume=. 1991 , publisher=

    1991

  11. [20]

    2012 , publisher=

    Confluent string rewriting , author=. 2012 , publisher=

    2012

  12. [21]

    Advances in algorithms, languages, and complexity , pages=

    Properties of monoids that are presented by finite convergent string-rewriting systems—a survey , author=. Advances in algorithms, languages, and complexity , pages=. 1997 , publisher=

    1997

  13. [22]

    arXiv preprint arXiv:2103.00386 , year=

    On Problems Dual to Unification: The String-Rewriting Case , author=. arXiv preprint arXiv:2103.00386 , year=

    arXiv

  14. [23]

    Theoretical computer science , volume=

    Divisibility problem for one relator monoids , author=. Theoretical computer science , volume=. 2005 , publisher=

    2005

  15. [24]

    Theoretical computer science , volume=

    Equational unification, word unification, and 2nd-order equational unification , author=. Theoretical computer science , volume=. 1998 , publisher=

    1998

  16. [25]

    2021 IEEE symposium on security and privacy (SP) , pages=

    SoK: Computer-aided cryptography , author=. 2021 IEEE symposium on security and privacy (SP) , pages=. 2021 , organization=

    2021

  17. [26]

    Journal of Computer Security , volume=

    A survey of algebraic properties used in cryptographic protocols , author=. Journal of Computer Security , volume=. 2006 , publisher=

    2006

  18. [27]

    1998 , publisher=

    Term rewriting and all that , author=. 1998 , publisher=

    1998

  19. [28]

    String-Rewriting Systems , pages=

    String-rewriting systems , author=. String-Rewriting Systems , pages=. 1993 , publisher=

    1993

  20. [29]

    11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026) , pages=

    How Term Rewriting Structures Shape the Decidability of Knowledge Problems , author=. 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026) , pages=. 2026 , organization=

    2026

  21. [30]

    Journal of the ACM (JACM) , volume=

    Confluent and other types of Thue systems , author=. Journal of the ACM (JACM) , volume=. 1982 , publisher=

    1982

  22. [31]

    International Journal of Algebra and Computation , volume=

    Logical aspects of Cayley-graphs: the monoid case , author=. International Journal of Algebra and Computation , volume=. 2006 , publisher=

    2006

  23. [32]

    Discrete Mathematics & Theoretical Computer Science , volume=

    Cayley graphs of basic algebraic structures , author=. Discrete Mathematics & Theoretical Computer Science , volume=. 2020 , publisher=

    2020

Pith tools

Reviewed August 8, 2026 · model on record in the stance chip above.