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.
Detected risks:
Crypto Protocol Diagram extracts the message flow of a cryptographic protocol and produces a Mermaid sequenceDiagram (written to a file) plus an ASCII sequence diagram (printed inline). It accepts two kinds of input: source code implementing a protocol, or a specification such as an RFC, academic paper, pseudocode, informal prose, a ProVerif (.pv) model, or a Tamarin (.spthy) model. 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. It is suited to diagramming handshakes and key exchanges and to named protocols like TLS, Noise, Signal, X3DH, Double Ratchet, FROST, DH, and ECDH.
Use it when asked to diagram, visualize, or extract a cryptographic protocol from code, a spec, or a formal model. It should not be used for call graphs, class hierarchies, or module dependency maps (use diagramming-code), for formal verification (use mermaid-to-proverif after generating the diagram), or for input that has no protocol semantics. The skill enforces discipline against shortcuts: it rejects diagramming from memory, requires annotating every cryptographic operation, requires showing every abort and error path with alt blocks, and treats ProVerif and Tamarin models as specifications rather than code.
The workflow starts at Step 0 by classifying the input as code, spec, or both using a signal table (file extensions and imports indicate code; RFC headers, algorithm labels, ProVerif process/let/in/out, or Tamarin rule/--[...]-> indicate spec). Code input proceeds through locating protocol entry points with ripgrep, identifying parties and roles, tracing message flow (including treating in-process function-call boundaries as logical sends), annotating cryptographic operations such as keygen, DH/ECDH, KDF/HKDF, signing, verification, encryption, decryption, commitment, hashing, and secret sharing, and grouping steps into named phases like setup, handshake, authentication, key derivation, data transfer, and finalization. Specification input follows a parallel S1–S5 path; when both code and a spec exist, the spec workflow runs first and code is used to verify and annotate divergences. Both paths converge on generating the sequenceDiagram and verifying and delivering it.
It accepts source code implementing a protocol, and specifications including RFCs, academic papers, pseudocode, informal prose, ProVerif (.pv) models, and Tamarin (.spthy) models.
It produces a Mermaid sequenceDiagram written to a file and an ASCII sequence diagram printed inline, capturing who sends what to whom and the cryptographic operations at each step.
diagramming-code visualizes code structure such as call graphs, class hierarchies, and module dependencies. This skill instead extracts protocol semantics — parties, message exchanges, cryptographic transformations, and protocol phases.
Yes. When both exist, the spec workflow (S1–S5) runs first to build the diagram, then the code-reading steps verify the implementation against it and annotate any divergences with a warning marker.
Use the mermaid-to-proverif skill after generating the diagram. This skill itself does not perform formal verification.
Quick Setup:
.claude/skills/Repository
trailofbits/skills