Lean security formalization
Skill r-irbe/proof-skills/skills/lean-security-formalization
USE FOR: Data security, information security, access control, cryptographic properties, and privacy in Lean 4. Use when formalizing information flow policies, access control models, confidentiality/integrity/availability properties, data protection compliance (GDPR/LED), or trust model properties. DO NOT USE FOR: security policy design not in Lean (use @applied-data-information-security); AI safety formalisation (use @lean-ai-formalization); general knowledge formalisation (use @lean-knowledge-formalization). TRIGGERS: security formalization, information flow Lean, access control proof, cryptographic Lean, privacy proof.From its SKILL.md
npx -y skills add r-irbe/proof-skills --skill lean-security-formalizationAssembled 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.
SKILL.md
3.7 KB, 649 tokens by cl100k_base, as published. Nobody here has run it
Lean 4 Security & Privacy Formalization
Guide to formalizing security properties, access control, information flow, and privacy in Lean 4.
Routing
- USE FOR: Data security, information security, access control, cryptographic properties, and privacy in Lean 4. Use when formalizing information flow policies, access control models, confidentiality/integrity/availability properties, data protection compliance (GDPR/LED), or trust model properties.
- DO NOT USE FOR: security policy design not in Lean (use @applied-data-information-security); AI safety formalisation (use @lean-ai-formalization); general knowledge formalisation (use @lean-knowledge-formalization).
- TRIGGERS: security formalization, information flow Lean, access control proof, cryptographic Lean, privacy proof.
Workflow
- Identify the security property class: information flow, access control, cryptographic, or privacy.
- Pick the matching encoding from the body (non-interference, BLP-Lean, IND-CPA-Lean, k-anonymity-Lean).
- Produce the Lean statement + proof skeleton; verify Mathlib primitives at the pin.
- Hand off: to
@lean-proof-reviewfor review, to@lean-enforcementfor CI, to@applied-data-information-securityif the model is wrong.
Recovery & STOP
- STOP if the question is about policy design — delegate to
@applied-data-information-security. - STOP if Mathlib lacks the cryptographic primitive — escalate to
@lean-research. - STOP if the property has not been formally stated — delegate to
@lean-specification.
Handoffs
- Predecessors:
agent:gateway,skill:lean-research. - Successors:
skill:lean-proof-review,skill:lean-enforcement,skill:lean-zettelkasten.
Detailed reference
Full content for lean-security-formalization lives in
references/lean-security-formalization-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 |
| Part 4 | Privacy and Data Protection |
| Part 5 | Cryptographic Properties |
| Part 6 | Trust Models |
| Part 7 | Research Council Integration |
See also
../../references/lean-security-formalization-handbook.md— Full handbook (extracted from this skill)../lean-proof-review/SKILL.md— Successor../lean-enforcement/SKILL.md— Successor../lean-zettelkasten/SKILL.md— Successor
What ships with it
Read from the repository
Just SKILL.md. No reference files, no scripts.