mermaid-to-proverif

Translation of Mermaid sequenceDiagrams that describe cryptographic protocols into ProVerif formal verification models, producing a `.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 such as Sign, Verify, DH, HKDF, Enc, and Dec, together with message arrows. It is used to formally verify a protocol or prove secrecy, authentication, or forward secrecy properties, and it is not for cases where no diagram exists yet, for non-cryptographic systems such as state machines or access control, or for simply running ProVerif on an existing model.

The workflow proceeds through eight steps. It parses participants and channels, where each participant or actor becomes a ProVerif process and message arrows become communication steps; public channels are used for network messages before a secure channel exists, while private channels are reserved for internal state threading within a single party, defaulting to one shared public channel `c`. It then inventories the cryptographic operations from Note annotations and message labels, mapping each Mermaid annotation to a ProVerif declaration category. Types, constants, functions, and equations form the cryptographic preamble, with destructors using inline `reduc` so a process aborts on verification or decryption failure, and equations declared only on constructors; only operations the diagram actually uses are declared.

The remaining steps identify and declare events that mark security-relevant moments (begin events fired before sending an identity-committing message and end events fired after verifying the peer), formulate security queries, write the participant processes, write the main process, and finally verify and deliver. The skill emphasizes adding reachability queries first as a sanity check, since a model that merely compiles can still have dead receives, type mismatches, or impossible guards that make security queries vacuously true. It also calls for cleaning up unused declarations, adding a ForwardSecrecyTest process whenever the diagram shows ephemeral keys, and studying the included simple-handshake example before tackling unfamiliar protocols.