{"id":"06450438-592d-4620-b1fa-a099c11b0823","arxiv_id":"2505.14514","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"The authors propose an SDLC taxonomy that refines first-level security properties into design-level sub-properties, and formalize a subset in Event-B to check consistency.","lead":"This paper organizes security goals like confidentiality and integrity into a tree of finer-grained sub-properties, pulled from attack-pattern databases, and then uses the Event-B formal method to check that the tree is internally consistent. A generalist might read it because it tries to make security requirements traceable from high-level goals down to concrete design decisions across the software lifecycle.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Event-B verification only proves internal consistency of hand-built models; the asserted correspondence between machine refinement and 'sub-security property' lacks any formal semantics, so the taxonomy's correctness is not actually verified.","rationale":"The paper's central claim is that Event-B formalization verifies the taxonomy's correctness. For that claim to hold, two things must be true: the Event-B machines must be faithful formalizations of the informal security properties, and the refinement relation must correspond to the intuitive 'sub-security property' relation. Neither is established. The reader's concern focuses on the second condition (refinement as a faithful counterpart of sub-property inclusion). Our stress-test finds that the first condition is even more load-bearing: without a formal semantics linking machines to security properties, refinement cannot be interpreted as implication between properties at all. Section V-B asserts the correspondence in one sentence, and Section V-C concludes correctness from discharged POs that only prove internal consistency of the hand-built models. The paper's own limitation (Section III.5) acknowledges that proving the model is built correctly does not mean it behaves as expected. The example in Section VII where formalization 'discovered' that Authenticity refines Integrity shows the taxonomy hierarchy is being adjusted to fit the models, not independently checked against a semantic criterion. We agree with the reader's conditional verdict: the taxonomy and methodology may be useful, but the verification claim needs major revision or reframing. Our concrete test would settle the issue on one representative edge, checking whether the formal refinement genuinely tracks a semantic implication between the properties.","tokens_in":12786,"tokens_out":4574,"duration_ms":42835,"concrete_test":"Take the Authenticity ⊑ Integrity edge (Section V-C/VII). First, give both properties a trace-based or LTL semantics (e.g., integrity = no unauthorized state modification; authenticity = source identification/spoofing prevention). Check whether the implication Authenticity ⇒ Integrity is valid under that semantics, e.g., with a model checker or a theorem prover. Second, re-formalize the two properties in Event-B using that semantics and check whether the refinement PO is discharged. If the semantic implication fails, or if the Event-B refinement succeeds while the semantic implication fails (or vice versa), the verification claim is invalidated. This would settle whether machine refinement tracks sub-property inclusion rather than merely modeler intent.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section V-C concludes 'All the models are proven correct by construction. This means that the taxonomy is promising.' This is a non-sequitur. The proof obligations generated by Rodin (Table II) are discharged for well-definedness, invariant preservation, and refinement of Event-B machines; they say nothing about whether those machines faithfully represent the informal security properties of Section IV. The machines in Fig. 4-5 use ad hoc variables (asset, ask_access, assetStatus) with no stated mapping to the natural-language definitions (e.g., 'not disclosed to unauthorized persons'). No formal semantics is given for what it means for a machine to satisfy 'integrity' or 'authenticity.' Consequently, the Event-B refinement of NonRepudiation_Mch by Integrity_Mch is a syntactic artifact of the modeler's choices, not a proven fact about the properties. The paper asserts in Section V-B that refinement 'reflects' that non-repudiation gets all properties of integrity and does not contradict it, but no argument shows refinement in Event-B coincides with semantic subsumption of the security properties. The validation via ProB animation (Section V-C) uses a small set of scenarios, and the authors admit non-exhaustive validation in Section VII. Thus the load-bearing link between formal verification and taxonomy correctness is missing.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes an SDLC-oriented taxonomy of security properties that decomposes high-level properties (confidentiality, integrity, availability, authorization, and human confidence) into sub-properties intended for use in requirements analysis and architecture design. The taxonomy is derived from CAPEC and ATT&CK repositories. To support the taxonomy's correctness, the authors formalize each property as an Event-B machine/context pair and use the Rodin provers to discharge proof obligations, together with ProB animation scenarios. The paper claims that this formalization verifies the taxonomy, and that refinement relations between Event-B machines reflect sub-property relationships. The central contribution is the taxonomy itself plus a methodology for building and formally checking it.","tokens_in":13046,"tokens_out":3927,"duration_ms":36521,"significance":"If the taxonomy's hierarchy were validated and its Event-B formalization were semantically faithful, the work could be a useful bridge between high-level security goals and concrete design activities, aiding requirements engineers and architects. The paper makes a concrete formalization effort using Event-B, reports proof obligations (Table II), and provides reproducible artifacts in principle (machines/contexts are shown in figures). It also makes a falsifiable claim: that the refinement relation among formal models matches the sub-property relation in the taxonomy. However, the current validation is substantially self-referential: the Event-B models are hand-written to encode the authors' own definitions, and the discharged POs establish only internal consistency, not that the models correctly represent the informal security properties. Therefore, the paper's significance as a verified taxonomy is not yet established, though the raw taxonomy may still be a useful resource for practitioners.","major_comments":[{"comment":"The claim that 'All the models are proven correct by construction' is unsupported. The proof obligations reported in Table II are discharged by Rodin for well-definedness, invariant preservation, and refinement of Event-B machines; they do not prove that the models faithfully represent the security properties defined in Section IV. No mapping is given between the natural-language definitions (e.g., 'not disclosed to unauthorized persons') and the Event-B variables/invariants shown in Fig. 4 (e.g., asset, ask_access, assetStatus). Without such a semantics, the Event-B machines are arbitrary formalizations, and their internal consistency does not validate the taxonomy.","section":"V-C"},{"comment":"The assertion that refinement of NonRepudiation_Mch by Integrity_Mch 'reflects that the NonRepudiation_Mch gets all the properties of Integrity_Mch and does not contradict it' is not justified. Event-B refinement is a behavioral consistency relation between two machines; it is not a semantic subsumption relation between informal security properties. The paper does not define what it means for a machine to satisfy 'authenticity' or 'integrity' as trace properties, nor does it prove that refinement in Event-B coincides with the taxonomy's sub-property relation. This is the load-bearing link between the formal verification and the taxonomy's correctness, and it is missing.","section":"V-B"},{"comment":"The validation by ProB animation, as described in items (1)-(5) and Fig. 6, does not constitute a proof. The text says that after one animation scenario 'this proves that the model is secure against this attack scenario,' but a single scenario (or a finite set of scenarios) cannot prove security without exhaustive model checking. The authors themselves acknowledge in Section VII that the validation is non-exhaustive. Consequently, the conclusion that 'this step of the taxonomy definition is correct' (end of Section V-C) is not supported by the evidence presented.","section":"V-C"},{"comment":"The taxonomy's correctness is not defined or independently checked against a stated criterion. The assignment of sub-properties to parents (e.g., making Authenticity a child of Integrity) is based on the authors' interpretation of CAPEC and ATT&CK entries, but no explicit subsumption rule is given. To support a correctness claim, the taxonomy should be accompanied by a criterion such as 'every violation of the child property is a violation of the parent property' (or its trace-level analogue), and the Event-B formalization should be constructed so that refinement provably enforces that criterion. As presented, the Event-B verification only checks the internal consistency of the authors' chosen models, so it cannot arbitrate whether the hierarchy is correct.","section":"III and IV"}],"minor_comments":[{"comment":"There is an inconsistency between the table and the text: Table I lists '3.4 Zero Source Leak' while the bullet list defines 'Zero resource leak' (CAPEC-131). The terminology should be unified.","section":"IV, Table I"},{"comment":"The Non-repudiation entry is defined without any source identifiers, whereas all other entries in Section IV include CAPEC or ATT&CK sources. Please add the relevant source or explain its absence.","section":"IV, Integrity bullet"},{"comment":"The phrase 'Sources CAPEC-624' lacks the colon used elsewhere (e.g., 'Sources: CAPEC-624'). This is a minor formatting issue.","section":"IV, Hardware non-interference"},{"comment":"The Event-B excerpt is abbreviated; it shows variables and events but not their full guards/actions or invariants. For reproducibility, consider providing a link to the complete machine/context files or a more complete listing, given that the verification claims depend on these details.","section":"V-B, Fig. 4"},{"comment":"The priority claim 'the first SDLC taxonomy of formalized security properties' appears twice (abstract and Section VI) and is not carefully qualified. The paper should explain more precisely how the cited formalizations of individual properties (e.g., Focardi and Gorrieri) differ from an SDLC-oriented taxonomy, rather than simply asserting novelty.","section":"VI"},{"comment":"The 'Human confidence' property is acknowledged as underdeveloped; since it appears as a first-level property in Table I, the paper should either mark it clearly as a placeholder or add a note about its provisional status in the taxonomy.","section":"VII"}],"recommendation":"major_revision","confidential_remarks":"The paper's core issue is that the Event-B verification does not validate the taxonomy's correctness; it only checks internal consistency of the authors' models. The taxonomy itself may be a useful practical artifact, but the paper should either (a) provide a formal semantics mapping each security property to trace predicates and prove refinement implies subsumption, or (b) substantially weaken the correctness claims and present the work as a taxonomy proposal with a formalization methodology. The current framing overstates what has been verified. The novelty claim about being the first SDLC taxonomy of formalized security properties is plausible but should be scoped against existing classification work (e.g., Focardi and Gorrieri). If the authors cannot supply the missing semantic link, the paper would be more honest as a position/vision paper, though it would then need to be repositioned to match its claims."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Core take: the taxonomy is a genuine practical contribution to security requirements engineering; the Event-B 'verification' does not actually validate it. The paper deserves a serious referee, but the formal claim in the abstract and Section V-C needs major rework.\n\nWhat's actually new: the specific hierarchy—Integrity decomposed into Non-repudiation, Authenticity, Pointer Integrity, Supply Chain Integrity with four lifecycle-stage children—is not in the prior work I've seen, and mapping each node to CAPEC/ATT&CK identifiers gives engineers a concrete bridge from 'what' to attack/defense patterns. The extraction process is transparent, and the authors are upfront about limitations (manual taxonomy updates, non-exhaustive validation, thin human-confidence branch).\n\nThe soft spot is load-bearing. Section V-C states 'All the models are proven correct by construction. This means that the taxonomy is promising.' Rodin's proof obligations discharge well-definedness, invariant preservation, and refinement consistency. They say nothing about whether the Event-B machines faithfully represent the informal security properties, nor whether Event-B refinement corresponds to 'is a sub-property of.' The authors assert that NonRepudiation_Mch refines Integrity_Mch and therefore non-repudiation inherits integrity, but no semantics is given for that correspondence. The formalization checks the internal consistency of hand-built models, not the correctness of the hierarchy. This is the circularity the stress-test note flags, and it lands.\n\nMinor issues: the Event-B artifacts are not shipped, so the Rodin numbers are not independently reproducible; the comparison to prior formal classifications (Focardi–Gorrieri, Aldini) is cursory; and the 'first SDLC taxonomy' claim is stronger than the literature survey supports.\n\nWho this is for: requirements engineers and architects who want a practical starting point for decomposing security objectives into design-level properties aligned with attack repositories. The taxonomy is plausible; the verification story is not. A serious referee should ask for revision: cut or reframe the 'correct by construction' claim, add a semantics linking refinement to sub-property inclusion, and make the models available.","headline":"The taxonomy is worth engaging with; the 'correct by construction' verification claim is not.","tokens_in":13561,"tokens_out":5357,"would_cite":true,"duration_ms":45559,"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 a formally verified, lifecycle-spanning taxonomy can decompose high-level security properties into design-level sub-properties.","keywords":["security properties","taxonomy","system development life cycle","Event-B","formal verification","refinement","requirements engineering","self-adaptive systems"],"falsifier":"Run the ProB model-checker on a taxonomy pair such as NonRepudiation_Mch refining Integrity_Mch and search for a reachable state in which an event the informal non-repudiation definition forbids is enabled; a single such counterexample trace would show that refinement provability does not by itself certify the taxonomy's sub-property relation.","tokens_in":12587,"feed_emoji":"🔐","tokens_out":6463,"duration_ms":64044,"temperature":0.7,"pith_summary":"The paper tries to establish that security properties such as confidentiality, integrity, availability, and authorization can be organized into a hierarchy that follows the phases of system development, so that a requirement-level goal like integrity can be decomposed into concrete sub-properties for design and implementation. The authors build the taxonomy by analyzing public attack-pattern and tactic repositories, then formalize each property as an Event-B model, a formal modelling language with machine refinement. They claim that machine refinement in Event-B mirrors the taxonomy's parent–child relation, and that because all proof obligations are discharged and the models are animated against attack scenarios, the taxonomy is promising. If the claim holds, requirement analysts and architects would have a shared, checkable bridge between what a system must preserve and how that can be designed and built.","feed_headline":"Event-B proofs back a lifecycle-wide security property taxonomy","feed_subtitle":"Requirement-level goals like integrity decompose into verified sub-properties for design and implementation.","key_machinery":"The load-bearing mechanism is Event-B machine refinement, verified with automated provers and validated by animation and model-checking. An Event-B model pairs a CONTEXT, containing static sets, constants, and axioms, with a MACHINE, containing variables, invariants, and events; when one machine refines another, the refinement proof obligations guarantee that the concrete behavior is consistent with and preserves the abstract behavior. The paper interprets this relation as the formal counterpart of the taxonomy's 'is-a-sub-property-of' hierarchy, with each child property's machine refining its parent property's machine.","core_discovery":"The central claim is that the proposed taxonomy is correct, and that its correctness can be checked by construction: each security property is formalized as an Event-B model, each proposed parent–child relation is rendered as a machine refinement, and the discharge of proof obligations plus animation of attack scenarios shows the hierarchy is sound. The paper's own example is the repositioning of authenticity: what began as a first-level property was moved to a sub-property of integrity when its model refined Integrity_Mch, illustrating that the formalization does real reorganizing work on the taxonomy.","pith_inferences":["The paper leaves implicit that Event-B refinement guarantees behavioral consistency, not semantic equivalence of the informal security notions; until that gap is closed, the verification evidence is supportive but not conclusive.","A natural extension would be to translate each formalized property into a runtime monitor or a self-adaptive controller condition, letting the taxonomy's 'what' become an enforceable 'how' during operation.","The same extraction-and-refinement process could be applied to vulnerability databases to generate lower-level properties automatically, which would make the taxonomy updateable at the pace of new attack data."],"forward_implications":["Requirement analysts can start from a high-level property such as integrity and select the taxonomy's sub-properties, instead of relying on ad hoc brainstorming, to produce component-level security requirements.","Architects can map each sub-property to architecture elements and later to code-level properties, keeping security concerns aligned with attack and defense refinements throughout the lifecycle.","A proposed new sub-property can be checked before adoption: if its Event-B machine does not refine the parent machine, the taxonomy needs adjustment.","The taxonomy can be embedded in a static interrelationship model that ties security requirements to architectural elements, supporting both building and verifying a system."],"supporting_citations":[{"why":"Supplies the Event-B language and its refinement semantics, which the paper uses to formalize every security property as a machine.","marker":"[2]"},{"why":"Provides the Rodin platform whose provers discharge the proof obligations for each formalized model.","marker":"[3]"},{"why":"Provides the ProB animator and model-checker used to validate the Event-B models against attack scenarios.","marker":"[22]"}],"fun_headline_variants":["Event-B proofs validate security property refinement","From what to how: Event-B checks security taxonomy","Machine-checked taxonomy for lifecycle security properties","Proof obligations confirm security property taxonomy","Formal verification backs SDLC security taxonomy"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The verification evidence stands on the assumption that an Event-B refinement between two machines means the corresponding informal security properties really stand in a sub-property relation, and the paper gives no independent argument for that equivalence.","fun_headline_variants_meta":{"raw":{"variants":["Event-B proofs validate security property refinement","From what to how: Event-B checks security taxonomy","Machine-checked taxonomy for lifecycle security properties","Proof obligations confirm security property taxonomy","Formal verification backs SDLC security taxonomy"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00091,"raw_usage":{"total_tokens":3825,"prompt_tokens":773,"completion_tokens":3052,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":389,"completion_tokens_details":{"reasoning_tokens":2987}},"tokens_in":389,"tokens_out":3052,"duration_ms":22329,"temperature":1.0,"reasoning_tokens":2987,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T15:32:26.715696+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the ProB model-checker on a taxonomy pair such as NonRepudiation_Mch refining Integrity_Mch and search for a reachable state in which an event the informal non-repudiation definition forbids is enabled; a single such counterexample trace would show that refinement provability does not by itself certify the taxonomy's sub-property relation.","supporting_citations":[{"cited_title":"Modeling in Event-B - System and Software Engineering","cited_arxiv_id":null,"evidence_quote":"Supplies the Event-B language and its refinement semantics, which the paper uses to formalize every security property as a machine."},{"cited_title":"Rodin: an open toolset for modelling and reasoning in event-b","cited_arxiv_id":null,"evidence_quote":"Provides the Rodin platform whose provers discharge the proof obligations for each formalized model."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the ProB animator and model-checker used to validate the Event-B models against attack scenarios."}],"review_version":1}