{"id":"39075ca2-31ce-43ee-98b4-5657ad720f55","arxiv_id":"2401.17226","paper_version":5,"verdict":"UNVERDICTED","confidence":"LOW","novelty_score":7.0,"correctness_risk":"unknown","formal_verification":"none","parameter_count":0,"one_line_summary":"Introduces graph-embedded convergent term rewrite systems, proves decidability of knowledge problems for the contracting convergent subclass, and undecidability for the full class, plus combination results.","lead":"The paper defines graph-embedded term rewrite systems as a flexible extension of subterm convergent systems and identifies a contracting convergent subclass for which deduction and static equivalence remain decidable in security protocol analysis. A generalist might read it to see how broader classes of equational theories can still support automated verification of protocol security properties.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.3","headline":"No significant objection identified","rationale":"The reader's weakest assumption correctly flags the key point that must be established for the decidability claim to hold. Because the paper states that it proves the claim for the new class, and no counterexample or missing reduction step is apparent, the assessment remains unverdicted pending full-text inspection but does not require adjustment on the basis of an identified flaw.","tokens_in":1753,"tokens_out":270,"duration_ms":18128,"concrete_test":"Re-derive the decidability claim for contracting convergent systems from the definitions of graph embedding and contraction (without assuming prior subterm-convergent results) and check whether the reduction to existing procedures holds uniformly for at least two non-subterm-convergent examples mentioned in the paper.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that knowledge problems (deduction and static equivalence) are decidable for the contracting convergent subclass of graph-embedded convergent systems and undecidable for the full graph-embedded class, with additional combination results. The abstract indicates that the paper supplies direct proofs for both the decidability result on the subclass and the undecidability result on the superclass, rather than relying on case-by-case verification. No internal gap in the argument structure is visible from the provided description.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.3","summary":"The paper introduces graph-embedded term rewrite systems, a generalization of homeomorphic embedding inspired by the graph minor relation. It defines the subclass of contracting convergent systems and claims that deduction and static equivalence (the knowledge problems) are decidable for contracting convergent systems, undecidable for the full class of graph-embedded convergent systems, and provides combination results both among contracting convergent systems and with certain permutative theories.","tokens_in":1843,"tokens_out":404,"duration_ms":16853,"significance":"If the decidability and undecidability results hold with direct proofs, the work supplies a new syntactic criterion under which existing decision procedures for protocol analysis apply without per-example verification, while delineating a boundary via undecidability. The combination theorems would further increase the class of equational theories amenable to automated analysis.","major_comments":[{"comment":"The central claim that contracting convergent systems inherit the termination and confluence properties needed for existing decision procedures to apply without additional case analysis rests on the syntactic restrictions; the manuscript must verify this preservation explicitly rather than assuming it follows from the definition alone.","section":"Definition of contracting convergent systems"},{"comment":"For the undecidability result on graph-embedded systems, the reduction must be shown to produce a system that satisfies the graph-embedded property while encoding an undecidable instance; any gap in the construction would undermine the separation from the decidable subclass.","section":"Undecidability section"}],"minor_comments":[{"comment":"Notation distinguishing graph-embedded from homeomorphic-embedded systems should be introduced with an explicit comparison table or example to improve readability.","section":null},{"comment":"The abstract would benefit from a one-sentence indication of the proof strategy (direct vs. reduction to prior results) for the decidability claim.","section":null}],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":{"model":"grok-4.3","summary":"We thank the referee for their careful reading and constructive comments, which help clarify the presentation of our results on graph-embedded term rewrite systems and their application to knowledge problems in protocol analysis. We address each major comment below.","responses":[{"response":"We agree that an explicit verification strengthens the manuscript. The contracting condition is defined to enforce a strict measure decrease on terms (via the graph embedding), which directly implies termination; confluence then follows from the local confluence check under this measure. In the revision we will add a dedicated lemma immediately after the definition, proving both properties from the syntactic restrictions without external assumptions, so that the applicability of existing decision procedures is fully justified within the paper.","revision_made":"yes","referee_comment":"[Definition of contracting convergent systems] The central claim that contracting convergent systems inherit the termination and confluence properties needed for existing decision procedures to apply without additional case analysis rests on the syntactic restrictions; the manuscript must verify this preservation explicitly rather than assuming it follows from the definition alone."},{"response":"The reduction in the undecidability proof is constructed so that every rule of the target system is obtained by a direct embedding-preserving transformation of the source instance; hence the resulting system satisfies the graph-embedded condition by construction. To eliminate any possible perception of a gap, the revised section will include an auxiliary claim that explicitly verifies the embedding relation for each rule generated by the reduction, together with a short argument that the undecidable problem instance is faithfully encoded.","revision_made":"yes","referee_comment":"[Undecidability section] For the undecidability result on graph-embedded systems, the reduction must be shown to produce a system that satisfies the graph-embedded property while encoding an undecidable instance; any gap in the construction would undermine the separation from the decidable subclass."}],"tokens_in":1374,"tokens_out":396,"duration_ms":16978,"standing_objections":[]},"desk_editor":{"model":"grok-4.3","letter":"The main takeaway is that the authors define a new syntactic restriction on convergent term rewrite systems that captures several examples people had been checking one at a time. They prove the usual deduction and static equivalence procedures still work on the contracting convergent subclass while showing undecidability for the broader graph-embedded class, and they add combination results for multiple such systems and with permutative theories. This reduces the need for separate arguments on each new theory. The definitions draw from graph minors as an extension of homeomorphic embedding, which gives a clean way to generalize the subterm case. The stress-test note indicates the proofs are direct rather than relying on fitting parameters or self-reference, which strengthens the claim. The comparisons to existing notions in the protocol literature also help place the new classes. One minor soft spot is that the contracting condition may still leave out some useful theories that analysts encounter, though the paper does not overclaim generality. The undecidability result mainly serves to mark the boundary and is not surprising on its own. Readers working on symbolic protocol analysis and decision procedures for equational theories will get the most from this. It is technical enough that a specialist in automated verification would find the new classes and the combination theorems worth knowing. The work shows clear engagement with the literature and supplies fresh results rather than restatements. An editor should send it for peer review.","headline":"The paper carves out graph-embedded and contracting convergent rewrite systems to get uniform decidability for knowledge problems on more protocol theories than subterm convergence alone.","tokens_in":2320,"tokens_out":344,"would_cite":false,"duration_ms":14301,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":{"model":"grok-4.3","evidence":[],"headline":"Term-rewriting decidability results for protocol knowledge problems unrelated to RS forcing chain","alignment":"orthogonal","rationale":"The paper defines graph-embedded TRSs and the contracting convergent subclass to obtain local stability (hence decidability of deduction/static equivalence) while proving undecidability for the full class; all results are syntactic and algorithmic in the domain of equational theories and intruder models. RS begins from a single distinction and forces J-cost, phi, 8-tick periodicity, 3D spacetime and the constants via the chain in reality_from_one_distinction and supporting modules (AbsoluteFloorClosure, Cost/FunctionalEquation, DimensionForcing, etc.). No shared primitives, cost functions, or structural theorems exist between the two.","tokens_in":61527,"confidence":"high","tokens_out":163,"duration_ms":5469,"cache_read_input_tokens":38528,"cache_creation_input_tokens":0},"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.3","headline":"The deduction and static equivalence problems are decidable for contracting convergent term rewrite systems but undecidable for graph-embedded ones.","keywords":["term rewriting","security protocols","deduction problem","static equivalence","decidability","convergence","graph embedding","protocol analysis"],"falsifier":"A specific contracting convergent rewrite system for which the deduction problem is shown to be undecidable.","tokens_in":2667,"feed_emoji":"","tokens_out":377,"duration_ms":14744,"temperature":0.7,"pith_summary":"The paper defines graph-embedded term rewrite systems as a flexible extension of subterm convergent systems for use in security protocol analysis. It identifies contracting convergent systems as a subclass where the two knowledge problems remain decidable using existing procedures. This covers many practical examples that previously required individual proofs. It proves undecidability for the full class of graph-embedded systems and gives combination results for multiple such systems and with permutative theories.","feed_headline":"Contracting convergent systems keep knowledge problems decidable","feed_subtitle":"A subclass of graph-embedded rewrite systems extends decidability results for protocol deduction and static equivalence beyond subterm cases","key_machinery":"Graph-embedded term rewrite systems, which extend the homeomorphic embedding property using a relation inspired by graph minors, with the contracting convergent subclass carrying the decidability results.","core_discovery":"Contracting convergent systems form a subclass of graph-embedded convergent term rewrite systems for which the knowledge problems of deduction and static equivalence are decidable, extending the reach of prior decision procedures beyond subterm convergent systems, while the same problems are undecidable in general for graph-embedded systems.","pith_inferences":[],"forward_implications":[],"fun_headline_variants":["Contracting convergent systems decidable for knowledge problems","Beyond subterm: contracting convergent knowledge problems decidable","Contracting convergent subclass decidable for protocol deduction","Knowledge problems remain decidable in contracting convergent systems"],"cache_read_input_tokens":2112,"weakest_assumption_plain":"The syntactic restrictions that define contracting convergent systems preserve termination and confluence so that existing decision procedures apply directly.","fun_headline_variants_meta":{"raw":{"variants":["Contracting convergent systems decidable for knowledge problems","Beyond subterm: contracting convergent knowledge problems decidable","Contracting convergent subclass decidable for protocol deduction","Knowledge problems remain decidable in contracting convergent systems"]},"model":"grok-4.3","cost_usd":0.009354,"raw_usage":{"total_tokens":4203,"prompt_tokens":708,"num_sources_used":0,"completion_tokens":52,"cost_in_usd_ticks":93537000,"prompt_tokens_details":{"text_tokens":708,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":3443,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":708,"tokens_out":52,"duration_ms":21587,"temperature":1.0,"reasoning_tokens":3443,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-05-24T04:11:55.011965+00:00","model_set":{"reader":"grok-4.3"},"falsifier":"A specific contracting convergent rewrite system for which the deduction problem is shown to be undecidable.","supporting_citations":[],"review_version":1}