Crypto Protocol Diagram
Trail of BitsOfficialPublished by Trail of Bits
- Skill
- Content generator
- Security
- CC-BY-SA-4.0
- Low risk
- Has scripts
AutoGineer summary
Written by AutoGineer from the skill’s own files, not by the author
This skill extracts the semantic message flow and cryptographic operations of a protocol from various inputs, including source code, RFCs, academic papers, and formal models like ProVerif or Tamarin. It produces both a Mermaid sequence diagram file and an inline ASCII representation, ensuring that cryptographic transformations and protocol phases are clearly annotated for security review.
What it does
- Parses source code, RFCs, papers, and formal models to extract protocol structure.
- Identifies protocol participants and maps them to sequence diagram roles.
- Traces message flows and cryptographic operations like DH, signing, and KDF.
- Groups protocol steps into logical phases using visual blocks.
- Generates a Mermaid sequence diagram file with cryptographic annotations.
- Provides an inline ASCII sequence diagram for quick reference.
When to use it
- When you need to visualize a cryptographic handshake or key exchange flow.
- When auditing a protocol implementation against its specification.
- When documenting a protocol from an RFC, academic paper, or formal model.
- When you need to identify divergences between code and specification.
Advantages
- Ensures protocol semantics are captured rather than just code structure.
- Highlights cryptographic operations at each step for easier security analysis.
- Supports both formal models and informal prose as input sources.
- Provides standardized visual output for consistent documentation.
Usage examples
- “Diagram the handshake flow from this TLS 1.3 implementation.”
- The agent analyzes the provided source code, extracts the handshake message sequence, annotates the key exchange and signing operations, and outputs a Mermaid file and ASCII diagram.
- “Create a sequence diagram for the X3DH protocol based on this specification.”
- The agent reads the provided spec, identifies the participants (Alice, Bob, Server), maps the message flow, and generates a diagram showing the key bundle exchange and DH operations.
Install
Download the skill as a ZIP:
https://autogineer.com/agent-skills/trailofbits/crypto-protocol-diagram/downloadUnzip it into the cross-client skills folder of your project:
mkdir -p .agents/skills && unzip crypto-protocol-diagram.zip -d .agents/skills
Documentation by Trail of Bits
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-codeUser 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 deliverStep 0: Determine Input Type
Before doing anything else, classify the input:
| Signal | Input type |
|---|---|
Source file extensions (.py, .rs, .go, .ts, .js, .cpp, .c) | Code |
| Function/class definitions, import statements | Code |
RFC-style section headers (§, Section X.Y, MUST/SHALL keywords) | Spec |
Algorithm/Protocol/Figure labels, mathematical notation | Spec |
ProVerif file (.pv) with process, let, in/out | Spec |
Tamarin file (.spthy) with rule, --[...]-> | Spec |
| Plain prose or numbered steps describing a protocol | Spec |
| Both source files and a spec document | Both (annotate divergences with ⚠️) |
Code only → skip to Step 1 below
Spec only → skip to Spec Workflow (S1–S5) below
Both → run Spec Workflow first, then use the code-reading steps to verify the implementation against the spec diagram and annotate any divergences with
⚠️Ambiguous → ask the user: "Is this a source code file, a specification document, or both?"
Step 1: Locate Protocol Entry Points
Grep for function names, type names, and comments that reveal the protocol:
# Find handshake, session, round, phase entry points
rg -l "handshake|session_init|round[_0-9]|setup|keygen|send_msg|recv_msg" {targetDir}
# Find crypto primitives in use
rg "sign|verify|encrypt|decrypt|dh|ecdh|kdf|hkdf|hmac|hash|commit|reveal|share" \
{targetDir} --type-add 'src:*.{py,rs,go,ts,js,cpp,c}' -t src -lStart 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,CoordinatorFunction 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 ResponderStep 3: Trace Message Flow
Follow state transitions and network sends/receives. Look for patterns like:
| Pattern | Meaning |
|---|---|
send(msg) / recv() | Direct message exchange |
serialize + transmit | Structured message sent |
| Return value passed to other party's function | Logical message (in-process) |
round1_output → round2_input | Round-based MPC step |
Struct fields named ephemeral_key, ciphertext, mac, tag | Message contents |
For in-process protocol implementations (where both parties run in the same process), treat function call boundaries as logical message sends when they represent what would be a network boundary in deployment.
Step 4: Annotate Cryptographic Operations
At each protocol step, identify and label:
| Operation | Diagram annotation |
|---|---|
| Key generation | Note over A: keygen(params) → pk, sk |
| DH / ECDH | Note over A,B: DH(sk_A, pk_B) |
| KDF / HKDF | Note over A: HKDF(ikm, salt, info) |
| Signing | Note over A: Sign(sk, msg) → σ |
| Verification | Note over B: Verify(pk, msg, σ) |
| Encryption | Note over A: Enc(key, plaintext) → ct |
| Decryption | Note over B: Dec(key, ct) → plaintext |
| Commitment | Note over A: Commit(value, rand) → C |
| Hash | Note over A: H(data) → digest |
| Secret sharing | Note over D: Share(secret, t, n) → {s_i} |
| Threshold combine | Note over C: Combine({s_i}) → secret |
Keep annotations concise — use mathematical shorthand, not code.
Step 5: Identify Protocol Phases
Group message steps into named phases using rect or Note blocks:
Common phases to detect:
Setup / Key Generation: party key creation, trusted setup, parameter gen
Handshake / Init: ephemeral key exchange, nonce exchange, version negotiation
Authentication: identity proof, certificate exchange, signature verification
Key Derivation: session key derivation from shared secrets
Data Transfer / Main Protocol: encrypted application data exchange
Finalization / Teardown: session close, MAC verification, abort handling
Detect abort/error paths and show them with alt blocks.
Spec Workflow (S1–S5)
Use this path when the input is a specification document rather than source code. After completing S1–S5, continue with Step 6 (Generate sequenceDiagram) and Step 7 (Verify and deliver) from the code workflow above.
Step S1: Ingest the Spec
Obtain the full spec text:
File path provided → read with the Read tool
URL provided → fetch with WebFetch
Pasted inline → work directly from conversation context
Then identify the spec format and read references/spec-parsing-patterns.md for format-specific extraction guidance:
| Format | Signals |
|---|---|
| RFC | RFC XXXX, MUST/SHALL/SHOULD, ABNF grammars, section-numbered prose |
| Academic paper / pseudocode | Algorithm X, Protocol X, Figure X, numbered steps, ←/→ in math mode |
| Informal prose | Numbered lists, "A sends B ...", plain English descriptions |
ProVerif (.pv) | process, let, in(ch, x), out(ch, msg), ! (replication) |
Tamarin (.spthy) | rule, --[ ]->, Fr(~x), !Pk(A, pk), In(m), Out(m) |
If the spec references a known named protocol (TLS, Noise, Signal, X3DH, Double Ratchet, FROST), also read references/protocol-patterns.md to use its canonical flow as a skeleton and fill in spec-specific details.
Step S2: Extract Parties and Roles
Identify all protocol participants. Look for:
Named roles in prose or pseudocode:
Alice,Bob,Client,Server,Initiator,Responder,Prover,Verifier,Dealer,Party_i,Coordinator,SignerSection 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)—$Ais a party)
Map each role to a Mermaid participant declaration. Use short IDs with
descriptive aliases (see naming conventions in
references/mermaid-sequence-syntax.md).
Step S3: Extract Message Flow
Trace what each party sends to whom and in what order. Extraction patterns by format:
RFC / informal prose:
Arrow notation:
A → B: msg,A -> BSentence 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/receiverparameterssend(party, msg)/receive(party)callsReturn values passed as inputs to the other party's function in the next step
ProVerif (.pv):
out(ch, msg)— send on channelchin(ch, x)— receive on channelch, bind toxMatch
out/inpairs on the same channel to identify message flows!(replication) signals a role that handles multiple sessions
Tamarin (.spthy):
In(m)premise — receive messagemOut(m)conclusion — send messagemRule 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 ... abortProVerif:
if m = expected then ... else 0Tamarin: 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 structureImplied 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 itUnderspecified crypto: if the spec says "encrypt" without specifying the scheme, annotate:
⚠️ encryption scheme not specifiedProVerif/Tamarin: private channels (
cdeclared withnew cor as a private free name) represent out-of-band channels — note them
<!-- Both code path (Steps 1–5) and spec path (Steps S1–S5) continue here -->
Step 6: Generate sequenceDiagram
Produce Mermaid syntax following the rules in references/mermaid-sequence-syntax.md.
Completeness over brevity. Show every distinct message type. Omit repeated
loop iterations (use loop blocks instead), but never omit a distinct protocol
step.
Correctness over aesthetics. The diagram must match what the code actually does. If the code diverges from a known spec, annotate the divergence:
Note over A,B: ⚠️ spec requires MAC here — implementation omits itStep 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
[ ]
altblocks cover known abort/error paths[ ] Diagram renders without syntax errors (check references/mermaid-sequence-syntax.md for common pitfalls)
[ ] If spec divergence found, annotated with
⚠️
Write the diagram to a file. Choose a filename derived from the protocol
name, e.g. noise-xx-handshake.md or x3dh-key-agreement.md. Write a
Markdown file with this structure:
# <Protocol Name> Sequence Diagram
\`\`\`mermaid
sequenceDiagram
...
\`\`\`
## Protocol Summary
- **Parties:** ...
- **Round complexity:** ...
- **Key primitives:** ...
- **Authentication:** ...
- **Forward secrecy:** ...
- **Notable:** [spec deviations or security observations, or "none"]After writing the file, print an ASCII sequence diagram inline in the response, followed by the Protocol Summary. State the output filename so the user knows where to find the Mermaid source.
Follow all drawing conventions in references/ascii-sequence-diagram.md, including the inline output format.
Decision Tree
── Input is a spec document (not code)?
│ └─ Step S1: identify format, read references/spec-parsing-patterns.md
│
── Input is source code (not a spec)?
│ └─ Step 1: grep for handshake/round/send/recv entry points
│
── Both spec and code provided?
│ └─ Run Spec Workflow (S1–S5) first to build canonical diagram,
│ then read code and annotate divergences with ⚠️
│
── Spec is a known protocol (TLS, Noise, Signal, X3DH, FROST)?
│ └─ Read references/protocol-patterns.md and use canonical flow as skeleton
│
── Spec is ProVerif (.pv) or Tamarin (.spthy)?
│ └─ Read references/spec-parsing-patterns.md → Formal Models section
│
── Spec message ordering is ambiguous?
│ └─ Infer from round/section structure, annotate with ⚠️
│
── Can't identify parties from spec?
│ └─ Check "Parties"/"Notation" sections; for ProVerif read process names;
│ for Tamarin read rule names and fact arguments
│
── Don't know which code files implement the protocol?
│ └─ Step 1: grep for handshake/round/send/recv entry points
│
── Can't identify parties from struct names?
│ └─ Read test files — test setup reveals roles
│
── Protocol runs in-process (no network calls)?
│ └─ Treat function argument passing at role boundaries as messages
│
── MPC / threshold protocol with N parties?
│ └─ Read references/protocol-patterns.md → MPC section
│
── Mermaid syntax error?
│ └─ Read references/mermaid-sequence-syntax.md → Common Pitfalls
│
└─ ASCII drawing conventions?
└─ Read references/ascii-sequence-diagram.mdExamples
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 ProVerifexpected-output.md— step-by-step extraction walkthrough (parties, message flow, crypto ops) and the exact ASCII diagram and Mermaid file the skill should produce
Study the relevant example before working on an unfamiliar input.
Supporting Documentation
references/spec-parsing-patterns.md — Extraction rules for RFC, academic paper/pseudocode, informal prose, ProVerif, and Tamarin input formats; read during Step S1
references/mermaid-sequence-syntax.md — Participant syntax, arrow types, activations, grouping blocks, escaping rules, and common rendering pitfalls
references/protocol-patterns.md — Canonical message flows for TLS 1.3, Noise, X3DH, Double Ratchet, Shamir secret sharing, commit-reveal, and generic MPC rounds; use as a reference when comparing implementation against spec
references/ascii-sequence-diagram.md — Column layout, arrow conventions, self-loops, phase labels, and inline output format for the ASCII diagram
Files
- ATTRIBUTION.mdAdded by AutoGineer949 B
- LICENSELicence file added by AutoGineer19.7 KiB
- SKILL.md18.4 KiB
- agents/openai.yaml244 B
- assets/trail-of-bits-mark.svg3.0 KiB
- examples/simple-handshake/expected-output.md4.8 KiB
- examples/simple-handshake/protocol.pyScript5.7 KiB
- examples/simple-proverif/expected-output.md4.0 KiB
- examples/simple-proverif/model.pv1.8 KiB
- references/ascii-sequence-diagram.md2.3 KiB
- references/mermaid-sequence-syntax.md7.5 KiB
- references/protocol-patterns.md10.9 KiB
- references/spec-parsing-patterns.md11.6 KiB
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
Find the handshake section: search for "handshake", "key exchange", "authentication", "message flow", or "overview" in section titles
Find message definitions: sections titled "Messages", "Record Layer", "Handshake Protocol", or numbered
X.Ysubsections for each message typeFind 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 derivationSign(sk, transcript),Verify(pk, transcript, sig)— signaturesEncryption notation:
{...}braces around a message mean it is encrypted (TLS convention); note which key is used in the surrounding proseTranscript 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 | VPseudocode function names:
Client.KeyGen(),Server.Respond(),Prover.Commit(),Verifier.Challenge()Subscripts in mathematical notation:
pk_A,sk_B—AandBare 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 yRead 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
UserandService
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) → ctin the noteAdd
⚠️ 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:
(* 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 ins 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 networkTamarin models rules that fire when their premises are satisfied. Map rule ordering to protocol steps.
Key constructs:
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.
Requirements and compatibility
Written for: Claude Code
Works with: Claude Code, Claude apps, OpenAI Codex, GitHub Copilot, Cursor, Gemini CLI, Kiro, OpenCode, Goose, Amp, Roo Code, JetBrains Junie, Factory Droid, Devin (ex-Windsurf), Mistral Vibe, OpenHands, Letta
“Works with” means the tool reads the open Agent Skills format; a skill written for one tool may use features others lack.
Needs: Names Claude Code tools, Needs Python
Security
What our scanner noticed· Low risk
- Scripts that your agent may run
This skill includes scripts that your agent may run. Read them before you use it.
A static scan is not a guarantee. Skills are third-party content: review a skill before you let an agent use it.
Attribution and licence
- Published by
- Trail of Bits
- Publisher
- Trail of Bits (Official)
- Source
- trailofbits/skills · plugins/trailmark/skills/crypto-protocol-diagram · commit e4dd0bb
- Licence
- Creative Commons Attribution-ShareAlike 4.0 International (redistribution allowed)
- LICENSE (added by AutoGineer from LICENSE)
- ATTRIBUTION.md (written by AutoGineer)
- Synced
AutoGineer is not affiliated with or endorsed by Trail of Bits or Trail of Bits.
Download ZIP
The ZIP holds the skill’s files, its licence files and an ATTRIBUTION.md. Download crypto-protocol-diagram.zip