Crypto Protocol Diagram
Produces a Mermaid sequenceDiagram (written to file) and an ASCII sequence
diagram (printed inline) from either:
- Source code implementing a cryptographic protocol, or
- A specification — RFC, academic paper, pseudocode, informal prose,
ProVerif (
.pv), or Tamarin (.spthy) model.
Tools used: Read, Write, Grep, Glob, Bash, WebFetch (for URL specs).
Unlike the diagramming-code skill (which visualizes code structure), this skill
extracts protocol semantics: who sends what to whom, what cryptographic
transformations occur at each step, and what protocol phases exist.
For call graphs, class hierarchies, or module dependency maps, use the
diagramming-code skill instead.
When to Use
- User asks to diagram, visualize, or extract a cryptographic protocol
- Input is source code implementing a handshake, key exchange, or multi-party protocol
- Input is an RFC, academic paper, pseudocode, or formal model (ProVerif/Tamarin)
- User names a specific protocol (TLS, Noise, Signal, X3DH, FROST)
When NOT to Use
- User wants a call graph, class hierarchy, or module dependency map — use
diagramming-code
- User wants to formally verify a protocol — use
mermaid-to-proverif (after generating the diagram)
- Input has no cryptographic protocol semantics (no parties, no message exchange)
Rationalizations to Reject
| Rationalization |
Why It's Wrong |
Required Action |
| "The protocol is simple, I can diagram from memory" |
Memory-based diagrams miss steps and invert arrows |
Read the source or spec systematically |
| "I'll skip the spec path since code exists" |
Code may diverge from the spec — both paths catch different bugs |
When both exist, run spec workflow first, then annotate code divergences |
| "Crypto annotations are optional decoration" |
Without crypto annotations, the diagram is just a message flow — useless for security review |
Annotate every cryptographic operation |
| "The abort path is obvious, no need for alt blocks" |
Implicit abort handling hides missing error checks |
Show every abort/error path with alt blocks |
| "I don't need to check the examples first" |
The examples define the expected output quality bar |
Study the relevant example before working on unfamiliar input |
| "ProVerif/Tamarin models are code, not specs" |
Formal models are specifications — they describe intended behavior, not implementation |
Use the spec workflow (S1–S5) for .pv and .spthy files |
Workflow
Protocol Diagram Progress:
- [ ] Step 0: Determine input type (code / spec / both)
- [ ] Step 1 (code) or S1–S5 (spec): Extract protocol structure
- [ ] Step 6: Generate sequenceDiagram
- [ ] Step 7: Verify and deliver
Step 0: Determine Input Type
Before doing anything else, classify the input:
| Signal |
Input type |
Source file extensions (.py, .rs, .go, .ts, .js, .cpp, .c) |
Code |
| Function/class definitions, import statements |
Code |
RFC-style section headers (§, Section X.Y, MUST/SHALL keywords) |
Spec |
Algorithm/Protocol/Figure labels, mathematical notation |
Spec |
ProVerif file (.pv) with process, let, in/out |
Spec |
Tamarin file (.spthy) with rule, --[...]-> |
Spec |
| Plain prose or numbered steps describing a protocol |
Spec |
| Both source files and a spec document |
Both (annotate divergences with ⚠️) |
- Code only → skip to Step 1 below
- Spec only → skip to Spec Workflow (S1–S5) below
- Both → run Spec Workflow first, then use the code-reading steps to verify
the implementation against the spec diagram and annotate any divergences with
⚠️
- Ambiguous → ask the user: "Is this a source code file, a specification
document, or both?"
Step 1: Locate Protocol Entry Points
Grep for function names, type names, and comments that reveal the protocol:
# Find handshake, session, round, phase entry points
rg -l "handshake|session_init|round[_0-9]|setup|keygen|send_msg|recv_msg" {targetDir}
# Find crypto primitives in use
rg "sign|verify|encrypt|decrypt|dh|ecdh|kdf|hkdf|hmac|hash|commit|reveal|share" \
{targetDir} --type-add 'src:*.{py,rs,go,ts,js,cpp,c}' -t src -l
Start reading from the highest-level orchestration function — the one that calls
into handshake phases or the main protocol loop.
Step 2: Identify Parties and Roles
Extract participant names from:
- Struct/class names:
Client, Server, Initiator, Responder, Prover,
Verifier, Dealer, Party, Coordinator
- Function parameter names that carry state for a role
- Comments declaring the protocol role
- Test fixtures that set up two-party or N-party scenarios
Map these to Mermaid participant declarations. Use short, readable aliases:
participant I as Initiator
participant R as Responder
Step 3: Trace Message Flow
Follow state transitions and network sends/receives. Look for patterns like:
| Pattern |
Meaning |
send(msg) / recv() |
Direct message exchange |
serialize + transmit |
Structured message sent |
| Return value passed to other party's function |
Logical message (in-process) |
round1_output → round2_input |
Round-based MPC step |
Struct fields named ephemeral_key, ciphertext, mac, tag |
Message contents |
For in-process protocol implementations (where both parties run in the same
process), treat function call boundaries as logical message sends when they
represent what would be a network boundary in deployment.
Step 4: Annotate Cryptographic Operations
At each protocol step, identify and label:
| Operation |
Diagram annotation |
| Key generation |
Note over A: keygen(params) → pk, sk |
| DH / ECDH |
Note over A,B: DH(sk_A, pk_B) |
| KDF / HKDF |
Note over A: HKDF(ikm, salt, info) |
| Signing |
Note over A: Sign(sk, msg) → σ |
| Verification |
Note over B: Verify(pk, msg, σ) |
| Encryption |
Note over A: Enc(key, plaintext) → ct |
| Decryption |
Note over B: Dec(key, ct) → plaintext |
| Commitment |
Note over A: Commit(value, rand) → C |
| Hash |
Note over A: H(data) → digest |
| Secret sharing |
Note over D: Share(secret, t, n) → {s_i} |
| Threshold combine |
Note over C: Combine({s_i}) → secret |
Keep annotations concise — use mathematical shorthand, not code.
Step 5: Identify Protocol Phases
Group message steps into named phases using rect or Note blocks:
Common phases to detect:
- Setup / Key Generation: party key creation, trusted setup, parameter gen
- Handshake / Init: ephemeral key exchange, nonce exchange, version negotiation
- Authentication: identity proof, certificate exchange, signature verification
- Key Derivation: session key derivation from shared secrets
- Data Transfer / Main Protocol: encrypted application data exchange
- Finalization / Teardown: session close, MAC verification, abort handling
Detect abort/error paths and show them with alt blocks.
Spec Workflow (S1–S5)
Use this path when the input is a specification document rather than source code.
After completing S1–S5, continue with Step 6 (Generate sequenceDiagram) and
Step 7 (Verify and deliver) from the code workflow above.
Step S1: Ingest the Spec
Obtain the full spec text:
- File path provided → read with the Read tool
- URL provided → fetch with WebFetch
- Pasted inline → work directly from conversation context
Then identify the spec format and read
references/spec-parsing-patterns.md
for format-specific extraction guidance:
| Format |
Signals |
| RFC |
RFC XXXX, MUST/SHALL/SHOULD, ABNF grammars, section-numbered prose |
| Academic paper / pseudocode |
Algorithm X, Protocol X, Figure X, numbered steps, ←/→ in math mode |
| Informal prose |
Numbered lists, "A sends B ...", plain English descriptions |
ProVerif (.pv) |
process, let, in(ch, x), out(ch, msg), ! (replication) |
Tamarin (.spthy) |
rule, --[ ]->, Fr(~x), !Pk(A, pk), In(m), Out(m) |
If the spec references a known named protocol (TLS, Noise, Signal, X3DH, Double
Ratchet, FROST), also read
references/protocol-patterns.md to use its
canonical flow as a skeleton and fill in spec-specific details.
Step S2: Extract Parties and Roles
Identify all protocol participants. Look for:
- Named roles in prose or pseudocode:
Alice, Bob, Client, Server,
Initiator, Responder, Prover, Verifier, Dealer, Party_i,
Coordinator, Signer
- Section headers: "Parties", "Roles", "Participants", "Setup", "Notation"
- ProVerif: process names at top level (
let ClientProc(...), let ServerProc(...))
- Tamarin: rule names and fact arguments (e.g.
!Pk($A, pk) — $A is a party)
Map each role to a Mermaid participant declaration. Use short IDs with
descriptive aliases (see naming conventions in
references/mermaid-sequence-syntax.md).
Step S3: Extract Message Flow
Trace what each party sends to whom and in what order. Extraction patterns by format:
RFC / informal prose:
- Arrow notation:
A → B: msg, A -> B
- Sentence patterns: "A sends B ...", "B responds with ...", "A transmits ...",
"upon receiving X, B sends Y"
- Numbered steps: extract in order, inferring sender/receiver from context
Pseudocode:
- Function signatures with explicit
sender/receiver parameters
send(party, msg) / receive(party) calls
- Return values passed as inputs to the other party's function in the next step
ProVerif (.pv):
out(ch, msg) — send on channel ch
in(ch, x) — receive on channel ch, bind to x
- Match
out/in pairs on the same channel to identify message flows
! (replication) signals a role that handles multiple sessions
Tamarin (.spthy):
In(m) premise — receive message m
Out(m) conclusion — send message m
- Rule name and ordering of rules reveal protocol rounds
Fr(~x) — fresh random value generated by a party
--[ Label ]-> facts — security annotations, not messages
Preserve the ordering and round structure. Group concurrent sends (broadcast)
using par blocks in the final diagram.
Step S4: Extract Cryptographic Operations
For each protocol step, identify the cryptographic operations performed and which
party performs them:
| Spec notation |
Operation |
Diagram annotation |
keygen(), Gen(1^λ) |
Key generation |
Note over A: keygen() → pk, sk |
DH(a, B), g^ab |
DH / ECDH |
Note over A,B: DH(sk_A, pk_B) |
KDF(ikm), HKDF(...) |
Key derivation |
Note over A: HKDF(ikm, salt, info) → k |
Sign(sk, m), σ ← Sign |
Signing |
Note over A: Sign(sk, msg) → σ |
Verify(pk, m, σ) |
Verification |
Note over B: Verify(pk, msg, σ) |
Enc(k, m), {m}_k |
Encryption |
Note over A: Enc(k, plaintext) → ct |
Dec(k, c) |
Decryption |
Note over B: Dec(k, ct) → plaintext |
H(m), hash(m) |
Hash |
Note over A: H(data) → digest |
Commit(v, r), com |
Commitment |
Note over A: Commit(value, rand) → C |
ProVerif senc(m, k) |
Symmetric encryption |
Note over A: Enc(k, m) → ct |
ProVerif pk(sk) |
Public key derivation |
Note over A: pk = pk(sk) |
ProVerif sign(m, sk) |
Signing |
Note over A: Sign(sk, m) → σ |
Identify security conditions and abort paths:
- Prose: "if verification fails, abort", "only if ...", "reject if ..."
- Pseudocode:
assert, require, if ... abort
- ProVerif:
if m = expected then ... else 0
- Tamarin: contradicting facts or restriction lemmas
These become alt blocks in the final diagram.
Step S5: Flag Spec Ambiguities
Before moving to Step 6, check for gaps:
- Unclear message ordering: infer from round structure or section order;
annotate with
⚠️ ordering inferred from spec structure
- Implied parties: if a party's role is implied but unnamed, give it a
descriptive name and note the inference
- Missing steps: if the spec omits a step that the canonical pattern for
this protocol requires, annotate:
⚠️ spec omits [step] — canonical protocol requires it
- Underspecified crypto: if the spec says "encrypt" without specifying
the scheme, annotate:
⚠️ encryption scheme not specified
- ProVerif/Tamarin: private channels (
c declared with new c or as a
private free name) represent out-of-band channels — note them
Step 6: Generate sequenceDiagram
Produce Mermaid syntax following the rules in
references/mermaid-sequence-syntax.md.
Completeness over brevity. Show every distinct message type. Omit repeated
loop iterations (use loop blocks instead), but never omit a distinct protocol
step.
Correctness over aesthetics. The diagram must match what the code actually
does. If the code diverges from a known spec, annotate the divergence:
Note over A,B: ⚠️ spec requires MAC here — implementation omits it
Step 7: Verify and Deliver
Before delivering:
Write the diagram to a file. Choose a filename derived from the protocol
name, e.g. noise-xx-handshake.md or x3dh-key-agreement.md. Write a
Markdown file with this structure:
# <Protocol Name> Sequence Diagram
\`\`\`mermaid
sequenceDiagram
...
\`\`\`
## Protocol Summary
- **Parties:** ...
- **Round complexity:** ...
- **Key primitives:** ...
- **Authentication:** ...
- **Forward secrecy:** ...
- **Notable:** [spec deviations or security observations, or "none"]
After writing the file, print an ASCII sequence diagram inline in the
response, followed by the Protocol Summary. State the output filename so the
user knows where to find the Mermaid source.
Follow all drawing conventions in
references/ascii-sequence-diagram.md,
including the inline output format.
Decision Tree
── Input is a spec document (not code)?
│ └─ Step S1: identify format, read references/spec-parsing-patterns.md
│
── Input is source code (not a spec)?
│ └─ Step 1: grep for handshake/round/send/recv entry points
│
── Both spec and code provided?
│ └─ Run Spec Workflow (S1–S5) first to build canonical diagram,
│ then read code and annotate divergences with ⚠️
│
── Spec is a known protocol (TLS, Noise, Signal, X3DH, FROST)?
│ └─ Read references/protocol-patterns.md and use canonical flow as skeleton
│
── Spec is ProVerif (.pv) or Tamarin (.spthy)?
│ └─ Read references/spec-parsing-patterns.md → Formal Models section
│
── Spec message ordering is ambiguous?
│ └─ Infer from round/section structure, annotate with ⚠️
│
── Can't identify parties from spec?
│ └─ Check "Parties"/"Notation" sections; for ProVerif read process names;
│ for Tamarin read rule names and fact arguments
│
── Don't know which code files implement the protocol?
│ └─ Step 1: grep for handshake/round/send/recv entry points
│
── Can't identify parties from struct names?
│ └─ Read test files — test setup reveals roles
│
── Protocol runs in-process (no network calls)?
│ └─ Treat function argument passing at role boundaries as messages
│
── MPC / threshold protocol with N parties?
│ └─ Read references/protocol-patterns.md → MPC section
│
── Mermaid syntax error?
│ └─ Read references/mermaid-sequence-syntax.md → Common Pitfalls
│
└─ ASCII drawing conventions?
└─ Read references/ascii-sequence-diagram.md
Examples
Code path — examples/simple-handshake/:
protocol.py — two-party authenticated key exchange (X25519 DH +
Ed25519 signing + HKDF + ChaCha20-Poly1305)
expected-output.md — exact ASCII diagram and Mermaid file the skill
should produce for that protocol
Spec path (ProVerif) — examples/simple-proverif/:
model.pv — HMAC challenge-response authentication modeled in ProVerif
expected-output.md — step-by-step extraction walkthrough (parties,
message flow, crypto ops) and the exact ASCII diagram and Mermaid file the
skill should produce
Study the relevant example before working on an unfamiliar input.
Supporting Documentation
- references/spec-parsing-patterns.md —
Extraction rules for RFC, academic paper/pseudocode, informal prose, ProVerif,
and Tamarin input formats; read during Step S1
- references/mermaid-sequence-syntax.md —
Participant syntax, arrow types, activations, grouping blocks, escaping rules,
and common rendering pitfalls
- references/protocol-patterns.md —
Canonical message flows for TLS 1.3, Noise, X3DH, Double Ratchet, Shamir
secret sharing, commit-reveal, and generic MPC rounds; use as a reference
when comparing implementation against spec
- references/ascii-sequence-diagram.md —
Column layout, arrow conventions, self-loops, phase labels, and inline
output format for the ASCII diagram
1---2name: crypto-protocol-diagram3description: Extracts protocol message flow from source code, RFCs, academic papers, pseudocode, informal prose, ProVerif (.pv), or Tamarin (.spthy) models and generates Mermaid sequenceDiagrams with cryptographic annotations. Use when diagramming a crypto protocol, visualizing a handshake or key exchange flow, extracting message flow from a spec or RFC, diagramming a ProVerif or Tamarin model, or drawing sequence diagrams for TLS, Noise, Signal, X3DH, Double Ratchet, FROST, DH, or ECDH protocols.4---56# Crypto Protocol Diagram78Produces a Mermaid `sequenceDiagram` (written to file) and an ASCII sequence9diagram (printed inline) from either:1011- **Source code** implementing a cryptographic protocol, or12- **A specification** — RFC, academic paper, pseudocode, informal prose,13 ProVerif (`.pv`), or Tamarin (`.spthy`) model.1415**Tools used:** Read, Write, Grep, Glob, Bash, WebFetch (for URL specs).1617Unlike the `diagramming-code` skill (which visualizes code structure), this skill18extracts **protocol semantics**: who sends what to whom, what cryptographic19transformations occur at each step, and what protocol phases exist.2021For call graphs, class hierarchies, or module dependency maps, use the22`diagramming-code` skill instead.2324## When to Use2526- User asks to diagram, visualize, or extract a cryptographic protocol27- Input is source code implementing a handshake, key exchange, or multi-party protocol28- Input is an RFC, academic paper, pseudocode, or formal model (ProVerif/Tamarin)29- User names a specific protocol (TLS, Noise, Signal, X3DH, FROST)3031## When NOT to Use3233- User wants a call graph, class hierarchy, or module dependency map — use `diagramming-code`34- User wants to formally verify a protocol — use `mermaid-to-proverif` (after generating the diagram)35- Input has no cryptographic protocol semantics (no parties, no message exchange)3637## Rationalizations to Reject3839| Rationalization | Why It's Wrong | Required Action |40|-----------------|----------------|-----------------|41| "The protocol is simple, I can diagram from memory" | Memory-based diagrams miss steps and invert arrows | Read the source or spec systematically |42| "I'll skip the spec path since code exists" | Code may diverge from the spec — both paths catch different bugs | When both exist, run spec workflow first, then annotate code divergences |43| "Crypto annotations are optional decoration" | Without crypto annotations, the diagram is just a message flow — useless for security review | Annotate every cryptographic operation |44| "The abort path is obvious, no need for alt blocks" | Implicit abort handling hides missing error checks | Show every abort/error path with `alt` blocks |45| "I don't need to check the examples first" | The examples define the expected output quality bar | Study the relevant example before working on unfamiliar input |46| "ProVerif/Tamarin models are code, not specs" | Formal models are specifications — they describe intended behavior, not implementation | Use the spec workflow (S1–S5) for `.pv` and `.spthy` files |4748---4950## Workflow5152```53Protocol Diagram Progress:54- [ ] Step 0: Determine input type (code / spec / both)55- [ ] Step 1 (code) or S1–S5 (spec): Extract protocol structure56- [ ] Step 6: Generate sequenceDiagram57- [ ] Step 7: Verify and deliver58```5960---6162### Step 0: Determine Input Type6364Before doing anything else, classify the input:6566| Signal | Input type |67|--------|-----------|68| Source file extensions (`.py`, `.rs`, `.go`, `.ts`, `.js`, `.cpp`, `.c`) | **Code** |69| Function/class definitions, import statements | **Code** |70| RFC-style section headers (`§`, `Section X.Y`, `MUST`/`SHALL` keywords) | **Spec** |71| `Algorithm`/`Protocol`/`Figure` labels, mathematical notation | **Spec** |72| ProVerif file (`.pv`) with `process`, `let`, `in`/`out` | **Spec** |73| Tamarin file (`.spthy`) with `rule`, `--[...]->` | **Spec** |74| Plain prose or numbered steps describing a protocol | **Spec** |75| Both source files and a spec document | **Both** (annotate divergences with `⚠️`) |7677- **Code only** → skip to Step 1 below78- **Spec only** → skip to Spec Workflow (S1–S5) below79- **Both** → run Spec Workflow first, then use the code-reading steps to verify80 the implementation against the spec diagram and annotate any divergences with `⚠️`81- **Ambiguous** → ask the user: "Is this a source code file, a specification82 document, or both?"8384---8586### Step 1: Locate Protocol Entry Points8788Grep for function names, type names, and comments that reveal the protocol:8990```bash91# Find handshake, session, round, phase entry points92rg -l "handshake|session_init|round[_0-9]|setup|keygen|send_msg|recv_msg" {targetDir}9394# Find crypto primitives in use95rg "sign|verify|encrypt|decrypt|dh|ecdh|kdf|hkdf|hmac|hash|commit|reveal|share" \96 {targetDir} --type-add 'src:*.{py,rs,go,ts,js,cpp,c}' -t src -l97```9899Start reading from the highest-level orchestration function — the one that calls100into handshake phases or the main protocol loop.101102### Step 2: Identify Parties and Roles103104Extract participant names from:105106- Struct/class names: `Client`, `Server`, `Initiator`, `Responder`, `Prover`,107 `Verifier`, `Dealer`, `Party`, `Coordinator`108- Function parameter names that carry state for a role109- Comments declaring the protocol role110- Test fixtures that set up two-party or N-party scenarios111112Map these to Mermaid `participant` declarations. Use short, readable aliases:113114```115participant I as Initiator116participant R as Responder117```118119### Step 3: Trace Message Flow120121Follow state transitions and network sends/receives. Look for patterns like:122123| Pattern | Meaning |124|---------|---------|125| `send(msg)` / `recv()` | Direct message exchange |126| `serialize` + `transmit` | Structured message sent |127| Return value passed to other party's function | Logical message (in-process) |128| `round1_output` → `round2_input` | Round-based MPC step |129| Struct fields named `ephemeral_key`, `ciphertext`, `mac`, `tag` | Message contents |130131For **in-process** protocol implementations (where both parties run in the same132process), treat function call boundaries as logical message sends when they133represent what would be a network boundary in deployment.134135### Step 4: Annotate Cryptographic Operations136137At each protocol step, identify and label:138139| Operation | Diagram annotation |140|-----------|-------------------|141| Key generation | `Note over A: keygen(params) → pk, sk` |142| DH / ECDH | `Note over A,B: DH(sk_A, pk_B)` |143| KDF / HKDF | `Note over A: HKDF(ikm, salt, info)` |144| Signing | `Note over A: Sign(sk, msg) → σ` |145| Verification | `Note over B: Verify(pk, msg, σ)` |146| Encryption | `Note over A: Enc(key, plaintext) → ct` |147| Decryption | `Note over B: Dec(key, ct) → plaintext` |148| Commitment | `Note over A: Commit(value, rand) → C` |149| Hash | `Note over A: H(data) → digest` |150| Secret sharing | `Note over D: Share(secret, t, n) → {s_i}` |151| Threshold combine | `Note over C: Combine({s_i}) → secret` |152153Keep annotations concise — use mathematical shorthand, not code.154155### Step 5: Identify Protocol Phases156157Group message steps into named phases using `rect` or `Note` blocks:158159Common phases to detect:160- **Setup / Key Generation**: party key creation, trusted setup, parameter gen161- **Handshake / Init**: ephemeral key exchange, nonce exchange, version negotiation162- **Authentication**: identity proof, certificate exchange, signature verification163- **Key Derivation**: session key derivation from shared secrets164- **Data Transfer / Main Protocol**: encrypted application data exchange165- **Finalization / Teardown**: session close, MAC verification, abort handling166167Detect abort/error paths and show them with `alt` blocks.168169---170171## Spec Workflow (S1–S5)172173Use this path when the input is a specification document rather than source code.174After completing S1–S5, continue with Step 6 (Generate sequenceDiagram) and175Step 7 (Verify and deliver) from the code workflow above.176177### Step S1: Ingest the Spec178179Obtain the full spec text:180181- **File path provided** → read with the Read tool182- **URL provided** → fetch with WebFetch183- **Pasted inline** → work directly from conversation context184185Then identify the spec format and read186[references/spec-parsing-patterns.md](references/spec-parsing-patterns.md)187for format-specific extraction guidance:188189| Format | Signals |190|--------|---------|191| RFC | `RFC XXXX`, `MUST`/`SHALL`/`SHOULD`, ABNF grammars, section-numbered prose |192| Academic paper / pseudocode | `Algorithm X`, `Protocol X`, `Figure X`, numbered steps, `←`/`→` in math mode |193| Informal prose | Numbered lists, "A sends B ...", plain English descriptions |194| ProVerif (`.pv`) | `process`, `let`, `in(ch, x)`, `out(ch, msg)`, `!` (replication) |195| Tamarin (`.spthy`) | `rule`, `--[ ]->`, `Fr(~x)`, `!Pk(A, pk)`, `In(m)`, `Out(m)` |196197If the spec references a known named protocol (TLS, Noise, Signal, X3DH, Double198Ratchet, FROST), also read199[references/protocol-patterns.md](references/protocol-patterns.md) to use its200canonical flow as a skeleton and fill in spec-specific details.201202### Step S2: Extract Parties and Roles203204Identify all protocol participants. Look for:205206- **Named roles** in prose or pseudocode: `Alice`, `Bob`, `Client`, `Server`,207 `Initiator`, `Responder`, `Prover`, `Verifier`, `Dealer`, `Party_i`,208 `Coordinator`, `Signer`209- **Section headers**: "Parties", "Roles", "Participants", "Setup", "Notation"210- **ProVerif**: process names at top level (`let ClientProc(...)`, `let ServerProc(...)`)211- **Tamarin**: rule names and fact arguments (e.g. `!Pk($A, pk)` — `$A` is a party)212213Map each role to a Mermaid `participant` declaration. Use short IDs with214descriptive aliases (see naming conventions in215[references/mermaid-sequence-syntax.md](references/mermaid-sequence-syntax.md)).216217### Step S3: Extract Message Flow218219Trace what each party sends to whom and in what order. Extraction patterns by format:220221**RFC / informal prose:**222- Arrow notation: `A → B: msg`, `A -> B`223- Sentence patterns: "A sends B ...", "B responds with ...", "A transmits ...",224 "upon receiving X, B sends Y"225- Numbered steps: extract in order, inferring sender/receiver from context226227**Pseudocode:**228- Function signatures with explicit `sender`/`receiver` parameters229- `send(party, msg)` / `receive(party)` calls230- Return values passed as inputs to the other party's function in the next step231232**ProVerif (`.pv`):**233- `out(ch, msg)` — send on channel `ch`234- `in(ch, x)` — receive on channel `ch`, bind to `x`235- Match `out`/`in` pairs on the same channel to identify message flows236- `!` (replication) signals a role that handles multiple sessions237238**Tamarin (`.spthy`):**239- `In(m)` premise — receive message `m`240- `Out(m)` conclusion — send message `m`241- Rule name and ordering of rules reveal protocol rounds242- `Fr(~x)` — fresh random value generated by a party243- `--[ Label ]->` facts — security annotations, not messages244245Preserve the ordering and round structure. Group concurrent sends (broadcast)246using `par` blocks in the final diagram.247248### Step S4: Extract Cryptographic Operations249250For each protocol step, identify the cryptographic operations performed and which251party performs them:252253| Spec notation | Operation | Diagram annotation |254|---------------|-----------|-------------------|255| `keygen()`, `Gen(1^λ)` | Key generation | `Note over A: keygen() → pk, sk` |256| `DH(a, B)`, `g^ab` | DH / ECDH | `Note over A,B: DH(sk_A, pk_B)` |257| `KDF(ikm)`, `HKDF(...)` | Key derivation | `Note over A: HKDF(ikm, salt, info) → k` |258| `Sign(sk, m)`, `σ ← Sign` | Signing | `Note over A: Sign(sk, msg) → σ` |259| `Verify(pk, m, σ)` | Verification | `Note over B: Verify(pk, msg, σ)` |260| `Enc(k, m)`, `{m}_k` | Encryption | `Note over A: Enc(k, plaintext) → ct` |261| `Dec(k, c)` | Decryption | `Note over B: Dec(k, ct) → plaintext` |262| `H(m)`, `hash(m)` | Hash | `Note over A: H(data) → digest` |263| `Commit(v, r)`, `com` | Commitment | `Note over A: Commit(value, rand) → C` |264| ProVerif `senc(m, k)` | Symmetric encryption | `Note over A: Enc(k, m) → ct` |265| ProVerif `pk(sk)` | Public key derivation | `Note over A: pk = pk(sk)` |266| ProVerif `sign(m, sk)` | Signing | `Note over A: Sign(sk, m) → σ` |267268Identify security conditions and abort paths:269270- Prose: "if verification fails, abort", "only if ...", "reject if ..."271- Pseudocode: `assert`, `require`, `if ... abort`272- ProVerif: `if m = expected then ... else 0`273- Tamarin: contradicting facts or restriction lemmas274275These become `alt` blocks in the final diagram.276277### Step S5: Flag Spec Ambiguities278279Before moving to Step 6, check for gaps:280281- **Unclear message ordering**: infer from round structure or section order;282 annotate with `⚠️ ordering inferred from spec structure`283- **Implied parties**: if a party's role is implied but unnamed, give it a284 descriptive name and note the inference285- **Missing steps**: if the spec omits a step that the canonical pattern for286 this protocol requires, annotate:287 `⚠️ spec omits [step] — canonical protocol requires it`288- **Underspecified crypto**: if the spec says "encrypt" without specifying289 the scheme, annotate: `⚠️ encryption scheme not specified`290- **ProVerif/Tamarin**: private channels (`c` declared with `new c` or as a291 private free name) represent out-of-band channels — note them292293---294295<!-- Both code path (Steps 1–5) and spec path (Steps S1–S5) continue here -->296297### Step 6: Generate sequenceDiagram298299Produce Mermaid syntax following the rules in300[references/mermaid-sequence-syntax.md](references/mermaid-sequence-syntax.md).301302**Completeness over brevity.** Show every distinct message type. Omit repeated303loop iterations (use `loop` blocks instead), but never omit a distinct protocol304step.305306**Correctness over aesthetics.** The diagram must match what the code actually307does. If the code diverges from a known spec, annotate the divergence:308309```310Note over A,B: ⚠️ spec requires MAC here — implementation omits it311```312313### Step 7: Verify and Deliver314315Before delivering:316317- [ ] Every participant declared actually sends or receives at least one message318- [ ] Arrows point in the correct direction (sender → receiver)319- [ ] Cryptographic operations are on the correct party (the one computing them)320- [ ] If protocol phases are used, no arrows appear outside a phase block321- [ ] `alt` blocks cover known abort/error paths322- [ ] Diagram renders without syntax errors (check323 [references/mermaid-sequence-syntax.md](references/mermaid-sequence-syntax.md)324 for common pitfalls)325- [ ] If spec divergence found, annotated with `⚠️`326327**Write the diagram to a file.** Choose a filename derived from the protocol328name, e.g. `noise-xx-handshake.md` or `x3dh-key-agreement.md`. Write a329Markdown file with this structure:330331```markdown332# <Protocol Name> Sequence Diagram333334\`\`\`mermaid335sequenceDiagram336 ...337\`\`\`338339## Protocol Summary340341- **Parties:** ...342- **Round complexity:** ...343- **Key primitives:** ...344- **Authentication:** ...345- **Forward secrecy:** ...346- **Notable:** [spec deviations or security observations, or "none"]347```348349After writing the file, print an **ASCII sequence diagram** inline in the350response, followed by the Protocol Summary. State the output filename so the351user knows where to find the Mermaid source.352353Follow all drawing conventions in354[references/ascii-sequence-diagram.md](references/ascii-sequence-diagram.md),355including the inline output format.356357---358359## Decision Tree360361```362── Input is a spec document (not code)?363│ └─ Step S1: identify format, read references/spec-parsing-patterns.md364│365── Input is source code (not a spec)?366│ └─ Step 1: grep for handshake/round/send/recv entry points367│368── Both spec and code provided?369│ └─ Run Spec Workflow (S1–S5) first to build canonical diagram,370│ then read code and annotate divergences with ⚠️371│372── Spec is a known protocol (TLS, Noise, Signal, X3DH, FROST)?373│ └─ Read references/protocol-patterns.md and use canonical flow as skeleton374│375── Spec is ProVerif (.pv) or Tamarin (.spthy)?376│ └─ Read references/spec-parsing-patterns.md → Formal Models section377│378── Spec message ordering is ambiguous?379│ └─ Infer from round/section structure, annotate with ⚠️380│381── Can't identify parties from spec?382│ └─ Check "Parties"/"Notation" sections; for ProVerif read process names;383│ for Tamarin read rule names and fact arguments384│385── Don't know which code files implement the protocol?386│ └─ Step 1: grep for handshake/round/send/recv entry points387│388── Can't identify parties from struct names?389│ └─ Read test files — test setup reveals roles390│391── Protocol runs in-process (no network calls)?392│ └─ Treat function argument passing at role boundaries as messages393│394── MPC / threshold protocol with N parties?395│ └─ Read references/protocol-patterns.md → MPC section396│397── Mermaid syntax error?398│ └─ Read references/mermaid-sequence-syntax.md → Common Pitfalls399│400└─ ASCII drawing conventions?401 └─ Read references/ascii-sequence-diagram.md402```403404---405406## Examples407408**Code path** — `examples/simple-handshake/`:409410- **`protocol.py`** — two-party authenticated key exchange (X25519 DH +411 Ed25519 signing + HKDF + ChaCha20-Poly1305)412- **`expected-output.md`** — exact ASCII diagram and Mermaid file the skill413 should produce for that protocol414415**Spec path (ProVerif)** — `examples/simple-proverif/`:416417- **`model.pv`** — HMAC challenge-response authentication modeled in ProVerif418- **`expected-output.md`** — step-by-step extraction walkthrough (parties,419 message flow, crypto ops) and the exact ASCII diagram and Mermaid file the420 skill should produce421422Study the relevant example before working on an unfamiliar input.423424---425426## Supporting Documentation427428- **[references/spec-parsing-patterns.md](references/spec-parsing-patterns.md)** —429 Extraction rules for RFC, academic paper/pseudocode, informal prose, ProVerif,430 and Tamarin input formats; read during Step S1431- **[references/mermaid-sequence-syntax.md](references/mermaid-sequence-syntax.md)** —432 Participant syntax, arrow types, activations, grouping blocks, escaping rules,433 and common rendering pitfalls434- **[references/protocol-patterns.md](references/protocol-patterns.md)** —435 Canonical message flows for TLS 1.3, Noise, X3DH, Double Ratchet, Shamir436 secret sharing, commit-reveal, and generic MPC rounds; use as a reference437 when comparing implementation against spec438- **[references/ascii-sequence-diagram.md](references/ascii-sequence-diagram.md)** —439 Column layout, arrow conventions, self-loops, phase labels, and inline440 output format for the ASCII diagram