{"id":"a1d5f6a1-da15-49e3-9814-6631065c0b22","arxiv_id":"2506.01227","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":1,"one_line_summary":"SPEAR converts network configurations and vulnerabilities into an attack-connectivity hypergraph and uses AI planning to generate diverse hardening strategies that preserve connectivity.","lead":"This paper presents SPEAR, a framework that models a network's vulnerabilities and connections as an AI planning problem, then searches for diverse ways to harden the network while keeping services reachable. It is aimed at system administrators who want to test what-if scenarios before changing a live network.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1 completeness fails without an explicit one-node-per-host invariant: a valid ACG path can be invisible to the compiled planner because attack delete effects are applied host-wide rather than to the affected node.","rationale":"The reader's weakest assumption identifies the same underlying defect: Theorem 1's equivalence is unproved because the planning model does not track which node on a host supplied a fluent, and the ACG transition requires an exact source-node set. My analysis confirms the concern is real, but the precise failure direction differs from the reader's wording. The reader anticipated spurious plans (unsoundness), whereas the concrete counterexample above shows a failure of completeness: a valid ACG path exists that the compiled planner cannot find, because the planner's global delete effect removes an attribute that the ACG's node-relative transition preserves on a different node for the same host. For a security-hardening tool, missed real attack paths are at least as dangerous as phantom ones, so the central claim is not secure. The concern is load-bearing because every hardening suggestion, metric computation, and what-if analysis in Section 4 is performed on M_G, not on G. If M_G is not equivalent to G, then 'no plan found' in M_G does not mean the network is impenetrable, and 'minimum plan cost' may overstate the true attack difficulty. The paper's own definitions permit the problematic multi-node state: Definition 3 allows arbitrary node sets, and the connectivity transition λ adds nodes without removing the destination host's prior node. Thus the counterexample is not an artifact of an unreasonable interpretation; it follows from the formal text. I do not recommend a verdict change because the reader already assigned CONDITIONAL, which is the appropriate disposition: the framework may be repairable by adding an explicit one-node-per-host invariant, redefining connectivity transitions so they do not create duplicate nodes, and proving Theorem 1 under that invariant, but the current paper as written contains a false central theorem. The empirical evaluation is not the primary issue; the formal core needs a substantive correction before the tool's security claims can be accepted.","tokens_in":1305,"tokens_out":1280,"duration_ms":408553,"concrete_test":"Encode the counterexample in SPEAR's own PDDL generation pipeline: hosts A,B with φ_C(B,A)=True; S0_N={(A,{a}),(B,{b})}; connectivity edge B->A adding A{x}; attack T1 with pre={b}, add={z}, del={a} sourced from (A,{x}),(B,{b}); attack T2 with pre={a,z}, add={w}, del=∅ sourced from (A,{a}),(A,{x,z}),(B,{b}). Verify the ACG path S0_N -> {(A,{a}),(A,{x}),(B,{b})} -> {(A,{a}),(A,{x,z}),(B,{b})} -> {(A,{a}),(A,{x,z,w}),(B,{b})} exists. Then compile M_G per Definition 5 and run any classical planner for goal w. If the planner reports w unreachable while the ACG path is valid, Theorem 1(C2) is refuted. Alternatively, ask the authors to supply a proof of the missing one-node-per-host invariant; the transition rules as stated make it impossible to maintain.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing concern is Theorem 1 (Section 3): the representative planning model M_G is claimed to be sound and complete w.r.t. the ACG. The proof sketch in Section 3 silently assumes that each host contributes exactly one node to the current state, so that replacing the affected node (h_i,P_i) by (P_i\\post-)∪post+ has the same effect on the host's fluents as applying the action's global delete effect post-. The definitions do not state or prove that invariant, and it is false under the paper's own transition rules: λ(S_N,e_C) = S_N ∪ dest(e_C) can add a second node for a host that is already present. Concrete counterexample to completeness. Let H={A,B}, φ_C(A,B)=True. Initial S0_N={(A,{a}),(B,{b})}. Add a connectivity edge from (B,{b}) to (A,{x}), giving ACG state {(A,{a}),(A,{x}),(B,{b})}. Define attack T1 = ⟨pre={b}, post+={z}, post-={a}⟩ with edge src={(A,{x}),(B,{b})}, dest=(A,{x,z}); and attack T2 = ⟨pre={a,z}, post+={w}, post-=∅⟩ with edge src={(A,{a}),(A,{x,z}),(B,{b})}, dest=(A,{x,z,w}). In the ACG, T1 affects (A,{x}), so attribute a remains on (A,{a}); T2 is then applicable and w is reached. In M_G, however, the action for T1 has del(a) applied to host A globally, so the planner's state loses a, and T2's precondition a is unsatisfiable. Hence a valid attack path exists in G with no corresponding plan in M_G, contradicting Theorem 1(C2). The missing 'each host holds exactly one node' constraint is therefore not cosmetic: it is load-bearing for the central equivalence.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces the Attack-Connectivity Graph (ACG), a hypergraph model combining attack dependencies with network connectivity, and proposes SPEAR, a framework that compiles an ACG into a classical planning model in PDDL. On this compiled model, the paper defines robustness metrics (impenetrability and attack difficulty), an A*-based search for diverse hardening updates, an admissible heuristic based on top-K attack plans, and an empirical evaluation on a testbed and synthetic networks. The main formal claims are soundness and completeness of the planning compilation (Theorem 1), complexity results for attack/connectivity path existence (Theorem 2), and guarantees for the model-update search (Propositions 1–4).","tokens_in":20086,"tokens_out":17405,"duration_ms":166787,"significance":"The paper addresses a real gap in network hardening: jointly reasoning about attack reachability and connectivity while supporting human-in-the-loop what-if analysis. The hypergraph-plus-planning framing is promising and the authors provide a tool and a concrete case study. If the central equivalence were correct, the complexity results and the compositional treatment of connectivity would be useful contributions. However, the main theorem is currently unproven and false under the stated definitions, so the framework's formal guarantees do not transfer from the planning model to the ACG. The paper needs substantial revision before its central claims are credible.","major_comments":[{"comment":"","section":"Section 3, Definition 5 / Theorem 1"},{"comment":"","section":"Section 4.2, Definition 11"},{"comment":"","section":"Section 7, Table 1"}],"minor_comments":[{"comment":"The monotonicity condition 'FA(E1)≥FA(E2), if and only if, E1⊆E2' is a biconditional and would force FA to be injective; it should be an implication ('if E1⊆E2 then FA(E1)≥FA(E2)').","section":"Section 3, Definition 7"},{"comment":"The condition 'if {f}∪C has no subset in C' is unclear and appears to use C for both the current node and the closed list; based on the surrounding text it should check that the new update set is not a superset of an already discovered solution.","section":"Section 4.2, Algorithm 2"},{"comment":"The proof claims solutions are tested 'in order of increasing cardinality,' but this is not guaranteed when the heuristic equals 1: a size k+1 goal and a size k goal can then have equal f-cost, and tie-breaking may pop the larger first. The non-overlap guarantee needs a tie-breaking rule or a stricter bound on the heuristic.","section":"Section 4.2, Proposition 3"},{"comment":"Even if Theorem 1 is repaired, the membership argument for attack-path existence should be made precise: the reference to positive-precondition STRIPS must account for the unrestricted delete effects in the compiled actions, and the reduction must be shown to preserve both directions of plan/path existence.","section":"Theorem 2, proof sketch"}],"recommendation":"major_revision","confidential_remarks":"The paper is aimed at a security conference format, which may explain the proof sketches, but the issues are more than local typos: the compilation in Definition 5 must be reworked or the ACG restricted to one node per host, and Definition 11 must be corrected. The empirical evaluation is limited and the heuristic claim is contradicted by one of the paper's own tables. I would not recommend acceptance in the current form; however, the approach is salvageable and a careful revision could make the formal claims credible."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The load-bearing claim is Theorem 1, and it does not hold as stated. The stress-test counterexample is valid. The ACG transition function removes the specific source node (h_i, P_i) when an attack fires, so another node for the same host can keep attribute a. The compiled PDDL action applies del(a) to the whole host, so the planner loses a. I traced the example with hosts A, B and attacks T1, T2: the ACG reaches w, the planner cannot. Both soundness and completeness are affected, because the planning state is a union of fluents and does not track which node set contributed them. The proof sketch silently assumes one node per host. That invariant is not in Definitions 3 or 5 and is false once connectivity edges add a second node for a host already represented.\n\nThis is a pity, because the rest of the paper is genuinely useful. The ACG hypergraph, the non-monotonic compilation to PDDL, the impenetrability and attack-difficulty metrics, the constrained-model A* with the admissible heuristic, and the non-overlapping diverse solution generation are a real combination I have not seen in the attack-graph literature. The complexity claims are plausible if Theorem 1 is repaired, and Proposition 1 is straightforward for positive-precondition STRIPS. The empirical evaluation is honest enough to show the heuristic is not always faster, but the tables are noisy and the scale caps at 30 synthetic nodes; no artifacts are released, so I cannot check the PDDL generation.\n\nThe paper deserves a serious referee, but it is not ready as is. The authors need to either add the one-node-per-host invariant (and show it is preserved by all transitions) or change the compilation so that node identity is tracked, e.g. by fluents indexed by node id. They should also prove Theorem 1 for both directions under the revised invariant. If they do that, the framework is publishable. If not, the hardening suggestions are not guaranteed to correspond to actual attack paths.","headline":"Theorem 1 has a real soundness/completeness gap that is load-bearing for the whole framework, but SPEAR's ACG hypergraph and diverse-hardening search are novel enough to warrant a serious revision.","tokens_in":20574,"tokens_out":3774,"would_cite":false,"duration_ms":41652,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that an attack-connectivity hypergraph and its compiled planning model are exactly equivalent—same attack paths, same connectivity paths—so hardening advice can be computed by planning and then re-checked against the graph.","keywords":["Attack-Connectivity Graph","AI planning","network hardening","PDDL","what-if analysis","attack graph","hypergraph","security posture"],"falsifier":"Build a two-host ACG where one host starts with attributes {p, q} and an attack hyperedge has a source node carrying only {p}, preconditions {p}, and a destination adding attribute r. In the planning model the initial state contains both p and q, so the attack action is applicable and produces a plan leading to r, while in the ACG the transition function requires the exact source node (host, {p}) to be present and therefore no valid attack path to r exists. Running SPEAR on this instance and observing a suggested attack plan (or a hardening edit based on it) would falsify Theorem 1 as stated.","tokens_in":19483,"feed_emoji":"🛡️","tokens_out":5295,"duration_ms":49829,"temperature":0.7,"pith_summary":"SPEAR argues that the attack-connectivity hypergraph of a network and a classical AI planning model built from it are two views of the same object: every attack path in the graph is an action plan in the model, and every plan corresponds to a real path. If that equivalence holds, defenders can hand a network to an off-the-shelf planner and get, in return, not just attack paths but concrete hardening edits—changes to software versions, configurations, or reachability—that cut all attack paths to a target while preserving connectivity paths to that target. The paper also formalizes two robustness metrics (impenetrability and attack difficulty) and gives a search algorithm that returns diverse, non-overlapping sets of hardening changes so a human administrator can choose among them when exact costs are unknown. The reason this matters is human-in-the-loop: rather than optimizing a single cost function, the administrator sees several qualitatively different ways to block an attacker and can weigh implementation difficulty themselves.","feed_headline":"Attack graphs become planning problems, losslessly","feed_subtitle":"SPEAR compiles network hypergraphs into PDDL so admins can test hardening moves before deploying them.","key_machinery":"The carrying object is the Attack-Connectivity Graph (ACG), a hypergraph whose nodes are all pairs (host, attribute set) and whose edges are either connectivity edges between hosts or attack hyperedges from a set of source nodes to a destination node; it is non-monotonic (attacks may delete attributes) and may contain cycles. Its companion is the representative planning model M_G in PDDL/STRIPS, built by mapping every host-attribute pair to a fluent and every edge to an action, with the precondition of an action equal to the union of the fluents of its source nodes. Theorem 1's soundness and completeness equivalence is what licenses every downstream step: finding plans instead of graph paths, the PSPACE-completeness result for attack paths, the polynomial connectivity result via delete-free actions, the A*-search over constraining changes (limited to κ(M), the initial-state and add-effect parameters), and the compiled model M_α that computes attack difficulty as the cost of an optimal plan.","core_discovery":"The central claim is Theorem 1: for a given ACG G, initial node set S0_N, and target node n_t, the representative planning model M_G is sound and complete—a valid plan exists in M_G if and only if a valid connectivity or attack path exists in G. Nodes of the ACG are host-attribute-set pairs; connectivity edges and attack hyperedges become actions whose preconditions are the unions of the source nodes' attribute fluents, whose add and delete effects are the postconditions of the attack, and whose initial and goal states encode the given attacker start and target. The paper claims this planning formulation is lossless, which makes the follow-on results possible: attack-path existence is PSPACE-complete, connectivity-path existence is polynomial, hardening reduces to constraining away all attack plans while keeping a connectivity plan, and the minimum-cost-of-attack metric can be computed by a small compiled model that lets the planner choose the initial state and the target. The practical translation is that what-if analysis over an attack graph can be performed by editing the planning model and re-solving it.","pith_inferences":["Editorial inference: the soundness-completeness equivalence is only as tight as the state-tracking discipline; unless each host is constrained to hold exactly one node's attribute set, the planner can apply an attack whose preconditions are a proper subset of a host's current attributes while the ACG transition requires the exact source node, potentially creating phantom plans.","Editorial inference: the framework's central promise could be tested end-to-end by comparing planner-derived hardening suggestions against a ground-truth penetration test on the same network, a validation the paper does not report.","Editorial inference: the constraining-changes insight (only initial-state and add-effect removals can invalidate previous plans) may carry over to other security analyses, such as k-zero-day safety, where the goal is to block newly introduced attacker capabilities.","Editorial inference: because the ACG treats connectivity as a replaceable relation, the same machinery could be adapted to quantitative service-availability or latency targets rather than the indicator connectivity function used here."],"forward_implications":["If Theorem 1 holds, every valid plan produced by the planner in M_G corresponds to a genuine attack or connectivity path, so any hardening suggestion derived from blocking plans is grounded in actual graph paths.","Hardening to the impenetrability metric means making the attack-plan set empty while preserving a connectivity plan; the A* search with the proposed admissible heuristic guarantees an optimal set of model updates when costs are uniform.","The attack-difficulty metric equals the optimal plan cost of the compiled model M_α, so raising the required threshold forces the attacker's shortest path cost up by at least the chosen amount.","The non-overlapping solution set produced by the modified A* search lets an administrator choose among qualitatively different hardening strategies when modification costs are partially or wholly unspecified.","Relaxing the monotonicity assumption allows the framework to model lateral movement, revisits, and attribute loss, which earlier monotonic attack-graph frameworks cannot express."],"supporting_citations":[{"why":"Supplies the PSPACE-completeness of positive-precondition STRIPS planning that Theorem 2 uses to classify attack-path existence.","marker":"[7]"},{"why":"Supplies the result that plan existence with delete-free actions is polynomial, used for the connectivity-path complexity claim.","marker":"[16]"},{"why":"Introduces attack trees, the modeling paradigm that the ACG generalizes into a hypergraph with connectivity edges.","marker":"[33]"},{"why":"Presents MulVAL, the logic-based attack-graph analyzer that SPEAR positions itself against.","marker":"[27]"},{"why":"Represents the multi-objective optimization approach to hardening that SPEAR contrasts with its what-if analysis.","marker":"[9]"},{"why":"Identifies the monotonicity assumption that most prior attack-graph frameworks make, which SPEAR deliberately relaxes.","marker":"[15]"},{"why":"Provides the model-parameterization conventions that SPEAR's δ function and constraining-changes analysis follow.","marker":"[34]"},{"why":"Provides the model-reconciliation foundations for defining constrained versions of a planning model.","marker":"[35]"}],"fun_headline_variants":["Attack graphs as planning problems: lossless conversion","SPEAR compiles attack graphs to PDDL for what-if analysis","From attack hypergraphs to PDDL: lossless security planning","Attack graph to PDDL: sound and complete planning","Security hardening via PDDL planning on attack hypergraphs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The equivalence in Theorem 1 assumes that an action's preconditions can be represented simply as the union of the attribute fluents of its source nodes, so the planner may apply an attack whenever those fluents are present even if the affected host's attribute set is a proper superset of the source node's attribute set, whereas the ACG transition requires the exact source node set to be present.","fun_headline_variants_meta":{"raw":{"variants":["Attack graphs as planning problems: lossless conversion","SPEAR compiles attack graphs to PDDL for what-if analysis","From attack hypergraphs to PDDL: lossless security planning","Attack graph to PDDL: sound and complete planning","Security hardening via PDDL planning on attack hypergraphs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000527,"raw_usage":{"total_tokens":2538,"prompt_tokens":938,"completion_tokens":1600,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":554,"completion_tokens_details":{"reasoning_tokens":1516}},"tokens_in":554,"tokens_out":1600,"duration_ms":9581,"temperature":1.0,"reasoning_tokens":1516,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T11:47:12.562760+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Build a two-host ACG where one host starts with attributes {p, q} and an attack hyperedge has a source node carrying only {p}, preconditions {p}, and a destination adding attribute r. In the planning model the initial state contains both p and q, so the attack action is applicable and produces a plan leading to r, while in the ACG the transition function requires the exact source node (host, {p}) to be present and therefore no valid attack path to r exists. Running SPEAR on this instance and observing a suggested attack plan (or a hardening edit based on it) would falsify Theorem 1 as stated.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the PSPACE-completeness of positive-precondition STRIPS planning that Theorem 2 uses to classify attack-path existence."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the result that plan existence with delete-free actions is polynomial, used for the connectivity-path complexity claim."},{"cited_title":"Schneier","cited_arxiv_id":null,"evidence_quote":"Introduces attack trees, the modeling paradigm that the ACG generalizes into a hypergraph with connectivity edges."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Presents MulVAL, the logic-based attack-graph analyzer that SPEAR positions itself against."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Represents the multi-objective optimization approach to hardening that SPEAR contrasts with its what-if analysis."},{"cited_title":"Dijkstra","cited_arxiv_id":null,"evidence_quote":"Identifies the monotonicity assumption that most prior attack-graph frameworks make, which SPEAR deliberately relaxes."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the model-parameterization conventions that SPEAR's δ function and constraining-changes analysis follow."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the model-reconciliation foundations for defining constrained versions of a planning model."}],"review_version":1}