Crypto Protocol Diagrams

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:

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

<!-- Both code path (Steps 1–5) and spec path (Steps S1–S5) continue here -->

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:

• Every participant declared actually sends or receives at least one message
• Arrows point in the correct direction (sender → receiver)
• Cryptographic operations are on the correct party (the one computing them)
• If protocol phases are used, no arrows appear outside a phase block
• alt blocks cover known abort/error paths
• Diagram renders without syntax errors (check references/mermaid-sequence-syntax.md for common pitfalls)
• If spec divergence found, annotated with ⚠️

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