crypto-protocol-diagram — independently scanned and version-tracked by SaferSkills.
SaferSkills independently audited crypto-protocol-diagram (Agent Skill) and scored it 100/100 (green). The audit ran 55 deterministic rules across Security, Supply Chain, Maintenance, Transparency, and Community; it found 0 high-severity and 0 lower-severity findings. The full rule-by-rule trace and per-finding evidence are below. Free, methodology-open.
Findings & checks · 0 flagged
Every scanned point with the score it earned and what moved between them.
First recorded scan — no prior version to compare against.
The primary manifest — the file an agent reads to learn what this artifact does.
Produces a Mermaid sequenceDiagram (written to file) and an ASCII sequence diagram (printed inline) from either:
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.
diagramming-codemermaid-to-proverif (after generating the diagram)| 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 |
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 deliverBefore 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 ⚠️) |
the implementation against the spec diagram and annotate any divergences with ⚠️
document, or both?"
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.
Extract participant names from:
Client, Server, Initiator, Responder, Prover,Verifier, Dealer, Party, Coordinator
Map these to Mermaid participant declarations. Use short, readable aliases:
participant I as Initiator
participant R as ResponderFollow 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.
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.
Group message steps into named phases using rect or Note blocks:
Common phases to detect:
Detect abort/error paths and show them with alt blocks.
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.
Obtain the full spec text:
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.
Identify all protocol participants. Look for:
Alice, Bob, Client, Server,Initiator, Responder, Prover, Verifier, Dealer, Party_i, Coordinator, Signer
let ClientProc(...), let ServerProc(...))!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).
Trace what each party sends to whom and in what order. Extraction patterns by format:
RFC / informal prose:
A → B: msg, A -> B"upon receiving X, B sends Y"
Pseudocode:
sender/receiver parameterssend(party, msg) / receive(party) callsProVerif (`.pv`):
out(ch, msg) — send on channel chin(ch, x) — receive on channel ch, bind to xout/in pairs on the same channel to identify message flows! (replication) signals a role that handles multiple sessionsTamarin (`.spthy`):
In(m) premise — receive message mOut(m) conclusion — send message mFr(~x) — fresh random value generated by a party--[ Label ]-> facts — security annotations, not messagesPreserve the ordering and round structure. Group concurrent sends (broadcast) using par blocks in the final diagram.
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:
assert, require, if ... abortif m = expected then ... else 0These become alt blocks in the final diagram.
Before moving to Step 6, check for gaps:
annotate with ⚠️ ordering inferred from spec structure
descriptive name and note the inference
this protocol requires, annotate: ⚠️ spec omits [step] — canonical protocol requires it
the scheme, annotate: ⚠️ encryption scheme not specified
c declared with new c or as aprivate free name) represent out-of-band channels — note them
<!-- Both code path (Steps 1–5) and spec path (Steps S1–S5) continue here -->
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 itBefore delivering:
alt blocks cover known abort/error pathsreferences/mermaid-sequence-syntax.md for common pitfalls)
⚠️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.
── 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.mdCode path — examples/simple-handshake/:
Ed25519 signing + HKDF + ChaCha20-Poly1305)
should produce for that protocol
Spec path (ProVerif) — examples/simple-proverif/:
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.
Extraction rules for RFC, academic paper/pseudocode, informal prose, ProVerif, and Tamarin input formats; read during Step S1
Participant syntax, arrow types, activations, grouping blocks, escaping rules, and common rendering pitfalls
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
Column layout, arrow conventions, self-loops, phase labels, and inline output format for the ASCII diagram
~30 seconds. Free. No account. Every finding cites a rule and a line of evidence.