crypto-protocol-diagram

Files (11)

• SKILL.md
• openai.yaml · agents/
• trail-of-bits-mark.svg · assets/
• expected-output.md · examples/simple-handshake/
• protocol.py · examples/simple-handshake/
• expected-output.md · examples/simple-proverif/
• model.pv · examples/simple-proverif/
• ascii-sequence-diagram.md · references/
• mermaid-sequence-syntax.md · references/
• protocol-patterns.md · references/
• spec-parsing-patterns.md · references/

SKILL.md (first lines)

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

From trailofbits/skills, CC-BY-SA-4.0.

More from trailofbits/skills