interface:
  display_name: "Crypto Protocol Diagrams"
  short_description: "Diagram cryptographic protocols and message flows"
  icon_small: "assets/trail-of-bits-mark.svg"
  icon_large: "assets/trail-of-bits-mark.svg"
  brand_color: "#D83A34"

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

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

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

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