Proto Verif

Paste the material behind one cryptographic protocol - an RFC excerpt, a paper's pseudocode, informal prose, a handshake implementation, an existing ProVerif .pv model or a Tamarin .spthy theory - and work it into two artifacts in one sitting. The diagram lane extracts the message flow into an annotated Mermaid sequenceDiagram with every cryptographic operation on the party that computes it, phases grouped, abort paths shown as alt blocks, and every place the input is silent flagged as an inference rather than a fact. The model lane turns that diagram into a ProVerif model in canonical section order: reachability queries first, a private witness for secrecy, injective correspondence for authentication, a forward-secrecy test whenever ephemeral keys appear, and an honest list of what the symbolic abstraction hides. A free in-browser reader runs before either lane - it classifies the input, tokenises a Mermaid diagram and draws it as SVG with no third-party library, and parses a .pv model to catch destructors without an inline reduc, events declared but never fired, one-way channels and missing reachability queries. The same reader then re-lints the model this app produces. It runs no verifier and executes no pasted code. Derived from two Trail of Bits agent skills: @trailofbits/crypto-protocol-diagram (the diagram lane) and @trailofbits/mermaid-to-proverif (the model lane).

Every public app is built from a security-scanned skill and must pass a clean scan — skill and frontend — before it can be listed. Have a skill of your own? Turn it into an app — or read the step-by-step walkthrough.