# crypto-protocol-diagram

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.

- **Kind:** skill
- **Source:** https://github.com/trailofbits/skills
- **Page:** https://forefy.com/skills/42e0991f-c4a1-437f-98cc-533fc9ccd0ba
- **API (JSON + files):** https://forefy.com/api/asr/42e0991f-c4a1-437f-98cc-533fc9ccd0ba

---

## SKILL.md

---
name: crypto-protocol-diagram
description: "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."
---

# 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:

```bash
# 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](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](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](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

---

<!-- 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](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](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:

```markdown
# <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](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](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](references/mermaid-sequence-syntax.md)** —
  Participant syntax, arrow types, activations, grouping blocks, escaping rules,
  and common rendering pitfalls
- **[references/protocol-patterns.md](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](references/ascii-sequence-diagram.md)** —
  Column layout, arrow conventions, self-loops, phase labels, and inline
  output format for the ASCII diagram

## agents

```

```

## agents/openai.yaml

```yaml
interface:
  icon_small: "assets/trail-of-bits-mark.svg"
  icon_large: "assets/trail-of-bits-mark.svg"
  brand_color: "#D83A34"
```

## assets

```

```

## assets/trail-of-bits-mark.svg

```

```

## examples

```

```

## examples/simple-handshake

```

```

## examples/simple-handshake/expected-output.md

# Expected Skill Output

This file shows what the `crypto-protocol-diagram` skill should produce when
run on `protocol.py`. It covers both the inline response (ASCII diagram +
Protocol Summary) and the written Mermaid file.

---

## Inline Response

```
Protocol: Simple Authenticated Key Exchange
Output:   simple-authenticated-key-exchange.md

Initiator                          Responder
   |                                   |
   |   -- Setup (out-of-band) --       |
   +--.                                |
   |  | keygen() → sk_i, pk_i          |
   |<-'                                |
   |                                   +--.
   |                    keygen() → sk_r, pk_r |
   |                                   |<-'
   |                                   |
   |   -- Handshake --                 |
   +--.                                |
   |  | keygen() → ek_i, epk_i         |
   |  | sig_i = Sign(sk_i, "msg1"||epk_i) |
   |<-'                                |
   |                                   |
   +---------------------------------->|  epk_i || sig_i
   |                                   |
   |                                   +--.
   |           Verify(pk_i, sig_i)     |  |
   |     keygen() → ek_r, epk_r        |  |
   |  sig_r = Sign(sk_r, "msg2"||transcript) |
   |     dh = DH(ek_r, epk_i)          |  |
   |     sk = HKDF(dh, transcript)     |<-'
   |                                   |
   |<- - - - - - - - - - - - - - - - - +  epk_r || sig_r
   |                                   |
   +--.                                |
   |  | Verify(pk_r, sig_r)            |
   |  | dh = DH(ek_i, epk_r)           |
   |  | sk = HKDF(dh, transcript)      |
   |<-'                                |
   |                                   |
   |   -- Application Data --          |
   |                                   |
   +---------------------------------->|  ChaCha20Poly1305(sk, nonce, plaintext)
   |                                   |

   [on signature verification failure]
   |  abort(INVALID_SIGNATURE)         |
   |<- - - - - - - - - - - - - - - - - +

## Protocol Summary

- **Parties:** Initiator, Responder
- **Round complexity:** 1 round trip (2 messages)
- **Key primitives:** X25519 (ephemeral DH), Ed25519 (signing), HKDF-SHA256, ChaCha20-Poly1305
- **Authentication:** mutual — both parties sign their ephemeral keys with long-term Ed25519 keys
- **Forward secrecy:** yes — session key derived from ephemeral DH; compromise of static keys does not expose past sessions
- **Notable:** static keys are assumed registered out-of-band (no in-protocol key transmission); transcript binding covers only ephemeral public keys, not party identities — an implementation that doesn't bind pk_i and pk_r into the transcript is vulnerable to identity mislabeling
```

---

## Written Mermaid File (`simple-authenticated-key-exchange.md`)

```markdown
# Simple Authenticated Key Exchange Sequence Diagram

\`\`\`mermaid
sequenceDiagram
    participant I as Initiator
    participant R as Responder

    rect rgba(100, 149, 237, 0.15)
        Note over I,R: Setup (out-of-band key registration)
        Note over I: keygen() → sk_i, pk_i
        Note over R: keygen() → sk_r, pk_r
    end

    rect rgba(46, 204, 113, 0.15)
        Note over I,R: Handshake
        Note over I: keygen() → ek_i, epk_i
        Note over I: sig_i = Sign(sk_i, "msg1" || epk_i)
        I->>R: epk_i || sig_i
        Note over R: Verify(pk_i, "msg1" || epk_i, sig_i)
        Note over R: keygen() → ek_r, epk_r
        Note over R: transcript = epk_i || epk_r
        Note over R: sig_r = Sign(sk_r, "msg2" || transcript)
        Note over R: dh = DH(ek_r, epk_i)
        Note over R: sk_r = HKDF(dh || transcript, info="session-key-v1")
        R-->>I: epk_r || sig_r
        Note over I: Verify(pk_r, "msg2" || transcript, sig_r)
        Note over I: dh = DH(ek_i, epk_r)
        Note over I: sk_i = HKDF(dh || transcript, info="session-key-v1")
    end

    rect rgba(241, 196, 15, 0.15)
        Note over I,R: Application Data
        I->>R: ChaCha20Poly1305(sk, nonce, plaintext)
    end

    alt signature verification failure
        R-->>I: abort(INVALID_SIGNATURE)
    end
\`\`\`

## Protocol Summary

- **Parties:** Initiator, Responder
- **Round complexity:** 1 round trip (2 messages)
- **Key primitives:** X25519 (ephemeral DH), Ed25519 (signing), HKDF-SHA256, ChaCha20-Poly1305
- **Authentication:** mutual — both parties sign their ephemeral keys with long-term Ed25519 keys
- **Forward secrecy:** yes — session key derived from ephemeral DH; compromise of static keys does not expose past sessions
- **Notable:** static keys are assumed registered out-of-band (no in-protocol key transmission); transcript binding covers only ephemeral public keys, not party identities — an implementation that doesn't bind pk_i and pk_r into the transcript is vulnerable to identity mislabeling
```

## examples/simple-handshake/protocol.py

