Applied data information security
Skill r-irbe/proof-skills/skills/applied-data-information-security
APM-installable agent skills for Lean 4 and Mathlib4 — proof tactics, math domains, review and research workflows, generic tooling.
npx -y skills add r-irbe/proof-skills --skill applied-data-information-securityAssembled from the repository path, not quoted from the project. Check it against their README if it does not work.
One thing to look at
- 2 stars2 stars. Stars are a popularity signal and not a quality one, but at this level it is likely that nobody has read this closely except its author, and you would be relying on your own review.
What its author says it does
Copied from the file, not written here
USE FOR: Data security and information security formalization — CIA triad, access control models (BLP, RBAC, ABAC), information flow, cryptographic primitives, privacy (differential privacy, k-anonymity), threat modeling, and their formal verification in Lean 4. Use for security properties of provenance chains, trust composition, and multi-agent systems. DO NOT USE FOR: Lean formalisation of these policies (use @lean-security-formalization); engineering disciplines more broadly (use @applied-engineering-disciplines); legal-policy reasoning (use @applied-legal-reasoning). TRIGGERS: CIA triad, access control, BLP, RBAC, ABAC, information flow, cryptographic primitive, data security.
SKILL.md
4.2 KB, as published. Nobody here has run it
Data & Information Security
Formal foundations of security properties, access control, information flow, privacy, and their verification in formal frameworks.
Routing
- USE FOR: Data security and information security formalization — CIA triad, access control models (BLP, RBAC, ABAC), information flow, cryptographic primitives, privacy (differential privacy, k-anonymity), threat modeling, and their formal verification in Lean 4. Use for security properties of provenance chains, trust composition, and multi-agent systems.
- DO NOT USE FOR: Lean formalisation of these policies (use @lean-security-formalization); engineering disciplines more broadly (use @applied-engineering-disciplines); legal-policy reasoning (use @applied-legal-reasoning).
- TRIGGERS: CIA triad, access control, BLP, RBAC, ABAC, information flow, cryptographic primitive, data security.
Workflow
- Classify the security goal in the CIA triad and pick the access-control model (BLP / RBAC / ABAC) or information-flow model (non-interference) from the body.
- Apply the chosen model to the concrete asset or flow; surface assumptions and gaps.
- Produce the security argument or policy ready for formal encoding.
- Hand off: to
@lean-security-formalizationfor the Lean encoding, to@applied-engineering-disciplinesif reliability/safety overlap, to@lean-zettelkasten.
Recovery & STOP
- STOP if the question demands a Lean proof — delegate to
@lean-security-formalization. - STOP if the question is about cryptographic-protocol design — escalate to
@research-councilif the body lacks the protocol. - STOP if the question is about legal/regulatory compliance — delegate to
@applied-legal-reasoning.
Handoffs
- Predecessors:
agent:gateway,skill:lean-research. - Successors:
skill:lean-security-formalization,skill:applied-engineering-disciplines,skill:lean-knowledge-formalization.
Detailed reference
Full content for applied-data-information-security lives in
references/applied-data-information-security-handbook.md.
Load that file when the skill is convened; the SKILL.md only carries
the dispatch contract and the parts index.
| Section | Topic |
|---|---|
| Part 1 | Security Properties |
| Part 2 | Access Control Models |
| Part 3 | Information Flow Control |
| Part 4 | Cryptographic Foundations |
| Part 5 | Privacy Formalization |
| Part 6 | Threat Modeling |
| Part 7 | Security Verification in Lean |
| Part 8 | Cross-References |
See also
../../references/applied-data-information-security-handbook.md— Full handbook (extracted from this skill)../lean-security-formalization/SKILL.md— Successor../applied-engineering-disciplines/SKILL.md— Successor../lean-knowledge-formalization/SKILL.md— Successor