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 explains what its model simplifies. Before applying a finding to an implementation, compare its checks, encodings and compromise assumptions with the model.

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 Bob accepts the attacker’s signature after a key substitution, while Alice’s private key stays secret. 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 Without authenticated public keys, Diffie–Hellman lets the attacker substitute keys, read the message and make the peers derive different secrets. 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 A hash of a static key fails the freshness query; a hash containing a generated value passes. Open in Workbench →	`f1f0`	`f1f0`
unlinkability.vp The attacker cannot link hashes of a secret seed, but can link values with a leaked common origin or an identical public key. Open in Workbench →	`u0u1u1`	`u0u1u1`
accepted-key.vp The attacker can know a key the client discards. The precondition checks secrecy only when the client proceeds to send its request. 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 Authenticating the coordinator’s messages prevents the attacker from collecting partial signatures for a message it chose. The signers’ messages to the coordinator are authenticated too, because anyone can combine partial signatures. Open in Workbench → Read the model	`c0c0a0`	`c0c0a0`
nonce-reuse.vp Reusing a key and nonce reveals both plaintexts. A third message under a different nonce stays secret. 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 attacker replays a message from a second session. The recipient accepts and forwards it. 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 uses one run with an honest peer and another with a corrupt peer. 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. The signers’ messages to the coordinator are authenticated as well: combining partial signatures needs no secret, so over open channels the attacker could make the coordinator abort and hand the verifier the combined signature itself, which the verifier would accept although the coordinator never sent it. 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, so neither earlier ciphertext can replace it. Nonce reuse lets the attacker construct a new ciphertext 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 has a weakening annotation. Check when the attacker learns its plaintext and whether m_now remains secret.

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