```python
# /// script
# requires-python = ">=3.12"
# dependencies = ["cryptography>=42.0"]
# ///
"""
Simple authenticated key exchange protocol (2 messages, 1 round trip).

Both parties hold long-term Ed25519 signing keys registered out-of-band.
The protocol establishes a forward-secret session key via ephemeral X25519 DH,
with mutual authentication via signatures over the transcript.

Message flow:
  1. Initiator → Responder : epk_i, sig_i
  2. Responder → Initiator : epk_r, sig_r
  Both derive: session_key = HKDF(DH(ek_i, epk_r), transcript)
"""

import os

from cryptography.hazmat.primitives import hashes, serialization  # type: ignore
from cryptography.hazmat.primitives.asymmetric.ed25519 import (  # type: ignore
    Ed25519PrivateKey,
    Ed25519PublicKey,
)
from cryptography.hazmat.primitives.asymmetric.x25519 import (  # type: ignore
    X25519PrivateKey,
    X25519PublicKey,
)
from cryptography.hazmat.primitives.ciphers.aead import ChaCha20Poly1305  # type: ignore
from cryptography.hazmat.primitives.kdf.hkdf import HKDF  # type: ignore

# ---------------------------------------------------------------------------
# Key types
# ---------------------------------------------------------------------------


class StaticKeypair:
    """Long-term Ed25519 signing keypair (registered out-of-band)."""

    def __init__(self) -> None:
        self._sk = Ed25519PrivateKey.generate()
        self.pk = self._sk.public_key()

    def sign(self, message: bytes) -> bytes:
        return self._sk.sign(message)

    def public_bytes(self) -> bytes:
        return self.pk.public_bytes(serialization.Encoding.Raw, serialization.PublicFormat.Raw)


class EphemeralKeypair:
    """Single-use X25519 DH keypair."""

    def __init__(self) -> None:
        self._sk = X25519PrivateKey.generate()
        self.pk = self._sk.public_key()

    def exchange(self, peer_epk: X25519PublicKey) -> bytes:
        return self._sk.exchange(peer_epk)

    def public_bytes(self) -> bytes:
        return self.pk.public_bytes(serialization.Encoding.Raw, serialization.PublicFormat.Raw)


# ---------------------------------------------------------------------------
# Protocol messages
# ---------------------------------------------------------------------------


def _derive_session_key(dh_output: bytes, transcript: bytes) -> bytes:
    """HKDF-SHA256 over DH output, bound to the full transcript."""
    return HKDF(
        algorithm=hashes.SHA256(),
        length=32,
        salt=None,
        info=b"session-key-v1",
    ).derive(dh_output + transcript)


def initiator_send_msg1(
    static: StaticKeypair,
) -> tuple[EphemeralKeypair, bytes]:
    """
    Initiator builds message 1.

    Returns (ephemeral_keypair, wire_bytes).
    wire_bytes = epk_i (32 bytes) || sig_i (64 bytes)
    """
    ek = EphemeralKeypair()
    epk_bytes = ek.public_bytes()
    sig = static.sign(b"msg1:" + epk_bytes)
    return ek, epk_bytes + sig


def responder_recv_msg1_send_msg2(
    msg1: bytes,
    initiator_pk: Ed25519PublicKey,
    static: StaticKeypair,
) -> tuple[bytes, bytes, bytes]:
    """
    Responder processes message 1 and builds message 2.

    Returns (session_key, msg2_wire_bytes, transcript).
    msg2_wire_bytes = epk_r (32 bytes) || sig_r (64 bytes)
    """
    epk_i_bytes, sig_i = msg1[:32], msg1[32:]

    # Verify initiator's ephemeral key is authentic.
    initiator_pk.verify(sig_i, b"msg1:" + epk_i_bytes)

    epk_i = X25519PublicKey.from_public_bytes(epk_i_bytes)

    ek_r = EphemeralKeypair()
    epk_r_bytes = ek_r.public_bytes()

    transcript = epk_i_bytes + epk_r_bytes
    sig_r = static.sign(b"msg2:" + transcript)

    dh_output = ek_r.exchange(epk_i)
    session_key = _derive_session_key(dh_output, transcript)

    return session_key, epk_r_bytes + sig_r, transcript


def initiator_recv_msg2(
    msg2: bytes,
    ek_i: EphemeralKeypair,
    responder_pk: Ed25519PublicKey,
    epk_i_bytes: bytes,
) -> bytes:
    """
    Initiator processes message 2 and derives the session key.

    Returns session_key.
    """
    epk_r_bytes, sig_r = msg2[:32], msg2[32:]

    transcript = epk_i_bytes + epk_r_bytes

    # Verify responder's contribution is authentic.
    responder_pk.verify(sig_r, b"msg2:" + transcript)

    epk_r = X25519PublicKey.from_public_bytes(epk_r_bytes)

    dh_output = ek_i.exchange(epk_r)
    return _derive_session_key(dh_output, transcript)


# ---------------------------------------------------------------------------
# Application data (post-handshake)
# ---------------------------------------------------------------------------


def encrypt(session_key: bytes, plaintext: bytes, nonce: bytes) -> bytes:
    return ChaCha20Poly1305(session_key).encrypt(nonce, plaintext, None)


def decrypt(session_key: bytes, ciphertext: bytes, nonce: bytes) -> bytes:
    return ChaCha20Poly1305(session_key).decrypt(nonce, ciphertext, None)


# ---------------------------------------------------------------------------
# Demo
# ---------------------------------------------------------------------------

if __name__ == "__main__":
    # Out-of-band key registration
    initiator_static = StaticKeypair()
    responder_static = StaticKeypair()

    # --- Handshake ---
    ek_i, msg1 = initiator_send_msg1(initiator_static)
    epk_i_bytes = msg1[:32]

    sk_r, msg2, _ = responder_recv_msg1_send_msg2(
        msg1,
        initiator_static.pk,
        responder_static,
    )

    sk_i = initiator_recv_msg2(
        msg2,
        ek_i,
        responder_static.pk,
        epk_i_bytes,
    )

    if sk_i != sk_r:
        raise RuntimeError("session keys must match")
    print("Handshake complete. Session keys match.")

    # --- Application data ---
    nonce = os.urandom(12)
    ct = encrypt(sk_i, b"hello, responder", nonce)
    pt = decrypt(sk_r, ct, nonce)
    print(f"Decrypted: {pt}")
```

## examples/simple-proverif

```

```

## examples/simple-proverif/expected-output.md

# Expected Output: simple-proverif

This is the exact ASCII diagram and Mermaid file the `crypto-protocol-diagram`
skill should produce when given `model.pv` as input.

---

## Step 0 classification

Input: `model.pv` — ProVerif file (`.pv` extension, contains `process`, `let`,
`in`/`out`). Input type: **Spec (ProVerif)**.

