domains / families / security / mermaid-to-proverif

mermaid-to-proverif

separate

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.

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

Skill page

Source