mermaid-to-proveriflisted

# 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 | Rationalization | Why It's Wrong | Required Action | |-----------------|----------------|-----------------| | "Reachability queries are just busywork" | If events aren't reachable, all other query results are meaningless | Always add reachability queries first as a sanity check | | "Public channels are fine for all messages" | Private channels for internal state prevent false attacks |