{"id":"31308609-ae20-40e9-9a99-6322bc278e79","arxiv_id":"2608.03274","paper_version":2,"verdict":"REJECT","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"Right-divisibility is decidable for convergent prefix- and suffix-erasing semi-Thue systems, but the paper's undecidability proof for simultaneous variable-lifting term rewriting is flawed.","lead":"This paper studies when an attacker can derive a target word from observed messages using rewrite rules, reducing that question to a classical string-rewriting problem called right divisibility. It gives decision procedures for two erasing classes of such systems, and claims an undecidability boundary for a richer lifting class, though that proof is incomplete.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 6.16 is not established: the constructed SVL TRS is not confluent when the MPCP instance contains a pair (a,a), and the MPCP reduction is delegated to [BSE+24] without proof.","rationale":"The paper has two headline results: a positive decidability theorem for convergent suffix-erasing semi-Thue systems (Theorem 5.5) and a negative undecidability theorem for convergent simultaneous variable-lifting TRSs (Theorem 6.16). The reader's weakest-assumption analysis targets Theorem 6.16, and my independent check confirms that the constructed TRS is not confluent for an MPCP instance containing a pair (a,a). The explicit term f(a(a),a(a),locked(c)) rewrites to two distinct irreducible normal forms, so the system is not convergent. This is a concrete, load-bearing flaw: the undecidability result is advertised in the abstract as exposing the limits of extending the right-divisibility results, and without convergence the normal-form argument underpinning the reduction is absent. The proof also delegates the correctness of the MPCP reduction to an external reference without presenting the reduction, so the central negative claim is not self-contained. I do not see a comparably serious flaw in the positive suffix-erasing decision procedure; the confluence counterexample is specific to the term-rewriting construction in Section 6.3. Because the abstract's main boundary result depends on Theorem 6.16, and that theorem is not established as stated, the overall verdict of REJECT is appropriate.","tokens_in":20755,"tokens_out":6347,"duration_ms":69809,"concrete_test":"Fix Π={(a,a)} and run the rules of Theorem 6.16 on the term f(a(a),a(a),locked(c)); enumerate normal forms. If both f(a,a,c) and f(a(a),a(a),c) are reachable and irreducible, the TRS is not confluent. Independently, verify the claimed MPCP-to-deduction reduction by writing out the frame and target encoding and proving the equivalence, rather than citing [BSE+24].","verdict_should_be":"REJECT","load_bearing_attack":"Section 6.3 (Theorem 6.16) constructs, for an MPCP instance Π, the TRS with rules f(α_i(x), β_i(y), locked(z)) → f(x, y, locked(z)) for each pair (α_i,β_i) plus the unlock rule f(x,x,locked(z)) → f(x,x,z), and asserts that the resulting system is convergent. Take Π containing the pair (a,a) and consider the ground term t = f(a(a), a(a), locked(c)). The pair rule gives t → f(a,a,locked(c)) → f(a,a,c), the last step by the unlock rule with x=a, z=c. The unlock rule also gives t → f(a(a), a(a), c). Both f(a,a,c) and f(a(a),a(a),c) are irreducible and distinct, so the system has a non-joinable critical pair and is not confluent. Hence the 'convergent' hypothesis in Theorem 6.16 fails for this construction. Additionally, the proof does not describe the reduction from MPCP at all: after presenting the rules it says only 'The correctness of reduction can be seen in [BSE+24]', so the claimed undecidability of deduction for a convergent SVL TRS is unsupported. Since the abstract presents this undecidability result as the boundary of the decidability landscape, the central negative claim does not currently hold.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":21216,"tokens_out":12092,"duration_ms":122215,"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":[{"comment":"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.","section":"Section 6.3, Theorem 6.16"},{"comment":"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.","section":"Section 6.3, proof of Theorem 6.16"},{"comment":"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.","section":"Theorem 4.6 and Appendix A.4"}],"minor_comments":[{"comment":"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.","section":"Section 5"},{"comment":"'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.","section":"Proposition 6.7"},{"comment":"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.","section":"Remark 6.11"},{"comment":"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.","section":"Theorem 6.16"}],"recommendation":"reject","confidential_remarks":"The positive material in Sections 4 and 5 may be publishable on its own, but the advertised undecidability boundary is essential to the paper's narrative. The confluence counterexample shows that the current construction in Theorem 6.16 cannot be repaired by a local tweak, and the MPCP reduction is not present in the manuscript. The authors would need to supply a genuinely new proof of the undecidability claim or substantially re-scope the paper. I therefore recommend rejection rather than major revision, with the suggestion that a revised manuscript restricted to the positive results and open questions would deserve a fresh review."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know. First, the decidability result for convergent suffix-erasing (dwindling) systems (Theorem 5.5) looks genuinely solid: the backward search over delta sets is a real argument, and Lemma 5.4's finiteness proof is clean. Second, the advertised negative boundary, Theorem 6.16, does not hold as stated. The TRS built from an MPCP instance is not confluent, and the reduction correctness is merely delegated to [BSE+24] without proof.\n\nWhat is actually new: the prefix-erasing result is explicitly a special case of Abadi-Cortier, so the genuinely new positive content is the suffix-erasing decidability and the lifting framework. The paper is honest about the prefix-erasing provenance, and the complexity analysis is careful. The delta-graph perspective on Cayley graphs of such monoids is a useful observation.\n\nThe main soft spot is Theorem 6.16. For an instance containing the pair (a,a), the term f(a(a),a(a),locked(c)) rewrites to f(a,a,c) via the pair rule then the unlock rule, and also directly to f(a(a),a(a),c) via the unlock rule. Both targets are irreducible and distinct, so the system is not confluent. Convergence is asserted, not proved, and the reduction correctness is not described. That is load-bearing because the abstract sells this undecidability boundary as a key contribution.\n\nA second, more minor issue: AINP21 is cited as the source for \"dwindling systems,\" but the paper never compares its suffix-erasing decidability against that work, so the novelty claim is under-supported. The reversal-based dualities (Corollaries 4.8 and 5.7) are plausible but only sketched.\n\nWho this is for: people working on string rewriting and symbolic protocol analysis. The positive section could support a shorter paper; the negative theorem needs either a repaired construction with a full confluence proof and a described reduction, or removal. I would not cite the paper in its current form, but I would bring it to a reading group to discuss the gap between the positive and negative results.\n\nRecommendation: send to a serious referee, with the expectation of major revision. The positive results deserve scrutiny; the negative result as written is not established.","headline":"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].","tokens_in":21581,"tokens_out":3266,"would_cite":false,"duration_ms":32415,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q42","03D35","20M05"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["intruder deduction","semi-Thue systems","right divisibility","prefix-erasing systems","suffix-erasing systems","dwindling systems","term rewriting","convergent rewrite systems"],"falsifier":"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.","tokens_in":20559,"feed_emoji":"🧩","tokens_out":6449,"duration_ms":62223,"temperature":0.7,"pith_summary":"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.","feed_headline":"Right divisibility is decidable for erasing string-rewriting systems","feed_subtitle":"A minimal word model of intruder deduction draws the line between decidable and undecidable.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the subterm-convergent decidability framework and saturated sets that the prefix-erasing result specialises to the word level.","marker":"[AC06]"},{"why":"Provides the classical decidability result for right divisibility in finite confluent monadic systems that the paper extends beyond the monadic boundary.","marker":"[Boo83]"},{"why":"Gives the foundational theory of semi-Thue systems, confluence, and reversal that the paper uses throughout.","marker":"[BO93]"},{"why":"The paper cites it for the MPCP reduction behind the undecidability theorem and for the homeomorphic-embedding inclusion of lifting classes.","marker":"[BSE+24]"},{"why":"Introduces dwindling systems, the name used for convergent suffix-erasing systems, and the dual-unification motivation.","marker":"[AINP21]"},{"why":"Supplies the linear-time normalization result for fixed finite convergent length-reducing systems used in the prefix-erasing complexity bound.","marker":"[Boo82]"},{"why":"Provides the prior undecidability result for sufficiently general convergent theories that the simultaneous variable-lifting theorem refines.","marker":"[DT26]"}],"fun_headline_variants":["Erasing string systems: right divisibility is decidable","Word deduction via erasing: right divisibility decidable","Erasing rules decide right divisibility for word deduction"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Erasing string systems: right divisibility is decidable","Word deduction via erasing: right divisibility decidable","Erasing rules decide right divisibility for word deduction"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001292,"raw_usage":{"total_tokens":5292,"prompt_tokens":979,"completion_tokens":4313,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":595,"completion_tokens_details":{"reasoning_tokens":4261}},"tokens_in":595,"tokens_out":4313,"duration_ms":30496,"temperature":1.0,"reasoning_tokens":4261,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-08T00:47:04.102928+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":2}