Knowledge Problems in Protocol Analysis: Extending the Notion of Subterm Convergent

Referee: [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.

Authors: 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: yes

Referee: [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.

Authors: 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: yes