## Step S2: Parties extracted

- `AliceProc` → participant `A as Alice`
- `BobProc` → participant `B as Bob`

## Step S3: Message flow (channel `c`)

| # | `out` | `in` | Message |
|---|-------|------|---------|
| 1 | `AliceProc` | `BobProc` | `identity` |
| 2 | `BobProc` | `AliceProc` | `nonce` (fresh) |
| 3 | `AliceProc` | `BobProc` | `mac = HMAC(k, nonce \|\| identity)` |
| 4 | `BobProc` | — | `true` (auth success, conditional) |

## Step S4: Crypto operations

- `AliceProc`: `hmac(key, concat(nonce, identity))` → `Note over A: mac = HMAC(k, nonce \|\| id)`
- `BobProc`: `new nonce` → `Note over B: nonce ← fresh()`
- `BobProc`: `checkhmac(mac, key, ...)` → `alt` block (verify succeeds / fails)

## Step S5: Ambiguities

- Dolev-Yao model applies: annotate with `⚠️`
- Auth success sends `true` over `c` — in a real protocol this would be
  implicit; annotate as optional output

---

## Inline ASCII Diagram

```
Protocol: HMAC Challenge-Response Authentication (ProVerif model)
Output:   hmac-challenge-response.md

Alice                    Bob
   |                      |
   |   -- Authentication  |  --
   |                      |
   +--------------------->|  identity
   |                      |
   |                      +--.
   |                      |  | nonce ← fresh()
   |                      |<-'
   |                      |
   |       nonce          |
   |<- - - - - - - - - - -+
   |                      |
   +--.                   |
   |  | mac = HMAC(k,     |
   |  | nonce || id)      |
   |<-'                   |
   |                      |
   +--------------------->|  mac
   |                      |
   |                      +--.
   |                      |  | checkHMAC(mac, k,
   |                      |  | nonce || identity)
   |                      |<-'
   |                      |
   |  [on verify success] |
   |                      +----.
   |                      |    | auth_ok
   |                      |<---'
   |                      |
   |  [on verify failure] |
   |                      | (abort)

⚠️ ProVerif note: all messages transit adversary network (Dolev-Yao model)
```

## Protocol Summary

- **Parties:** Alice (initiator), Bob (responder/verifier)
- **Round complexity:** 1.5 RTT (3 messages)
- **Key primitives:** HMAC with shared symmetric key; fresh nonce
- **Authentication:** Unilateral (Alice authenticates to Bob only)
- **Forward secrecy:** No (static shared key `k`; compromise reveals all sessions)
- **Notable:** `query attacker(k)` verifies the shared key remains secret under
  Dolev-Yao. No mutual authentication — Bob does not prove identity to Alice.

---

## Mermaid File: hmac-challenge-response.md

````markdown
# HMAC Challenge-Response Authentication Sequence Diagram

```mermaid
sequenceDiagram
    participant A as Alice
    participant B as Bob

    Note over A,B: ⚠️ ProVerif Dolev-Yao model — all messages transit adversary network

    rect rgba(241, 196, 15, 0.15)
        Note over A,B: Authentication
        A->>B: identity
        Note over B: nonce ← fresh()
        B-->>A: nonce
        Note over A: mac = HMAC(k, nonce || identity)
        A->>B: mac
        Note over B: checkHMAC(mac, k, nonce || identity)
        alt verification succeeds
            Note over B: auth_ok
        else verification fails
            Note over B: abort
        end
    end
```

## Protocol Summary

- **Parties:** Alice (initiator), Bob (responder)
- **Round complexity:** 1.5 RTT (3 messages)
- **Key primitives:** HMAC with shared symmetric key; fresh nonce
- **Authentication:** Unilateral (Alice → Bob only)
- **Forward secrecy:** No
- **Notable:** No mutual authentication. `query attacker(k)` checks key secrecy.
````

## examples/simple-proverif/model.pv

```

```

## references

```

```

## references/ascii-sequence-diagram.md

# ASCII Sequence Diagram Reference

Rules for drawing ASCII sequence diagrams inline in responses.

## Column Layout

Lay out participants as column headers, each above a vertical `|` lifeline.
Space columns ~28–32 characters apart so labels fit without wrapping:

```
Initiator                 Responder
   |                         |
   |                         |
```

For three or more participants, extend the layout rightward:

```
Client          Server          CA
   |               |             |
   |               |             |
```

## Arrow Conventions

| Element | Syntax | Use for |
|---------|--------|---------|
| Request (→) | `+------>` | message send |
| Reply (←) | `<- - - -+` | response / reply |
| Lost / async | `+------x` | dropped message |

- Sending end: `+`
- Receiving end: `>` (rightward) or `<` (leftward)
- Solid lines `---` for sends; dashed `- - -` for responses/replies
- Label goes **on the arrow line**, positioned between the two lifelines

```
   |                         |
   +------------------------>|  epk_I
   |                         |
   |  epk_R, Enc(k, cert_R)  |
   |<- - - - - - - - - - - - +
   |                         |
```

## Self-Loops (Local Computation)

For operations that happen at a single party without sending a message:

```
   |                         |
   +--.                      |
   |  | Sign(sk, transcript) |
   |<-'                      |
   |                         |
```

## Phase Labels

Group related steps under a phase label:

```
   |   -- Key Exchange --    |
   |                         |
   +------------------------>|  epk_I
   |                         |
```

## Abort / Error Paths

Place abort paths after the main flow, separated by a blank line:

```
   |   [on auth failure]     |
   |  abort(AUTH_FAILED)     |
   |<- - - - - - - - - - - - +
```

## Width and Labels

- Keep lines under ~60 characters wide
- If a label is too long, abbreviate it (e.g. `Enc(k,id||σ)`) and add a
  legend below the diagram explaining the abbreviations

## Inline Output Format

```
Protocol: <Name>
Output:   <filename>

<Participant1>            <Participant2>
   |                         |
   ...

## Protocol Summary

- **Parties:** ...
- **Round complexity:** ...
- **Key primitives:** ...
- **Authentication:** ...
- **Forward secrecy:** ...
- **Notable:** none
```

## references/mermaid-sequence-syntax.md

# Mermaid Sequence Diagram Syntax Reference

## Basic Structure

```
sequenceDiagram
    participant A as Alice
    participant B as Bob
    A->>B: Hello
    B-->>A: Hi
```

Every sequence diagram starts with `sequenceDiagram` on its own line (no
indentation). Participants are declared with `participant` before they appear
in messages; if undeclared, Mermaid auto-creates them in order of first
appearance — but always declare explicitly for crypto protocols to control
ordering.

