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.

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