mermaid-to-proverif
Mermaid to ProVerif
Reads a Mermaid sequenceDiagram describing a cryptographic protocol and
produces a ProVerif model (.pv file) that can be passed directly to the
ProVerif verifier.
Tools used: Read, Write, Grep, Glob.
The typical input is the output of the crypto-protocol-diagram skill — a
Mermaid sequenceDiagram annotated with cryptographic operations (Sign,
Verify, DH, HKDF, Enc, Dec, etc.) and message arrows.
When to Use
- User asks to formally verify a cryptographic protocol described as a Mermaid sequenceDiagram
- User wants to generate a ProVerif model (.pv file) from a protocol diagram
- User wants to prove secrecy, authentication, or forward secrecy properties
- Input is the output of the
crypto-protocol-diagramskill
More from trailofbits/skills
ask-questions-if-underspecified
Clarify requirements before implementing. Use when serious doubts arise.
4.2Ksemgrep
>-
3.8Kmodern-python
Configures Python projects with modern tooling (uv, ruff, ty). Use when creating projects, writing standalone scripts, or migrating from pip/Poetry/mypy/black.
3.8Kcodeql
>-
3.6Kinsecure-defaults
Detects fail-open insecure defaults (hardcoded secrets, weak auth, permissive security) that allow apps to run insecurely in production. Use when auditing security, reviewing config management, or analyzing environment variable handling.
3.5Ksecure-workflow-guide
Guides through Trail of Bits' 5-step secure development workflow. Runs Slither scans, checks special features (upgradeability/ERC conformance/token integration), generates visual security diagrams, helps document security properties for fuzzing/verification, and reviews manual security areas.
3.4K