---

## Participant Declarations

```
participant A             # ID = display name
participant A as Alice    # short ID, long display name
actor A as Alice          # person icon instead of box
```

**Ordering:** Participants are rendered left-to-right in declaration order.
Arrange them so that the dominant message direction flows left-to-right:
Initiator → Responder, Client → Server, Prover → Verifier.

**Naming conventions for crypto:**

| Role | Suggested ID | Display name |
|------|-------------|--------------|
| Initiator | `I` | Initiator |
| Responder | `R` | Responder |
| Client | `C` | Client |
| Server | `S` | Server |
| Trusted third party | `TTP` | TTP |
| Prover | `P` | Prover |
| Verifier | `V` | Verifier |
| Dealer | `D` | Dealer |
| Party i | `P1`, `P2`, … | Party 1, Party 2, … |
| Certificate Authority | `CA` | CA |

---

## Arrow Types

| Syntax | Arrow | Use for |
|--------|-------|---------|
| `A->>B: msg` | solid, open arrowhead | synchronous message send |
| `A-->>B: msg` | dashed, open arrowhead | reply / response |
| `A->B: msg` | solid, no arrowhead | passive / internal note |
| `A-->B: msg` | dashed, no arrowhead | async / passive reply |
| `A-xB: msg` | solid, X head | message lost / dropped |
| `A--xB: msg` | dashed, X head | async lost message |
| `A-)B: msg` | solid, async arrowhead | fire-and-forget |
| `A--)B: msg` | dashed, async arrowhead | async reply |

**For crypto protocols**, use `->>` for all protocol messages and `-->>` for
responses/replies. Reserve `-->` and `--x` for error/abort paths inside `alt`
blocks.

---

## Notes

Attach explanatory text to one or two participants:

```
Note over A: keygen() → pk, sk
Note over A,B: shared_secret = DH(sk_A, pk_B)
Note right of A: internal computation
Note left of B: validation step
```

Use `Note over` for cryptographic operations that happen at a party without
a message being sent. Use `Note over A,B` to annotate a shared computation or
the meaning of a message between them.

**Keep notes short.** Use mathematical shorthand:
- `HKDF(IKM=DH_out, salt, info) → k`
- `Sign(sk, transcript) → σ`
- `Verify(pk, transcript, σ)`
- `Enc(k, plaintext, AD) → ct || tag`
- `H(nonce || msg) → c`

---

## Activation Bars

Show when a participant is "active" (processing):

```
activate A
A->>B: request
B-->>A: response
deactivate A
```

Or inline with `+` / `-`:

```
A->>+B: request
B-->>-A: response
```

Use activations sparingly in protocol diagrams — they add noise unless the
protocol has clear request/response pairing that benefits from showing
duration.

---

## Grouping Blocks

### `rect` — colored background region

```
rect rgba(100, 149, 237, 0.15)
    Note over I,R: Phase 1: Key Exchange
    I->>R: ephemeral_pk
    R-->>I: ephemeral_pk
end
```

Use `rect` with a distinct color per protocol phase. Suggested palette:

| Phase | Color |
|-------|-------|
| Setup / Key Generation | `rgba(100, 149, 237, 0.15)` — blue |
| Handshake | `rgba(46, 204, 113, 0.15)` — green |
| Authentication | `rgba(241, 196, 15, 0.15)` — yellow |
| Key Derivation | `rgba(155, 89, 182, 0.15)` — purple |
| Data Transfer | `rgba(230, 196, 15, 0.12)` — gold |
| Error / Abort | `rgba(231, 76, 60, 0.15)` — red |

### `loop` — repeated block

```
loop for each data chunk
    A->>B: Enc(k, chunk_i) → ct_i
    B-->>A: ack
end
```

Use `loop` when a message exchange repeats N times. Avoid unrolling loops that
would add 5+ identical arrow pairs.

### `alt` — conditional / branching

```
alt verification succeeds
    B-->>A: session_key
else verification fails
    B-->>A: abort
end
```

Use `alt` for protocol branches: success path vs. abort/error paths. Always
show the error path — it's where security properties break down.

### `opt` — optional block

```
opt if session resumption requested
    A->>B: session_ticket
end
```

Use `opt` for optional protocol extensions (e.g. session resumption, renegotiation).

### `par` — parallel execution

```
par
    A->>B: msg_1
and
    A->>C: msg_2
end
```

Use `par` for genuinely concurrent sends (broadcast in MPC, simultaneous sends
to multiple parties).

### `critical` — mutual exclusion region

```
critical database access
    A->>DB: update
end
```

Rarely needed in protocol diagrams; use for atomic operations if relevant.

---

## Message Labels

Labels appear after the colon on arrow lines:

```
A->>B: ClientHello(random, cipher_suites, extensions)
B-->>A: ServerHello(random, chosen_cipher, session_id)
```

**Formatting guidance:**

- Use `FieldName(value)` or `Type{field: value, ...}` for structured messages
- Use `||` for concatenation: `nonce || ciphertext || tag`
- Use `→` to show output of a computation in a note: `KDF(shared) → k_enc, k_mac`
- Keep labels under ~60 characters; move detail into `Note over` annotations
- Subscript with underscore: `pk_e` (ephemeral pubkey), `k_1`, `σ_A`

---

## Common Pitfalls

### Colon in message label breaks parsing

**Broken:**
```
A->>B: key: value
```

**Fixed:** Use HTML entity or restructure:
```
A->>B: key=value
A->>B: "key: value"
```

### Special characters in participant IDs

Participant IDs must be alphanumeric + underscore. Avoid spaces, hyphens,
brackets.

**Broken:**
```
participant Party-1
```

**Fixed:**
```
participant P1 as Party 1
```

### `end` keyword clash

If a message label contains the word `end`, it may terminate a block early.
Quote it or rephrase.

### Unclosed blocks

Every `rect`, `loop`, `alt`, `opt`, `par` must have a matching `end`. Missing
`end` causes the entire diagram to fail silently.

### Long label lines

Labels longer than ~80 characters may overflow in some renderers. Break across
multiple notes rather than one very long label.

### `Note over A,B` with wrong participant order

The two participants in `Note over A,B` must be in left-to-right declaration
order, not reversed. `Note over B,A` when A is declared before B will fail in
some renderers.

---

## Complete Example

