Pith. sign in

REVIEW 4 major objections 6 minor 40 references

From What to How: A Taxonomy of Formalized Security Properties

T0 review · 4 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper claims that a formally verified, lifecycle-spanning taxonomy can decompose high-level security properties into design-level sub-properties.

desk verdict The taxonomy is worth engaging with; the 'correct by construction' verification claim is not. read the letter →

arxiv 2505.14514 v1 pith:F5XR2TO6 submitted 2025-05-20 cs.SE

Imen Sayar , Nan Messe , Sophie Ebersold , Jean-Michel Bruel This is my paper · ORCID
classification cs.SE
keywords securitypropertiestaxonomysystemdevelopmentlifecycleEvent-Bformalverificationrefinementrequirementsengineeringself-adaptivesystems
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 6 minor

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.

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 (4)
  1. [V-C] 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.
  2. [V-B] 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.
  3. [V-C] 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.
  4. [III and IV] 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.
minor comments (6)
  1. [IV, Table I] 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.
  2. [IV, Integrity bullet] 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.
  3. [IV, Hardware non-interference] The phrase 'Sources CAPEC-624' lacks the colon used elsewhere (e.g., 'Sources: CAPEC-624'). This is a minor formatting issue.
  4. [V-B, Fig. 4] 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.
  5. [VI] 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.
  6. [VII] 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.

Circularity Check

3 steps flagged · score 6.0 of 10

The Event-B 'correctness check' of the taxonomy is self-referential: the machine refinement hierarchy is authored to mirror the taxonomy, then discharged proof obligations are cited as evidence that the taxonomy hierarchy is correct.

  1. self definitional [Section V-B, paragraph beginning 'A powerful concept of the Event-B model is the refinement strategy.']
    "A powerful concept of the Event-B model is the refinement strategy. This concept ensures the correction of the proposed taxonomy. In fact, when a concrete machine like NonRepudiation_Mch refines another one such as Integrity_Mch, this reflects that the NonRepudiation_Mch gets all the properties of Integrity_Mch and does not contradict it."

    The refinement relation is a modeling choice made by the authors: the machines are named and structured according to Table I, where Non-repudiation and Authenticity are already listed as children of Integrity. No independent semantics is given that identifies Event-B refinement with the informal 'sub-security property' relation. The refinement POs, when discharged, only show that the hand-written concrete machine is a consistent strengthening of the hand-written abstract machine; they do not show that the informal security-property hierarchy is correct.

  2. fitted input called prediction [Section V-C, paragraph discussing Figure 7 and the conclusion about Authenticity.]
    "At the same time, since this machine is refining the Integrity_Mch, the sequence of the abstract events INITIALISATION ask_modify_asset and refuse_modify_asset is animated. This is relevant to show that the behavior of the concrete machine is respecting the behavior of the abstract one. This concludes that this step of the taxonomy definition (Authenticity is a sub-property of the Integrity property) is correct."

    The animation is produced from the same Event-B models whose refinement edge was inserted precisely to encode the taxonomy relation. The observed compatible behavior is a property of the author-built model, not an independent check on the informal properties. Phrasing this as a conclusion that Authenticity is a sub-property of Integrity converts the modeling assumption into the verification result, which is the fitted-input-called-prediction pattern.

1 more flagged steps
  1. self definitional [Section VII, Discussion, paragraph beginning 'Secondly, our taxonomy is promising thanks to its formalization using the Event-B language.']
    "When formalizing the integrity security property, we discovered that authenticity is in fact a refinement of integrity. Indeed, according to their definitions, the 'identity resource' in authenticity refines the 'data asset' in integrity, and 'spoofed' in authenticity refines 'misused' in integrity."

    The 'discovery' is a direct consequence of the authors' formalization decisions: they map 'identity resource' to the asset variable and 'spoofed' to the misused status in the Event-B machine. Those mappings are inputs chosen before the refinement is proved. The resulting refinement therefore reflects the modelers' prior interpretation of the concepts; it cannot serve as independent evidence that the taxonomy's hierarchy is correct.

full rationale

