Your protocol, drawn from what the text actually says

Paste the material behind one protocol — an RFC excerpt, a paper's pseudocode, plain prose, a handshake implementation, or an existing .pv / .spthy model. A reader in this page classifies it, profiles the parties and the cryptographic operations, and draws any Mermaid diagram it finds as SVG. Then the model extracts the message flow, annotates every cryptographic step on the party that computes it, and tells you where the input is silent.

Both examples ship with a saved model run for both lanes, so you can see all four complete outputs without signing in and without spending a credit.

Your protocol nothing pasted yet

Drag a file in, or Everything is read in your browser. Nothing uploads until you run.

How to read this input

This only tells the model which extraction workflow to use. A formal model is read as a specification, not as source code.

Context — optional, but it changes the answer

Paste a protocol to price the run.

verdict

protocol

read as

parties

messages

ambiguities

Parties

A party marked inferred is one the input never names. The diagram gives it a descriptive name and the model gives it a process, but a human should confirm it exists.

Id	Name	Trusted with	From input	Note

The diagram — drawn here from the model's own Mermaid

Mermaid source

Message flow

#	From	To	Message	Kind	Phase	Note

Cryptographic operations

Each operation sits on the party that computes it. An expression reading [scheme unspecified] is a place the input never said which algorithm.

Party	Operation	Expression	After step	Purpose

Phases

Abort paths

A path marked not in the input is one the protocol needs but the pasted text never describes. That silence is where a missing check hides.

Trigger	Party	Behaviour	In diagram	From input

Protocol summary

Parties
Round complexity
Key primitives
Authentication
Forward secrecy
Notable

ASCII rendering

For a code review comment, a commit message or a terminal — anywhere Mermaid will not render.

Ambiguities

Every place the diagram had to infer something the input did not state. Each one is a question for the protocol's author, not a finding against them.

The ProVerif model

Save it as model.pv and run proverif model.pv. Nothing here is executed by this page.

The page re-lints the model it just wrote

The same in-browser ProVerif reader that checked your paste runs over the generated model. A model that compiles can still have an event no process fires or a missing reachability query, and either makes the results meaningless.

Queries

Read the expected column before you run anything. A query whose expected result is false is there to demonstrate a weakness, not to pass.

#	Property	Strength	Proves	Expected

Sections

The canonical order ProVerif reads top to bottom: channels, noselect, types, constants, functions, equations, tables, events, queries, let-processes, main process.

Channels and events

Channel	Visibility	Carries

Event	Parameters	Fired by	When

Delivery checklist

Check	Status	Evidence

What this model does not capture

A symbolic model abstracts the cryptography. These are the abstractions this one makes, and what each would hide if it is wrong.

Assumption	Why	Risk if wrong

Run plan

Prescan reconciliation

Every flag this page raised, and what the model did with it. A flag the model never mentioned is called out here rather than quietly dropped.

Summary

Raw model reply

The reply did not parse as the structured result, so it is shown as it arrived.

What this does, and what it does not

The prescan is a real reader, not a word count. It classifies the paste with the same signal table the source skill uses to choose its workflow — RFC keywords and section numbers, process and reduc forall for ProVerif, rule and --[ ]-> for Tamarin — and tells you which signals it matched. If the paste is a Mermaid sequenceDiagram it is tokenised into participants, all eight arrow forms, notes and grouping blocks, then drawn in this page as SVG. There is no Mermaid library in this bundle and no request to a CDN: the layout is computed here and painted with createElementNS, because a content security policy that allows a third-party script is a policy that allows exfiltrating your session.

If the paste is a ProVerif model, the reader walks its eleven canonical sections with nesting-aware comment handling and checks the things that quietly invalidate a verification: a destructor such as verify or adec declared without an inline reduc, so it never aborts and the party accepts a forged signature; 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; a main process with no ! replication, so replay across sessions is out of scope. The same reader then runs over the model this app produces, which is why the model lane can tell you its own output is weak.

It reads and it writes. It does not run ProVerif or Tamarin, it does not execute your code, and it never claims a protocol is secure — it says what each query would establish if it came back true. Everything the prescan finds is handed to the model as facts with stable ids that must each be reconciled, and the reconciliation is checked here afterwards.

Nothing to hand? Load the , a prose specification with an unstated message ordering, an unnamed encryption scheme and no described abort path, or the , a two-party authenticated key exchange with ephemeral DH, signatures and a phase structure. Both replay a saved run for both lanes, for free.