Mermaid to ProVerif
技能 已验证 活跃Translates Mermaid sequenceDiagrams describing cryptographic protocols into ProVerif formal verification models (.pv files). Use when generating a ProVerif model, formally verifying a protocol, converting a Mermaid diagram to ProVerif, verifying protocol security properties (secrecy, authentication, forward secrecy), checking for replay attacks, or producing a .pv file from a sequence diagram.
To automate the creation of formal verification models for cryptographic protocols from visual Mermaid diagrams, enabling rigorous security analysis and property verification.
功能
- Mermaid sequenceDiagram to ProVerif (.pv) model conversion
- Formal verification of cryptographic protocols
- Support for secrecy, authentication, and forward secrecy properties
- Detailed guidance on ProVerif syntax and modeling patterns
- Generation of ProVerif files from protocol diagrams
使用场景
- Generating ProVerif models from Mermaid sequence diagrams
- Formally verifying cryptographic protocol security properties
- Checking for replay attacks and ensuring authentication
- Producing .pv files from protocol specifications
非目标
- Verifying protocols not described as Mermaid sequence diagrams
- Generating ProVerif models for non-cryptographic systems
- Running ProVerif on existing .pv files (users should do this directly)
工作流
- Parse participants and channels from Mermaid diagram
- Inventory cryptographic operations and map to ProVerif functions
- Declare ProVerif types, constants, and functions
- Formulate security queries (secrecy, authentication, forward secrecy)
- Write ProVerif participant processes based on diagram steps
- Write the main ProVerif process with replication and key publication
- Verify the generated model and deliver the .pv file
实践
- Formal Verification
- Protocol Security
- Model Generation
先决条件
- ProVerif installed and available in the environment
- Mermaid sequenceDiagram describing a cryptographic protocol
安装
请先添加 Marketplace
/plugin marketplace add trailofbits/skills/plugin install trailmark@trailofbits质量评分
已验证类似扩展
Crypto Protocol Diagram
97Extracts protocol message flow from source code, RFCs, academic papers, pseudocode, informal prose, ProVerif (.pv), or Tamarin (.spthy) models and generates Mermaid sequenceDiagrams with cryptographic annotations. Use when diagramming a crypto protocol, visualizing a handshake or key exchange flow, extracting message flow from a spec or RFC, diagramming a ProVerif or Tamarin model, or drawing sequence diagrams for TLS, Noise, Signal, X3DH, Double Ratchet, FROST, DH, or ECDH protocols.
Markdown and Mermaid Writing
100Comprehensive markdown and Mermaid diagram writing skill. Use when creating any scientific document, report, analysis, or visualization. Establishes text-based diagrams as the default documentation standard with full style guides (markdown + mermaid), 24 diagram type references, and 9 document templates.
Codacy Audit
100Codacy Cloud workflow for this repository -- run Codacy's analyzers locally before `git push` (mirrors what Codacy CI runs), and fetch/cluster Codacy issues for any PR via the v3 API. Use when the user mentions Codacy, "codacy analysis", `codacy-analysis-cli`, "codacy issues on PR", "fix codacy CI", "codacy markdownlint findings", or any Codacy gate failing on a netdata-org PR. Ships scripts analyze-local.sh (docker/binary runner for codacy-analysis-cli) and pr-issues.sh (paginated v3 issue fetch + group-by tool/pattern/severity/file). Token-safe -- CODACY_TOKEN never reaches assistant-visible stdout. Read-only by design in the current SOW; write actions (mark FP, mark fixed) are deferred.
Azure Key Vault Keys SDK for TypeScript
99Manage cryptographic keys using Azure Key Vault Keys SDK for JavaScript (@azure/keyvault-keys). Use when creating, encrypting/decrypting, signing, or rotating keys.
Generate Workflow Diagram
99Generate themed Mermaid flowchart diagrams from putior workflow data. Covers theme selection (9 themes including 4 colorblind-safe), output modes (console, file, clipboard, raw), interactive features (clickable nodes, source info), and embedding in README, Quarto, and R Markdown. Use after annotating source files and ready to produce a visual diagram, when regenerating a diagram after workflow changes, or when switching themes or output formats for different audiences.
Mermaid Diagrams
99Teaches PMs to create syntactically valid mermaid diagrams by selecting the right diagram type for their communication need, following syntax validity rules, and validating before shipping. Covers all 15 mermaid diagram types with PM-relevant examples and a dual-lens navigation system.