The taxonomy itself has independent content: it is assembled from the CAPEC and ATT&CK repositories and organized into levels, and this compilation is not circular. However, the paper's stated verification claim, that Event-B is used to check the correctness of the taxonomy, is circular in execution. Authenticity is placed under Integrity in Table I, and the corresponding machine Authenticity_Mch is declared to refine Integrity_Mch. The discharged proof obligations and ProB animations then confirm that these hand-written models are internally consistent and that the chosen refinement edges hold in the chosen state model. None of this establishes that Event-B refinement coincides with the informal 'sub-security property' relation, nor that the informal definitions are faithfully represented. The discussion section exposes the reduction: the authors say they 'discovered' that authenticity refines integrity because the 'identity resource' in authenticity was mapped to the 'data asset' in integrity and 'spoofed' was mapped to 'misused' in the machine. These mappings are modeling choices, not external findings. The conclusion that 'All the models are proven correct by construction. This means that the taxonomy is promising' moves from internal consistency of a self-made model to correctness of the taxonomy by assuming the model is a faithful counterpart of the taxonomy, which is exactly the point at issue. No load-bearing self-citation chain is present, so the score is not raised on that ground; the circularity is in the verification design. The admitted non-exhaustive validation in Section VII also does not close the gap, since it only limits the reach of the animation evidence rather than providing an independent link between refinement and sub-property semantics.

Assumptions & free parameters 3 free parameters · 4 assumptions · 0 invented entities

The central contribution, the hierarchy of sub-security properties, is a hand-constructed artifact. Its load-bearing assumptions are that the Event-B encoding captures the informal definitions and that refinement matches sub-property inclusion. The proof obligations then check the internal consistency of a model the authors wrote, not the validity of the taxonomy against external ground truth.

free parameters (3)
  • Top-level security property set = Confidentiality, Integrity, Availability, Authorization, Human Confidence
    Chosen from ISO/IEC 27000 and NIST CSRC (Section III step 1); the selection determines the root branches of the taxonomy. Human Confidence is added by the authors, and Non-repudiation is placed under Integrity rather than as a root.
  • Parent-child assignments in the taxonomy = e.g., Authenticity under Integrity; Sensitive Information Untraceability under Confidentiality
    Each mapping from a CAPEC/ATT&CK pattern to a property and each edge in the tree is made by the authors' judgment (Section IV). No algorithm or inter-rater study is provided, so the hierarchy itself is a set of hand-chosen parameters.
  • Event-B model structure per property = e.g., Integrity_Mch variables asset, ask_access, assetStatus; events ask_modify_asset, refuse_modify_asset, reinitialise
    The variables, invariants, and events are authored manually to express each property (Section V-B). A different encoding would produce different proof obligations and different animation behavior.
assumptions (4)
  • standard math Event-B proof obligation discharge establishes that the Event-B model is internally consistent
    Rodin's PO generation and provers are standard tools; the paper relies on them in Section V-C to claim the models are 'proven correct by construction'.
  • domain assumption Event-B machine refinement is equivalent to the taxonomic 'sub-security property' relation
    Section V-B states that NonRepudiation_Mch refining Integrity_Mch 'reflects that the NonRepudiation_Mch gets all the properties of Integrity_Mch'. This equivalence is asserted, not proved.
  • ad hoc to paper CAPEC Meta Attack Patterns and ATT&CK Tactics are an adequate and authoritative source for enumerating design-level security properties
    The taxonomy is extracted from these two MITRE repositories (Sections II and III); the paper provides no argument that this source set covers all relevant sub-properties, and it admits social engineering is underrepresented.
  • domain assumption Informal security property definitions can be unambiguously encoded as Event-B variables and events
    Section V-B maps concepts like 'data asset' to the SYSTASSET set and 'misused' to ASSETSSTATUS; the encoding is a modeling choice that determines what the POs and animations can show.

how reviews work

0 comments
Cite this review

Pith. "Pith review of From What to How: A Taxonomy of Formalized Security Properties." pith.science (2026). https://pith.science/paper/F5XR2TO6

