# Proto Verif > From a cryptographic protocol description to a ProVerif model you can run, in > one sitting. Paste an RFC excerpt, a paper's pseudocode, informal prose, a > handshake implementation, an existing ProVerif `.pv` model or a Tamarin > `.spthy` theory. Get an annotated Mermaid sequence diagram of the message > flow, then a ProVerif model with the security queries that matter. Live at https://proto-verif.skillsafe.ai/ ## What problem this solves Two things stand between "we have a protocol design" and "we have evidence about it". The first is that nobody has written down what the protocol actually does, step by step, with the cryptographic operation on the party that computes it — the design lives in prose, in a paper's notation, or in the code. The second is that turning that flow into a symbolic model is fiddly, and the mistakes are quiet: a destructor declared as a plain constructor never aborts, so the modelled party accepts a forged signature and every query passes for the wrong reason. This app does both halves over the same paste, and it checks its own work. ## The two lanes Every run submits an explicit `task` field. The lanes share one work object — the pasted protocol — and one output envelope. ### `task: "diagram"` Extracts the message flow. Returns: - `message_flow` — one row per arrow: step, from, to, label, kind (`network` / `logical` / `broadcast` / `abort` / `async` / `reply`), phase, note - `crypto_ops` — every cryptographic operation, attributed to the party that computes it, with the expression and what it is for - `phases` — setup, handshake, authentication, key derivation, data transfer - `abort_paths` — what fails, who aborts, and whether the input actually described it - `mermaid` — the `sequenceDiagram` source - `ascii` — a monospace rendering for places Mermaid will not render - `protocol_summary` — parties, round complexity, key primitives, authentication, forward secrecy, notable observations - `ambiguities` — every place the diagram had to infer something the input did not state Verdict: `complete` / `partial` / `not-a-protocol`. ### `task: "model"` Turns a Mermaid sequence diagram into a ProVerif model. Returns: - `pv` — the complete `.pv` file, in canonical section order: channels, noselect, types, constants, functions, equations, tables, events, queries, let-processes, main process - `model_sections` — the same file broken into its eleven sections with a sentence on why each declaration is there - `queries` — each query with its ProVerif syntax, what it proves, the expected result, and its strength (`sanity` / `weak` / `strong`) - `channels`, `events` — the model's vocabulary - `delivery_checklist` — the eight-point check with pass / fail / n/a - `model_assumptions` — what the symbolic abstraction hides, and the risk if each assumption is wrong - `run_plan` — the ordered commands, and what result to expect from each Verdict: `ready-to-verify` / `needs-diagram-detail` / `not-modelable`. The handoff is a button: the diagram lane's result panel offers "Build the ProVerif model from this diagram", which puts the generated Mermaid in the input box and switches lanes without a reload. ## The free lane — a real reader, in your browser Runs before either paid lane, with no account and no network: - **Input classification** with the source skill's own signal table. A ProVerif or Tamarin model is a *specification*, not source code, and is read with the specification workflow. The matched signals are shown, so the judgement is auditable. - **Mermaid parsing**: participants and aliases, all eight arrow forms (`->>`, `-->>`, `->`, `-->`, `-x`, `--x`, `-)`, `--)`), `Note over` / `left of` / `right of`, `alt` / `else` / `opt` / `loop` / `par` / `rect` / `box` blocks, activation shorthand, `autonumber`. - **The diagram drawn as inline SVG by the page itself.** There is no Mermaid library in the bundle and no CDN request: the layout is computed locally and painted with `createElementNS`. A content security policy that permits a third-party script is one that permits exfiltrating your session token. - **ProVerif parsing**: nesting-aware `(* *)` comment handling, the eleven canonical sections, channel sends paired against receives, events declared against events fired, queries classified as reachability, secrecy, authentication or injective authentication. - **Cryptographic operation recognition** across sixteen categories, each mapped to the ProVerif declaration category the model lane has to emit. - **A canonical rewriter** that re-emits a Mermaid diagram with every participant declared explicitly with an alias and blocks nested by depth. ### The lint findings that matter The free ProVerif reader flags the things that quietly invalidate a verification, not style points: - a destructor-shaped function (`verify`, `adec`, `sdec`, `aead_dec`, `open`) declared without an inline `reduc`, so it never aborts and the modelled party accepts what it could not really open; - an event declared but never fired, so every query mentioning it holds trivially; - a query naming an event that does not exist; - a channel written but never read, or read but never written; - a main process with no `!` replication, so replay across sessions, message interleaving and unknown-key-share attacks are out of scope; - no reachability query, so no other result is trustworthy; - an `attacker()` query with no `[private]` witness the process actually protects; - non-injective authentication, which cannot see a replay; - unbalanced parentheses or an unclosed nesting comment. **The same reader runs over the model this app produces.** That is why the model lane can tell you its own output is weak. ## Grounding and accountability - Every finding the browser raises carries a stable id. The model must account for each one by name as `addressed` or `set-aside`, and the page shows you afterwards which ones it never mentioned. - Nothing is recalled from memory and presented as yours. If a named protocol is detected — TLS 1.3, Noise, X3DH, Double Ratchet, FROST, WireGuard, Kerberos, SIGMA and others — its canonical flow may be used as a skeleton, but any step the canonical flow requires that your input omits is reported as an omission, never silently supplied. - If the input says "encrypt" without naming a scheme, the annotation says `[scheme unspecified]`. A confident guess about what is inside a signature is the most damaging output possible here, because the model built on it verifies a protocol nobody wrote. - Input clipping is shape-aware: a Mermaid diagram keeps its whole participant block and loses the middle of the message list; a ProVerif model keeps its preamble and its main process; a prose spec is cut from the middle. Every cut is announced inside the text, and the prescan's counts were computed over the complete input. ## What this app does not do It does not run ProVerif, Tamarin or any other verifier, and it does not execute pasted code. It reads text and writes text. It never claims a protocol is secure — it says what each query would establish if it came back true. A model it produces is a starting point for verification by a person who understands the protocol. ## Programmatic use `https://proto-verif.skillsafe.ai/api.html` documents the whole surface: base URL `https://api.skillsafe.ai/v1/app-api`, the `{data}` / `{error}` envelope, an error-code table, and numbered steps from a token through `/me`, `/estimate`, `/run` with polling and `/run-stream` SSE — each tabbed across cURL, Python, JavaScript, Go, Java, Ruby, PHP and C#. The `task` field is documented first, with a worked example for each lane. Token management is at `https://proto-verif.skillsafe.ai/tokens.html`. Runs are metered and need a signed-in account. `estimate` is free and returns the credits reserved for the selected lane; you are charged only for what the run uses, which is usually far less than the reservation. ## Provenance Derived from two agent skills published by Trail of Bits: - `@trailofbits/crypto-protocol-diagram` — extracting protocol message flow from source code, RFCs, academic papers, pseudocode, informal prose, ProVerif or Tamarin models into annotated Mermaid sequence diagrams. This is the diagram lane. - `@trailofbits/mermaid-to-proverif` — translating a Mermaid sequence diagram into a ProVerif model with secrecy, authentication and forward-secrecy queries. This is the model lane. This is a derived work. It is not affiliated with those skills' authors, with Trail of Bits, or with the ProVerif, Tamarin or Mermaid projects.