Documentation / Protocol studies and examples

Protocol studies and examples

Follow complete analyses, change one assumption at a time, and run all 33 teaching models yourself.

Three protocol studies

The Signal protocol

Classical X3DH, three Double Ratchet messages, and a later identity-key disclosure. Remove checks and trust assumptions to see which message properties depend on them.
The Scuttlebutt handshake

A simplified model explores identity hiding, ciphertexts accepted in the wrong protocol position, network membership and agreement across sessions.
Post-quantum protocol analysis

A PQXDH-inspired model exposes key-role confusion, repairs it with domain separation and tests what survives compromise of either hybrid component.

Each study states its simplifications. Its findings describe those models and the selected queries; use the protocol’s actual checks, encodings and compromise assumptions when applying the lesson.

Small experiments

Begin with the guided experiments, or choose a complete model below. Each download can be run on its own.

Compare the result codes at one and two sessions. Open a model in the Workbench to inspect its two-session trace.

Runnable models, including every documented variant
Model and purpose	One session	Two sessions
first.vp A substituted verification key accepts an attacker signature without revealing Alice's key. Open in Workbench →	`c0a1`	`c0a1`
first-guarded.vp The trusted signing key and checked signature bind Bob's challenge to Alice. Open in Workbench →	`c0a0`	`c0a0`
first-unchecked.vp Bob uses the delivered signature without requiring successful verification. Open in Workbench →	`c0a1`	`c0a1`
simple.vp Unauthenticated Diffie-Hellman permits key substitution, disclosure and divergence. Open in Workbench →	`c1c1a1e1`	`c1c1a1e1`
simple-passive.vp Only the transmitted ciphertext is public; a passive attacker cannot substitute the keys. Open in Workbench →	`c1c0a0e0`	`c1c0a0e0`
freshness.vp The used static hash is not fresh; the used generated-value hash is fresh. Open in Workbench →	`f1f0`	`f1f0`
unlinkability.vp The hidden seed stays unknown, while a leaked common origin and repeated public key link the other pairs. Open in Workbench →	`u0u1u1`	`u0u1u1`
accepted-key.vp A discarded key can be attacker-known; the precondition excludes a run that fails verification before sending. Open in Workbench →	`c1c0`	`c1c0`
challenge-response.vp Unchecked verification permits replacement, and a second session permits replay of the independent attestation. Open in Workbench →	`a1a0`	`a1a1`
threshold.vp Authenticated coordinator messages prevent collecting partials for an attacker-selected message. Open in Workbench → Read the model	`c0c0a0`	`c0c0a0`
nonce-reuse.vp The reused pair reveals its plaintexts, while the different-nonce plaintext remains protected. Open in Workbench → Read the model	`c1c1c0`	`c1c1c0`
nonce-forgery.vp Two distinct ciphertexts under one key and nonce permit a forged ciphertext. Open in Workbench → Read the model	`a1`	`a1`
harvest.vp Only the annotated ciphertext loses confidentiality in phase 2. Open in Workbench → Read the model	`c0c1`	`c0c1`
precondition.vp The second session supplies an accepted replay that still reaches the onward send. Open in Workbench →	`a0`	`a1`
challenge-checked.vp Checking a signature does not establish trust in an unguarded verification key. Open in Workbench →	`a1a0`	`a1a1`
challenge-guarded.vp The challenge proof is protected, but the attestation can still be replayed to another server run. Open in Workbench →	`a0a0`	`a0a1`
scenarios.vp Lowe's attack spans an honest and a corrupt peer configuration. Open in Workbench →	`c1a1a0`	`c1a1a0`

Explore a small model

Two-of-three threshold signing

A trusted dealer distributes two encrypted shares; two signers exchange commitments and a coordinator joins their partial signatures. This model omits partial-signature validation and key erasure. Remove the guards on the coordinator’s second-round deliveries to test signing an attacker-chosen message.

attacker[active]

principal Dealer[
	knows private psk_a, psk_b
	generates k, nd_a, nd_b
	pk = PUBKEY(k)
	s1, s2, s3 = THRESHOLD_SPLIT[2](k)
	ea = AEAD_ENC(psk_a, nd_a, s1, pk)
	eb = AEAD_ENC(psk_b, nd_b, s2, pk)
]

Dealer -> Alice: [pk], nd_a, ea