@misc{pith2026250514514,
  author       = {Pith},
  title        = {Pith review of: From What to How: A Taxonomy of Formalized Security Properties},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/F5XR2TO6}},
  note         = {Machine review of arXiv:2505.14514}
}
read the original abstract

Confidentiality, integrity, availability, authenticity, authorization, and accountability are known as security properties that secure systems should preserve. They are usually considered as security final goals that are achieved by system development activities, either in a direct or an indirect manner. However, these security properties are mainly elicited in the high-level requirement phase during the System Development Life Cycle (SDLC) and are not refined throughout the latter phases as other artifacts such as attacks, defenses, and system assets. To align security properties refinement with attacks, defenses, and system assets refinements, we propose an SDLC taxonomy of security properties that may be used in a self-adaptive context and present the methodology for defining it. To verify and check the correctness of the resulting taxonomy, we use the Event-B formal language.

Figures

Figures reproduced from arXiv: 2505.14514 by the authors.

Figure 1
Figure 1. Security artifacts refinement model security requirements, and provide mitigation controls which will be rendered as architecture decisions [25]. Consequently, the resulting architectural decisions are highly dependent on human expertise and the chosen tools. Moreover, in each phase of the SDLC, and particularly in the requirements definition phase, checking whether lower￾level (e.g., component-level) requirements d… view at source ↗
Figure 3
Figure 3. Extracting and verifying security properties process [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 5
Figure 5. This viewpoint diagram is obtained using the Event [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Machine seeing a Context represented by the right (pink) boxes. A powerful concept of the Event-B model is the refinement strategy. This con￾cept ensures the correction of the proposed taxonomy. In fact, when a concrete machine like NonRepudiation_Mch refines another o…
Figure 5
Figure 5. Figure 5: The formalized taxonomy classification for the Integrity property and its descendants. [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]
Figure 6
Figure 6. Figure 6: Animation and model-checking of the Integrity property using the ProB tool. [PITH_FULL_IMAGE:figures/full_fig_p009_6.png]
Figure 7
Figure 7. Figure 7: Concrete (left side of the figure) and abstract (right side) simulation [PITH_FULL_IMAGE:figures/full_fig_p010_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

40 extracted references · 39 canonical work pages

  1. [1]

    The B-book - assigning programs to meanings

    Jean-Raymond Abrial. The B-book - assigning programs to meanings . Cambridge University Press, 2005

    work page 2005

  2. [2]

    Modeling in Event-B - System and Software Engineering

    Jean-Raymond Abrial. Modeling in Event-B - System and Software Engineering. Cambridge University Press, 2010

    work page 2010

  3. [3]

    Rodin: an open toolset for modelling and reasoning in event-b

    Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, and Laurent V oisin. Rodin: an open toolset for modelling and reasoning in event-b. International journal on software tools for technology transfer , 12(6):447–466, 2010

    work page 2010

  4. [4]

    Classification of security properties in a linda-like process algebra

    Alessandro Aldini. Classification of security properties in a linda-like process algebra. Science of Computer Programming, 63(1):16–38, 2006

    work page 2006

  5. [5]

    Software penetration testing

    Brad Arkin, Scott Stender, and Gary McGraw. Software penetration testing. IEEE Security & Privacy , 3(1):84–87, 2005

    2005

  6. [6]

    A serious game for eliciting social engineering security requirements

    Kristian Beckers and Sebastian Pape. A serious game for eliciting social engineering security requirements. In 2016 IEEE 24th International Requirements Engineering Conference (RE) , pages 16–25. IEEE, 2016

    work page 2016

  7. [7]

    Multidimensional divide-and-conquer

    Jon Louis Bentley. Multidimensional divide-and-conquer. Communica- tions of the ACM , 23(4):214–229, 1980

    work page 1980

  8. [8]

    Less is more: supporting developers in vulnerability detection during code review

    Larissa Braz, Christian Aeberhard, G ¨ul C ¸ alikli, and Alberto Bacchelli. Less is more: supporting developers in vulnerability detection during code review. In Proceedings of the 44th International Conference on Software Engineering, pages 1317–1329, 2022

    work page 2022

Show all 40 references
  1. [9]

    The role of formalism in system requirements

    Jean-Michel Bruel, Sophie Ebersold, Florian Galinier, Manuel Mazzara, Alexandr Naumchev, and Bertrand Meyer. The role of formalism in system requirements. ACM Computing Surveys (CSUR) , 54(5):1–36, 2021

    2021

  2. [10]

    SMT Solvers for Rodin

    David D ´eharbe, Pascal Fontaine, Yoann Guyot, and Laurent V oisin. SMT Solvers for Rodin. In Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ Pisa, Italy , pages 194–207, 2012

    2012

  3. [11]

    A Discipline of Programming

    Edsger Wybe Dijkstra. A Discipline of Programming . Prentice-Hall, 1976

    1976

  4. [12]

    An Extensible SAT-solver

    Niklas E ´en and Niklas S ¨orensson. An Extensible SAT-solver. In Theory and Applications of Satisfiability Testing, 6th International Conference, SAT, Santa Margherita Ligure, Italy, , pages 502–518, 2003

    2003

  5. [13]

    Allen Emerson and Edmund M

    E. Allen Emerson and Edmund M. Clarke. Characterizing Correct- ness Properties of Parallel Programs Using Fixpoints. In Automata, Languages and Programming, 7th Colloquium, Noordweijkerhout, The Netherlands, pages 169–181, 1980

    1980

  6. [14]

    A taxonomy of trace-based security properties for ccs

    Riccardo Focardi and Roberto Gorrieri. A taxonomy of trace-based security properties for ccs. In Proceedings The Computer Security Foundations Workshop VII, pages 126–136. IEEE, 1994

    1994

  7. [15]

    Classification of security properties

    Riccardo Focardi and Roberto Gorrieri. Classification of security properties. In International School on Foundations of Security Analysis and Design, pages 331–396. Springer, 2000

    2000

  8. [16]

    Resolute: an assurance case language for architecture models

    Andrew Gacek, John Backes, Darren Cofer, Konrad Slind, and Mike Whalen. Resolute: an assurance case language for architecture models. ACM SIGAda Ada Letters , 34(3):19–28, 2014

    2014

  9. [17]

    Misuse and abuse cases: Getting past the positive

    Paco Hope, Gary McGraw, and Annie I Ant ´on. Misuse and abuse cases: Getting past the positive. IEEE Security & Privacy , 2(3):90–92, 2004

    2004

  10. [18]

    Iso/iec 27000: 2018 information technology—security tech- niques—information security management systems—overview and vo- cabulary, 2018

    MS ISO. Iso/iec 27000: 2018 information technology—security tech- niques—information security management systems—overview and vo- cabulary, 2018

    2018

  11. [19]

    Software Abstractions - Logic, Language, and Analysis

    Daniel Jackson. Software Abstractions - Logic, Language, and Analysis. MIT Press, 2006

    2006

  12. [20]

    Towards an improved understanding of human factors in cybersecurity

    Jongkil Jeong, Joanne Mihelcic, Gillian Oliver, and Carsten Rudolph. Towards an improved understanding of human factors in cybersecurity. In 2019 IEEE 5th International Conference on Collaboration and Internet Computing (CIC) , pages 338–345. IEEE, 2019

    2019

  13. [21]

    Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers

    Leslie Lamport. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley, 2002

    2002

  14. [22]

    Michael Leuschel and Michael J. Butler. Prob: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf., 10(2):185– 203, 2008

    2008

  15. [23]

    Information security management objectives and practices: a parsimonious frame- work

    Qingxiong Ma, Allen C Johnston, and J Michael Pearson. Information security management objectives and practices: a parsimonious frame- work. Information Management & Computer Security , 2008

    2008

  16. [24]

    Fundamentals of secure system modelling

    Raimundas Matulevi ˇcius. Fundamentals of secure system modelling . Springer, 2017

    2017

  17. [25]

    Asset-oriented threat modeling

    Nan Messe, Vanea Chiprianov, Nicolas Belloir, Jamal El-Hachem, R ´egis Fleurquin, and Salah Sadou. Asset-oriented threat modeling. In 2020 IEEE 19th International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom) , pages 491–501. IEEE, 2020

    2020

  18. [26]

    Using the cia and aaa models to explain cybersecurity activities

    Livinus Obiora Nweke. Using the cia and aaa models to explain cybersecurity activities. PM World Journal, 6(12):1–3, 2017

    2017

  19. [27]

    The Temporal Logic of Programs

    Amir Pnueli. The Temporal Logic of Programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, pages 46–57, 1977

    1977

  20. [28]

    A formal methods approach to security requirements specification and verification

    Quentin Rouland, Brahim Hamid, Jean-Paul Bodeveix, and Mamoun Filali. A formal methods approach to security requirements specification and verification. In 2019 24th International Conference on Engineering of Complex Computer Systems (ICECCS) , pages 236–241, 2019

    2019

  21. [29]

    Formalization of requirements for correct systems

    Imen Sayar and Jeanine Souqui `eres. Formalization of requirements for correct systems. In 2020 IEEE Workshop on Formal Requirements (FORMREQ), pages 28–34. IEEE, 2020

    2020

  22. [30]

    Security Patterns: Integrating security and systems engineering

    Markus Schumacher, Eduardo Fernandez-Buglioni, Duane Hybertson, Frank Buschmann, and Peter Sommerlad. Security Patterns: Integrating security and systems engineering . John Wiley & Sons, 2013

    2013

  23. [31]

    Reusable knowledge in security requirements engineering: a systematic mapping study

    Amina Souag, Ra ´ul Mazo, Camille Salinesi, and Isabelle Comyn- Wattiau. Reusable knowledge in security requirements engineering: a systematic mapping study. Requirements Engineering, 21(2):251–283, 2016

    2016

  24. [32]

    Applica- tion of validation obligations to security concerns

    Sebastian Stock, Atif Mashkoor, and Alexander Egyed. Applica- tion of validation obligations to security concerns. arXiv preprint arXiv:2207.03209, 2022

    2022 arXiv

  25. [33]

    Risk analysis in software design

    Denis Verdon and Gary McGraw. Risk analysis in software design. IEEE Security & Privacy , 2(4):79–84, 2004

    2004

  26. [34]

    From information security to cyber security

    Rossouw V on Solms and Johan Van Niekerk. From information security to cyber security. computers & security , 38:97–102, 2013

    2013

  27. [35]

    Your” what” is my” how”: Iteration and hierarchy in system design

    Michael W Whalen, Andrew Gacek, Darren Cofer, Anitha Murugesan, Mats PE Heimdahl, and Sanjai Rayadurgam. Your” what” is my” how”: Iteration and hierarchy in system design. IEEE software, 30(2):54–60, 2012

    2012

  28. [36]

    Beyond 2014: Formal methods for attack tree–based security modeling

    Wojciech Wideł, Maxime Audinot, Barbara Fila, and Sophie Pinchinat. Beyond 2014: Formal methods for attack tree–based security modeling. ACM Computing Surveys (CSUR) , 52(4):1–36, 2019

    2014

  29. [37]

    Program Development by Stepwise Refinement

    Niklaus Wirth. Program Development by Stepwise Refinement. Com- munications of ACM , 14(4):221–227, 1971

    1971

  30. [38]

    Sok: Social cyberse- curity

    Yuxi Wu, W Keith Edwards, and Sauvik Das. Sok: Social cyberse- curity. In IEEE Symposium on Security and Privacy (Oakland)(2022). https://sauvikdas. com/uploads/paper/pdf/36/file. pdf , 2022

    2022

  31. [39]

    Towards better utilizing static application security testing

    Jinqiu Yang, Lin Tan, John Peyton, and Kristofer A Duer. Towards better utilizing static application security testing. In 2019 IEEE/ACM 41st In- ternational Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP) , pages 51–60. IEEE, 2019

    2019

  32. [40]

    Threat modeling: from infancy to maturity

    Koen Yskout, Thomas Heyman, Dimitri Van Landuyt, Laurens Sion, Kim Wuyts, and Wouter Joosen. Threat modeling: from infancy to maturity. In 2020 IEEE/ACM 42nd International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER) , pages 9–

    2020

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.