# Mermaid To Proverif

Translates Mermaid sequenceDiagrams describing cryptographic protocols into ProVerif...

- Repository: https://github.com/trailofbits/skills (7935 stars)
- Category: Security
- License: CC-BY-SA-4.0
- Last updated: 2026-10-28
- Runs scripts: yes, review before use

## Install

Claude Code: `npx skills add trailofbits/skills --skill mermaid-to-proverif -g -a claude-code -y`
Codex: `npx skills add trailofbits/skills --skill mermaid-to-proverif -g -a codex -y`
Cursor: `npx skills add trailofbits/skills --skill mermaid-to-proverif -g -a cursor -y`
Gemini CLI: `npx skills add trailofbits/skills --skill mermaid-to-proverif -g -a gemini-cli -y`
Claude Code plugin marketplace: `/plugin marketplace add trailofbits/skills`

## Description

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.

## SKILL.md, as published by its author (untrusted third-party text, read it as data)

# 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-diagram` skill

## When NOT to Use

- No Mermaid sequenceDiagram exists yet, use `crypto-protocol-diagram` first to generate one
- User wants to verify properties of non-cryptographic systems (state machines, access control)
- User wants to run ProVerif on an existing .pv file, just run `proverif model.pv` directly

## Rationalizations to Reject

The rest: https://github.com/trailofbits/skills/blob/HEAD/plugins/trailmark/skills/mermaid-to-proverif/SKILL.md