Dealer -> Bob: [pk], nd_b, eb

Dealer -> Coordinator: [pk]

Dealer -> Verifier: [pk]

principal Alice[
	knows private psk_a
	sa = AEAD_DEC(psk_a, nd_a, ea, pk)?
	generates na
	ca = PUBKEY(na)
]

principal Bob[
	knows private psk_b
	sb = AEAD_DEC(psk_b, nd_b, eb, pk)?
	generates nb
	cb = PUBKEY(nb)
]

Alice -> Coordinator: ca

Bob -> Coordinator: cb

principal Coordinator[
	generates m
]

Coordinator -> Alice: [m], [cb]

Coordinator -> Bob: [m], [ca]

principal Alice[
	cl_a = CONCAT(ca, cb)
	pa = THRESHOLD_SIGN(sa, na, cl_a, m)
]

principal Bob[
	cl_b = CONCAT(ca, cb)
	pb = THRESHOLD_SIGN(sb, nb, cl_b, m)
]

Alice -> Coordinator: pa

Bob -> Coordinator: pb

principal Coordinator[
	sig = THRESHOLD_JOIN(pa, pb)
	_ = SIGNVERIF(pk, m, sig)?
]

Coordinator -> Verifier: m, sig

principal Verifier[
	_ = SIGNVERIF(pk, m, sig)?
]

queries[
	confidentiality? k
	confidentiality? s1
	authentication? Coordinator -> Verifier: sig
]

Plaintext disclosure from nonce reuse

Compare the two ciphertexts sharing n1 with the third ciphertext under n2. The attacker only observes traffic.

attacker[passive]

principal Alice[
	knows private k
	knows private n1, n2
	knows private m1, m2, m3
	knows public ad
	e1 = AEAD_ENC(k, n1, m1, ad)
	e2 = AEAD_ENC(k, n1, m2, ad)
	e3 = AEAD_ENC(k, n2, m3, ad)
]

Alice -> Bob: e1, e2, e3

principal Bob[
	knows private k
	knows private n1, n2
	knows public ad
	d1 = AEAD_DEC(k, n1, e1, ad)?
	d2 = AEAD_DEC(k, n1, e2, ad)?
	d3 = AEAD_DEC(k, n2, e3, ad)?
]

queries[
	confidentiality? m1
	confidentiality? m2
	confidentiality? m3
]

Forgery from nonce reuse

The third ciphertext uses different associated data, ruling out substitution of either earlier honest ciphertext. Inspect how the attacker instead constructs one that Bob accepts.

attacker[active]

principal Alice[
	knows private k
	knows private n
	knows public ad1, ad2
	generates m1, m2, m3
	e1 = AEAD_ENC(k, n, m1, ad1)
	e2 = AEAD_ENC(k, n, m2, ad1)
	e3 = AEAD_ENC(k, n, m3, ad2)
]

Alice -> Bob: e1, e2, e3

principal Bob[
	knows private k
	knows private n
	knows public ad1, ad2
	d = AEAD_DEC(k, n, e3, ad2)?
	r = HASH(d)
]

queries[
	authentication? Alice -> Bob: e3
]

Harvest now, decrypt later

Only e_later carries a weakening annotation. Inspect when its plaintext becomes available and compare it with m_now.

attacker[passive]

principal Alice[
	knows private k, m_now, m_later
	generates n_now, n_later
	e_now = AEAD_ENC(k, n_now, m_now, nil)
	e_later = AEAD_ENC[weak from phase 2](k, n_later, m_later, nil)
]

Alice -> Bob: n_now, e_now, n_later, e_later

principal Bob[
	_ = HASH(e_now, e_later)
]

phase[1]

phase[2]

queries[
	confidentiality? m_now
	confidentiality? m_later
]

Reproducing the examples

Download a model and run verifpal verify model.vp --sessions 2. The command-line guide covers exporting and preserving reports. Trace excerpts in the studies omit routine progress and may abbreviate terms; another run may choose a different witness.

The example manifest records the expected codes and the edits defining each variant. The checking instructions explain how to verify the full collection against the bundled browser engine or an installed verifier.

Three protocol studies

The Signal protocol

The Scuttlebutt handshake

Post-quantum protocol analysis

Small experiments

Explore a small model

Reproducing the examples