```mermaid
sequenceDiagram
    participant I as Initiator
    participant R as Responder

    rect rgba(100, 149, 237, 0.15)
        Note over I,R: Phase 1: Key Exchange
        Note over I: keygen() → ek_I, epk_I
        I->>R: epk_I
        Note over R: keygen() → ek_R, epk_R
        R-->>I: epk_R
        Note over I,R: dh_out = DH(ek_I, epk_R) = DH(ek_R, epk_I)
        Note over I,R: k_send, k_recv = HKDF(dh_out, salt, "handshake")
    end

    rect rgba(241, 196, 15, 0.15)
        Note over I,R: Phase 2: Authentication
        Note over I: σ_I = Sign(sk_I, transcript)
        I->>R: Enc(k_send, identity_I || σ_I)
        Note over R: Verify(pk_I, transcript, σ_I)
        Note over R: σ_R = Sign(sk_R, transcript)
        R-->>I: Enc(k_recv, identity_R || σ_R)
        Note over I: Verify(pk_R, transcript, σ_R)
    end

    rect rgba(46, 204, 113, 0.15)
        Note over I,R: Phase 3: Data Transfer
        Note over I,R: k_app = HKDF(dh_out, transcript_hash, "application")
        loop application data
            I->>R: Enc(k_app, data_i, nonce_i)
            R-->>I: ack_i
        end
    end

    alt authentication failure
        R-->>I: abort(AUTHENTICATION_FAILED)
    end
```

## references/protocol-patterns.md

# Crypto Protocol Patterns Reference

Canonical message flows for common cryptographic protocols. Use these as a
reference when comparing an implementation against a known spec, or as a
starting skeleton when the implementation follows a named protocol.

---

## TLS 1.3 Handshake (RFC 8446)

**Parties:** Client (C), Server (S)
**Round complexity:** 1 RTT (0-RTT with resumption)

```
C → S: ClientHello(random, legacy_session_id, cipher_suites,
                   key_share[ecdhe], supported_versions=[TLS 1.3])

S → C: ServerHello(random, legacy_session_id, cipher_suite,
                   key_share[ecdhe], supported_versions=TLS 1.3)

Note: ECDHE shared secret derived by both sides
Note: HKDF chain: early_secret → handshake_secret → master_secret

S → C: {EncryptedExtensions}   (under handshake key)
S → C: {Certificate}           (server cert chain)
S → C: {CertificateVerify}     (Sign(sk_S, transcript))
S → C: {Finished}              (HMAC over transcript)

C → S: {Certificate}           (if mutual auth requested)
C → S: {CertificateVerify}     (Sign(sk_C, transcript))
C → S: {Finished}              (HMAC over transcript)

Both: derive application traffic keys from master_secret
C ↔ S: {Application Data}      (under application keys)
```

**Code signals:** Look for `ClientHello`, `ServerHello`, `key_share`,
`supported_versions`, `cipher_suite`, `HKDF`, `transcript_hash`, `Finished`.

---

## Noise Protocol Framework (https://noiseprotocol.org)

**Pattern family:** NN, NK, NX, KN, KK, KX, XN, XK, XX, IX, ...

### Noise_XX (most common: mutual auth, no prior knowledge)

**Parties:** Initiator (I), Responder (R)
**Round complexity:** 1.5 RTT

```
I → R: msg_1 = e
       (send ephemeral pubkey)

R → I: msg_2 = e, ee, s, es
       (send ephemeral pubkey,
        DH(e_R, e_I),
        send static pubkey encrypted,
        DH(s_R, e_I))

I → R: msg_3 = s, se
       (send static pubkey encrypted,
        DH(s_I, e_R))

Both: transport keys derived from chained hash state
I ↔ R: encrypted transport messages
```

**State machine:** `CipherState → SymmetricState → HandshakeState`.
Look for `MixKey`, `MixHash`, `EncryptAndHash`, `DecryptAndHash`,
`Split` (produces two `CipherState` objects for send/recv).

**Code signals:** `HandshakeState`, `CipherState`, `SymmetricState`,
`h` (handshake hash), `ck` (chaining key), `n` (nonce counter),
pattern strings like `"XX"`, `"IK"`.

### Noise_IK (identity-hiding initiator, known responder static key)

```
I → R: msg_1 = e, es, s, ss
       (ephemeral, DH(e_I, s_R), static (encrypted), DH(s_I, s_R))

R → I: msg_2 = e, ee, se
       (ephemeral, DH(e_R, e_I), DH(e_R, s_I))
```

---

## Signal Protocol

### X3DH (Extended Triple Diffie-Hellman) Key Agreement

**Parties:** Alice (A), Bob (B), Server (S)
**Purpose:** Establish shared secret for asynchronous messaging

```
Note over B: Publish to server:
             IK_B (identity key),
             SPK_B (signed prekey) + Sig(IK_B, SPK_B),
             {OPK_B_i} (one-time prekeys)

Note over A: Fetch Bob's key bundle from server
A → S: fetch_prekey_bundle(Bob)
S → A: IK_B, SPK_B, Sig, OPK_B_1

Note over A: Verify Sig(IK_B, SPK_B)
Note over A: EK_A = generate ephemeral keypair

Note over A: DH1 = DH(IK_A, SPK_B)
             DH2 = DH(EK_A, IK_B)
             DH3 = DH(EK_A, SPK_B)
             DH4 = DH(EK_A, OPK_B_1)  [if one-time prekey available]
             SK = KDF(DH1 || DH2 || DH3 || DH4)

A → B: InitialMessage(IK_A, EK_A, OPK_B_id, Enc(SK, initial_plaintext))

Note over B: Recompute DH1..DH4, derive SK
             Decrypt initial message
```

**Code signals:** `identity_key`, `signed_prekey`, `one_time_prekey`,
`ephemeral_key`, `X3DH`, `triple_dh`, `prekey_bundle`.

### Double Ratchet Algorithm

**Parties:** Alice, Bob (symmetric, both have SK from X3DH)
**Purpose:** Forward-secret, break-in-recovery message encryption

```
Note over A,B: Initialize with SK from X3DH
               A has B's ratchet public key

A → B: Header(dh_ratchet_pk_A, prev_chain_len, msg_num)
       || Enc(message_key, plaintext)
Note over B: DH ratchet step: new root_key, new chain_key
             Derive message_key from chain_key
             Decrypt

B → A: Header(dh_ratchet_pk_B, prev_chain_len, msg_num)
       || Enc(message_key, plaintext)
Note over A: DH ratchet step: new root_key, new chain_key
             Derive message_key from chain_key
             Decrypt
```

**Code signals:** `root_key`, `chain_key`, `message_key`, `ratchet_key`,
`sending_chain`, `receiving_chain`, `skip_message_keys`, `MessageKey`.

---

## Diffie-Hellman Key Exchange (Classic / ECDH)

**Parties:** Alice (A), Bob (B)
**Round complexity:** 1 RTT

```
Note over A: a = random scalar; g_a = g^a (or a·G for ECDH)
A → B: g_a

Note over B: b = random scalar; g_b = g^b (or b·G for ECDH)
B → A: g_b

Note over A: shared = g_b^a = g^(ab)
Note over B: shared = g_a^b = g^(ab)
Note over A,B: session_key = KDF(shared)
```

**Authenticated DH:** add signatures or MACs over the transcript to bind
identities. Without authentication, this is vulnerable to MITM.

---

## Challenge-Response Authentication

**Variants:** HMAC-based, signature-based, password-based (PAKE)

### Signature-based

```
C → S: authenticate_request(identity)
S → C: challenge(nonce, session_id)
Note over C: σ = Sign(sk_C, nonce || session_id || identity)
C → S: response(σ, pk_C)
Note over S: Verify(pk_C, nonce || session_id || identity, σ)

alt verification succeeds
    S → C: session_token
else verification fails
    S → C: auth_failure
end
```

**Code signals:** `challenge`, `nonce`, `sign`, `verify`, `response`,
`session_token`, `authenticate`.

### HMAC-based (shared secret)

```
C → S: auth_request(identity)
S → C: challenge(nonce)
Note over C: mac = HMAC(shared_key, nonce || identity)
C → S: response(mac)
Note over S: expected = HMAC(shared_key, nonce || identity)
             ct_equal(mac, expected)
```

---

## Shamir Secret Sharing

**Parties:** Dealer (D), Parties P1…Pn, Combiner (C)
**Setup:** (t, n) threshold

```
Note over D: Split secret s into n shares using degree-(t-1) polynomial
             f(x) = s + a_1·x + … + a_{t-1}·x^{t-1}
             share_i = f(i) for i = 1..n

D → P1: Enc(pk_1, share_1)
D → P2: Enc(pk_2, share_2)
...
D → Pn: Enc(pk_n, share_n)

# (t-of-n parties agree to reconstruct)

P1 → C: share_1
P2 → C: share_2
...
Pt → C: share_t

Note over C: Lagrange interpolation on {(i, share_i)}
             → recover f(0) = s
```

**Code signals:** `split`, `share`, `combine`, `threshold`, `lagrange`,
`polynomial`, `evaluate`.

---

## Commit-Reveal

**Parties:** Committer (C), Verifier (V)
**Purpose:** Bind to a value without revealing it; reveal later

```
rect rgba(100, 149, 237, 0.15)
    Note over C,V: Phase 1: Commit
    Note over C: r = random nonce
                 commitment = H(value || r)
    C → V: commitment
end

rect rgba(46, 204, 113, 0.15)
    Note over C,V: Phase 2: Reveal
    C → V: value, r
    Note over V: Check H(value || r) == commitment
end

alt commitment matches
    Note over V: value accepted
else mismatch
    Note over V: ABORT — equivocation detected
end
```

**Code signals:** `commit`, `reveal`, `commitment`, `open`, `binding`,
`hiding`.

---

## Generic N-Party MPC (Round-Based)

**Parties:** P1, P2, …, Pn
**Structure:** Preprocessing + Online phases, or direct rounds

```
rect rgba(100, 149, 237, 0.15)
    Note over P1,P3: Round 0: Input Commitment
    Note over P1: share_1_j = Share(input_1, t, n) for j=1..n
    P1 ->> P2: share_1_2
    P1 ->> P3: share_1_3
    Note over P2: share_2_j = Share(input_2, t, n)
    P2 ->> P1: share_2_1
    P2 ->> P3: share_2_3
    Note over P3: share_3_j = Share(input_3, t, n)
    P3 ->> P1: share_3_1
    P3 ->> P2: share_3_2
end

rect rgba(46, 204, 113, 0.15)
    Note over P1,P3: Round 1: Local Computation
    Note over P1: result_share_1 = f(share_1_1, share_2_1, share_3_1)
    Note over P2: result_share_2 = f(share_1_2, share_2_2, share_3_2)
    Note over P3: result_share_3 = f(share_1_3, share_2_3, share_3_3)
end

rect rgba(155, 89, 182, 0.15)
    Note over P1,P3: Round 2: Output Reconstruction
    P1 ->> P2: result_share_1
    P1 ->> P3: result_share_1
    P2 ->> P1: result_share_2
    P2 ->> P3: result_share_2
    P3 ->> P1: result_share_3
    P3 ->> P2: result_share_3
    Note over P1: Combine(result_share_1, result_share_2, result_share_3) → output
    Note over P2: Combine(...) → output
    Note over P3: Combine(...) → output
end
```

**Broadcast channel:** In many MPC protocols, "send to all" is a broadcast.
Use `par` blocks or annotate with `Note over P1: broadcast to all`.

**Code signals:** `round`, `broadcast`, `send_share`, `recv_share`,
`local_computation`, `reconstruct`, `output`.

---

## Threshold Signature (FROST / GG20 pattern)

**Parties:** Signers S1…St (threshold-of-n), Aggregator (A)
**Setup:** n parties each hold a signing key share

```
rect rgba(100, 149, 237, 0.15)
    Note over A: Coordinator selects t signers, distributes message m
    A ->> S1: sign_request(m, participants=[S1..St])
    A ->> S2: sign_request(m, participants=[S1..St])
    A ->> St: sign_request(m, participants=[S1..St])
end

rect rgba(46, 204, 113, 0.15)
    Note over S1..St: Round 1: Nonce Generation
    Note over S1: (d_1, e_1) = random nonces; D_1=g^d_1, E_1=g^e_1
    S1 ->> A: (D_1, E_1)
    Note over S2: (d_2, e_2) = random nonces
    S2 ->> A: (D_2, E_2)
    Note over St: (d_t, e_t) = random nonces
    St ->> A: (D_t, E_t)
end

rect rgba(155, 89, 182, 0.15)
    Note over A: Aggregate binding factors, compute group commitment R
    A ->> S1: commitment_list = [(D_i, E_i) for i in participants]
    A ->> S2: commitment_list
    A ->> St: commitment_list
end

rect rgba(241, 196, 15, 0.15)
    Note over S1..St: Round 2: Partial Signatures
    Note over S1: z_1 = d_1 + e_1·ρ_1 + λ_1·sk_1·c (partial sig)
    S1 ->> A: z_1
    Note over S2: z_2 = d_2 + e_2·ρ_2 + λ_2·sk_2·c
    S2 ->> A: z_2
    Note over St: z_t = ...
    St ->> A: z_t
end

Note over A: σ = (R, z_1 + z_2 + ... + z_t) — final signature
Note over A: Verify(group_pk, m, σ)
```

**Code signals:** `partial_sign`, `aggregate`, `nonce`, `commitment`,
`binding_factor`, `lagrange_coefficient`, `group_key`, `threshold_sign`.

---

## Reading Hints: Identifying Protocol Patterns in Code

| Code pattern | Protocol signal |
|---|---|
| `send_msg` / `recv_msg` loop with round counter | Round-based MPC |
| Two `CipherState` after `split()` | Noise protocol completion |
| `transcript` accumulated via hash | TLS-style transcript MAC |
| `chain_key` / `root_key` updated per message | Double Ratchet |
| `verify_prekey_signature` | X3DH signal protocol |
| `lagrange` / `interpolate` | Shamir / threshold |
| `partial_sig` aggregated after broadcast | Threshold signature |
| `commitment = H(value || nonce)` followed by `open` | Commit-reveal |
| `challenge` sent, `Sign(sk, challenge)` response | Challenge-response |
| `g^a` sent, `g^b` received, `g^(ab)` computed | Classic DH |

## references/spec-parsing-patterns.md

# Spec Parsing Patterns Reference

Extraction rules for turning protocol specifications into sequence diagram
content. Covers four spec formats. Read the section matching your input.

---

## RFC Format

RFCs follow a predictable structure. Use it to locate the right content fast.

### Locating the protocol description

1. **Find the handshake section**: search for "handshake", "key exchange",
   "authentication", "message flow", or "overview" in section titles
2. **Find message definitions**: sections titled "Messages", "Record Layer",
   "Handshake Protocol", or numbered `X.Y` subsections for each message type
3. **Find ASCII diagrams**: many RFCs embed sequence diagrams in code blocks
   using `->` or `<-` arrows — use these as a starting point for message
   ordering. If an ASCII diagram and the normative prose conflict, the prose
   takes precedence — RFC ASCII diagrams are illustrative, not normative.

### Extracting parties

- Parties are usually named in the introduction or in a "Notation" / "Overview"
  section: look for "client", "server", "initiator", "responder"
- Role names in RFCs are typically lowercase (`client`, `server`) — capitalise
  them in the diagram

### Extracting message flow

Arrow patterns in RFC prose and ASCII diagrams:

```
Client                                           Server
  |                                                |
  |----------ClientHello------------------------->|
  |<---------ServerHello + {EncryptedExtensions}--|
```

Also watch for:
- "The client sends a X message containing ..."
- "Upon receiving X, the server MUST ..."
- "The handshake proceeds as follows:" followed by a numbered list

`MUST`/`SHALL` clauses describe required steps; `MAY`/`SHOULD` describe
optional ones (use `opt` blocks in the diagram).

### Extracting crypto operations

RFCs typically define crypto in a "Cryptographic Computations" or "Key
Schedule" section. Look for:
- `HKDF-Extract`, `HKDF-Expand`, `Derive-Secret` — key derivation
- `Sign(sk, transcript)`, `Verify(pk, transcript, sig)` — signatures
- Encryption notation: `{...}` braces around a message mean it is encrypted
  (TLS convention); note which key is used in the surrounding prose
- Transcript hash: running hash over all handshake messages — annotate as
  `H(handshake_transcript)` at the point it is finalised

### ABNF grammars

ABNF defines message structure, not flow. Use it to populate arrow labels:

```
ClientHello = ProtocolVersion random [SessionID] CipherSuites Extensions
```

→ Arrow label: `ClientHello(version, random, session_id, cipher_suites, extensions)`

---

## Academic Paper / Pseudocode

Papers vary widely, but protocol descriptions follow common conventions.

### Locating the protocol description

- Look for boxes or figures labelled "Protocol X", "Figure X: Protocol name",
  "Algorithm X"
- Section titles: "Protocol Description", "Construction", "Our Protocol",
  "The Scheme", "Formal Description"
- Some papers give an informal description first, then a formal pseudocode box —
  prefer the pseudocode box for message flow accuracy

### Extracting parties

- Header row of a protocol figure: `Alice | Bob`, `Client | Server`, `P | V`
- Pseudocode function names: `Client.KeyGen()`, `Server.Respond()`,
  `Prover.Commit()`, `Verifier.Challenge()`
- Subscripts in mathematical notation: `pk_A`, `sk_B` — `A` and `B` are parties

### Extracting message flow

**Two-column layouts** (most common):

```
Alice                    Bob
---                      ---
Compute x ← f(...)
Send x ──────────────►
                         Receive x
                         Compute y ← g(x, ...)
         ◄────────────── Send y
Receive y
```

Read left-to-right for Alice's column, right-to-left for Bob's. Arrows cross
the column boundary to indicate message sends.

**Numbered step lists**:

```
1. A generates (pk, sk) ← KeyGen(1^λ)
2. A sends pk to B
3. B computes c ← Enc(pk, m) and sends c to A
4. A decrypts m' ← Dec(sk, c)
```

Map step numbers to rounds. A step that says "X sends Y to Z" is a message
arrow. A step that says "X computes ..." is a `Note over X` annotation.

**Pseudocode with explicit send/receive**:

```
function Round1_Alice(sk_A, pk_B):
    ek, epk = DH.KeyGen()
    msg = epk
    send(Bob, msg)
    return ek

function Round1_Bob(pk_A):
    epk_A = recv(Alice)
    ...
```

Treat `send(Party, msg)` as a message arrow, `recv(Party)` as the receiving
end of the previous arrow.

### Mathematical notation quick-reference

| Notation | Meaning |
|----------|---------|
| `←` or `:=` | assignment / output of a computation |
| `←$` or `←_R` | sample uniformly at random |
| `→` or `\leftarrow` between parties | message send |
| `\{m\}_k` or `Enc_k(m)` | encryption of `m` under key `k` |
| `[m]_sk` or `Sign_{sk}(m)` | signature on `m` with key `sk` |
| `H(m)` | hash |
| `\pi` or `Π` | protocol |
| `\lambda` | security parameter |
| `\bot` | reject / abort |

---

## Informal Prose

Informal descriptions vary the most. Apply these heuristics systematically.

### Locating the description

- Section headings: "Protocol Overview", "How It Works", "Flow", "Steps"
- Numbered or bulleted lists of protocol steps
- Diagrams embedded as images (describe what you can infer; note you cannot
  read image content)

### Extracting parties

- Look for the first paragraph that names the participants: "Alice and Bob",
  "the client and the server", "the initiator and responder"
- Use the first two prominent nouns that interact: if the text says "the user
  authenticates to the service", parties are `User` and `Service`

### Extracting message flow — sentence patterns

Arrow syntax in the table below maps to Mermaid (`->>` solid, `-->>` dashed).

| Pattern | Arrow |
|---------|-------|
| "A sends [msg] to B" | `A->>B: msg` |
| "B receives [msg] from A" | `A->>B: msg` (same arrow, B's perspective) |
| "A transmits / delivers / forwards [msg]" | `A->>B: msg` (infer B from context) |
| "B responds with [msg]" | `B-->>A: msg` |
| "A and B exchange [msg]" | use two arrows if asymmetric, or `Note over A,B` if symmetric |
| "A computes / derives / generates [value]" | `Note over A: compute value` |
| "if [condition] then [action]" | `alt condition` block |
| "optionally, A sends [msg]" | `opt description` block |

### Handling vague crypto

If the prose says "encrypts" without specifying the scheme:
- Use `Enc(k, plaintext) → ct` in the note
- Add `⚠️ encryption scheme not specified in spec`

If the prose says "signs" without specifying the algorithm:
- Use `Sign(sk, msg) → σ`
- Add `⚠️ signature algorithm not specified`

---

## Formal Verification Models

### ProVerif (`.pv`)

ProVerif models processes, not a narrative sequence. Map process structure to
sequence diagram steps.

**Key constructs:**

```proverif
(* Channel declaration *)
free c: channel.                    (* public channel *)
free s: channel [private].          (* private / secure channel *)

(* Free names — constants known to attacker if not private *)
free pk_A: bitstring.

(* Process definition *)
let ClientProc(sk: bitstring, pk_S: bitstring) =
    new nonce: bitstring;           (* fresh random — Note over Client: nonce ← rand *)
    out(c, nonce);                  (* send on channel c → arrow to Server *)
    in(c, resp: bitstring);         (* receive on channel c → arrow from Server *)
    let (m1, sig) = resp in
    if verify(m1, sig, pk_S) then  (* conditional — alt block *)
        ...
    else 0.                         (* abort path *)

(* Main process — composition of roles *)
process
    ( !ClientProc(sk_A, pk_S) | !ServerProc(sk_S, pk_A) )
```

**Extraction rules:**

| Construct | Diagram element |
|-----------|----------------|
| `let ProcName(params) =` | Defines a role; `ProcName` → participant |
| `new x: t` | `Note over Party: x ← fresh()` |
| `out(ch, msg)` | Arrow from this process to the process that `in`s on same `ch` |
| `in(ch, x)` | Receiving end of the matching `out` |
| `if cond then P else Q` | `alt cond` / `else` block |
| `let (a, b) = msg` | Destructuring — local computation, `Note over Party` |
| `!P` | Replication — this role handles multiple sessions; use `loop` annotation |
| `senc(m, k)` / `sdec(c, k)` | Symmetric enc/dec |
| `aenc(m, pk)` / `adec(c, sk)` | Asymmetric enc/dec |
| `sign(m, sk)` / `verify(m, sig, pk)` | Sign / verify |
| `hash(m)` | Hash |
| `pk(sk)` | Public key derivation — `Note over Party: pk = pk(sk)` |

**Channel matching:** Pair each `out(ch, msg)` with the `in(ch, x)` in another
process on the same channel. The sending process owns the arrow's tail; the
receiving process owns the arrow's head.

**Private channels** (`[private]` or declared with `new c`): represent
out-of-band communication — annotate: `Note over A,B: via private channel`.

**`phase N` construct:** ProVerif's `phase N` keyword sequences protocol steps
that cannot execute concurrently. Steps in phase N execute only after all phase
N-1 processes have terminated. If a model uses `phase`, use the phase numbers
to order the diagram: steps in phase 0 come before steps in phase 1, and so on.
Annotate phase boundaries: `Note over A,B: --- phase N begins ---`.

**Queries** (`query attacker(x)`, `query event(...)`) are security properties,
not protocol steps — omit from the diagram but mention in the Protocol Summary.

### Tamarin (`.spthy`)

**Important — Dolev-Yao attacker model:** Tamarin does not model direct
peer-to-peer channels. Every `Out(m)` delivers to the attacker network, and
every `In(m)` can be satisfied by any message the attacker knows (including
forwarded or replayed messages). For the diagram, treat `Out(m)` in one rule
and `In(m)` in another as a logical A→B message, but always add this note on
the diagram:

```
Note over A,B: ⚠️ Tamarin uses Dolev-Yao model — all messages transit adversary network
```

Tamarin models rules that fire when their premises are satisfied. Map rule
ordering to protocol steps.

**Key constructs:**

```tamarin
rule Register_pk:
    [ Fr(~sk) ]                     (* fresh secret key generated *)
  --[ Register($A, pk(~sk)) ]->    (* security annotation — not a message *)
    [ !Ltk($A, ~sk)                 (* persistent fact — stored state *)
    , !Pk($A, pk(~sk))              (* persistent fact — public key *)
    , Out(pk(~sk)) ]                (* send public key to network *)

rule Client_Send:
    [ Fr(~n)                        (* fresh nonce *)
    , !Pk($S, pk_S) ]               (* lookup server's public key *)
  --[ Send($C, $S, ~n) ]->
    [ St_Client_1($C, $S, ~n)       (* client state after round 1 *)
    , Out(aenc(~n, pk_S)) ]         (* send encrypted nonce *)

rule Server_Recv:
    [ In(aenc(n, pk(~sk)))          (* receive encrypted nonce *)
    , !Ltk($S, ~sk) ]               (* lookup server's secret key *)
  --[ Recv($S, n) ]->
    [ Out(n) ]                      (* echo decrypted nonce *)
```

**Extraction rules:**

| Construct | Diagram element |
|-----------|----------------|
| `Fr(~x)` in premise | `Note over Party: x ← fresh()` |
| `In(m)` in premise | Receive arrow — find matching `Out(m)` rule for sender |
| `Out(m)` in conclusion | Send arrow to network / other party |
| `!Fact($A, ...)` | Persistent state lookup — not a message |
| `St_Role_N(...)` | State fact — marks which round the party is in |
| `--[ Label ]->` | Security event annotation — omit from diagram |
| `$A` (public name) | Party / principal |
| `~x` (fresh name) | Freshly generated secret |
| `#i` (timepoint) | Ordering hint — earlier timepoint = earlier in diagram |

**Rule ordering:** Reconstruct order by following state facts: `St_Role_N`
consumed by a rule → `St_Role_{N+1}` produced → next rule for that role.