Documentation / The Scuttlebutt handshake

The Scuttlebutt handshake

Investigate identity hiding, ciphertext substitution, session binding and compromise in a simplified Scuttlebutt handshake.

For running these models and interpreting trace excerpts, see Reproducing the examples.

Scuttlebutt¹ is a decentralized communication protocol. This guide uses a simplified handshake to study identity hiding, transcript binding and compromise. The model deliberately uses one key and empty associated data across several boxes. The deployed construction has additional key separation and box-stream framing. A substitution found here must therefore be read as a finding about this model, not as a claimed vulnerability in deployed Scuttlebutt.

Security Goals

The model examines four properties of the handshake and the assumptions behind them:

• Initiator identity hiding. An attacker cannot learn the public key of the initiator.

• Message confidentiality. An attacker cannot learn the content of messages exchanged between principals.

• Network-identifier hiding. Both peers know a key identifying the Scuttlebutt network, but a network attacker should not learn it from the handshake.

• Forward secrecy. A later compromise of a long-term private key should not decrypt previously recorded handshakes.

This guide’s scuttlebutt.vp contains the private-identifier base model. Its public-identifier, unguarded-key and later-leak variants have descriptive suffixes in the same directory. The engine repository’s example uses different assumptions; use this guide’s files to reproduce this guide.

Principals

Each principal has a long-term identity key pair and a fresh ephemeral key pair:

attacker[active]
principal Alice[
		knows private n
		knows private longTermA
		generates ephemeralA
		longTermAPub = PUBKEY(longTermA)
		ephemeralAPub = PUBKEY(ephemeralA)
	]
principal Bob[
		knows private n
		knows private longTermB
		generates ephemeralB
		longTermBPub = PUBKEY(longTermB)
		ephemeralBPub = PUBKEY(ephemeralB)
	]
Bob -> Alice: [longTermBPub]

The network identifier n is initially declared private and pre-shared. This assumption excludes malicious network members, because every member must know n. The main Scuttlebutt network identifier is publicly documented; a private identifier instead describes a restricted network. A later variant makes n public to measure the properties that depend on its secrecy. The example distributed with Verifpal, examples/messaging/scuttlebutt.vp, uses the public declaration and therefore includes attacks by network members.

The exchange spans two round trips. Alice and Bob first exchange ephemeral public keys and MACs:

principal Alice[
		nMacAlice = MAC(n, ephemeralAPub)
	]
Alice -> Bob: ephemeralAPub, nMacAlice
principal Bob[
		nMacAliceValid = ASSERT(MAC(n, ephemeralAPub), nMacAlice)?
		nMacBob = MAC(n, ephemeralBPub)
	]
Bob -> Alice: ephemeralBPub, nMacBob

Each MAC binds an ephemeral public key to n. A key and MAC from another network will not pass the checked assertion. This mechanism does not distinguish sessions within the same network.

Alice derives one master secret to protect her identity and a second to protect the authenticated session and its messages:

principal Alice[
		nMacBobValid = ASSERT(MAC(n, ephemeralBPub), nMacBob)?
		ephemeralSecretAlice = DH_KEX(ephemeralBPub, ephemeralA)
		longTermSecretAlice = DH_KEX(longTermBPub, ephemeralA)
		masterSecret1Alice = HASH(n, ephemeralSecretAlice, longTermSecretAlice)
		sig1Alice = SIGN(longTermA, HASH(n, longTermBPub, ephemeralSecretAlice))
		generates n1, n2
		secretBox1Alice = AEAD_ENC(masterSecret1Alice, n1, sig1Alice, nil)
		secretBox2Alice = AEAD_ENC(masterSecret1Alice, n2, longTermAPub, nil)
		longEphemeralSecretAlice = DH_KEX(ephemeralBPub, longTermA)
		masterSecret2Alice = HASH(n, ephemeralSecretAlice, longTermSecretAlice, longEphemeralSecretAlice)
	]
Alice -> Bob: n1, secretBox1Alice, n2, secretBox2Alice

Bob reconstructs the first master secret, decrypts Alice’s signature and identity key, verifies the signature, and derives the remaining Diffie–Hellman input:

principal Bob[
		ephemeralSecretBob = DH_KEX(ephemeralAPub, ephemeralB)
		longTermSecretBob = DH_KEX(ephemeralAPub, longTermB)
		masterSecret1Bob = HASH(n, ephemeralSecretBob, longTermSecretBob)
		sig1Bob = AEAD_DEC(masterSecret1Bob, n1, secretBox1Alice, nil)?
		longTermAPub_Bob = AEAD_DEC(masterSecret1Bob, n2, secretBox2Alice, nil)?
		sig1Valid = SIGNVERIF(longTermAPub_Bob, HASH(n, longTermBPub, ephemeralSecretBob), sig1Bob)?
		longEphemeralSecretBob = DH_KEX(longTermAPub_Bob, ephemeralB)
	]

Bob signs the transcript and encrypts the signature under the second master secret:

principal Bob[
		sig2Bob = SIGN(longTermB, HASH(n, sig1Bob, longTermAPub_Bob, ephemeralSecretBob))
		masterSecret2Bob = HASH(n, ephemeralSecretBob, longTermSecretBob, longEphemeralSecretBob)
		generates n3
		secretBox1Bob = AEAD_ENC(masterSecret2Bob, n3, sig2Bob, nil)
	]
Bob -> Alice: n3, secretBox1Bob

After Alice verifies Bob’s transcript signature, the model sends one encrypted message in each direction:

principal Alice[
		knows private m1
		sig2Alice = AEAD_DEC(masterSecret2Alice, n3, secretBox1Bob, nil)?
		sig2Valid = SIGNVERIF(longTermBPub, HASH(n, sig1Alice, longTermAPub, ephemeralSecretAlice), sig2Alice)?
		generates n4
		secretBoxM1Alice = AEAD_ENC(masterSecret2Alice, n4, m1, nil)
	]
Alice -> Bob: n4, secretBoxM1Alice

principal Bob[
		knows private m2
		m1Bob = AEAD_DEC(masterSecret2Bob, n4, secretBoxM1Alice, nil)?
		generates n5
		secretBoxM2Bob = AEAD_ENC(masterSecret2Bob, n5, m2, nil)
	]

Bob -> Alice: n5, secretBoxM2Bob
principal Alice [
		m2Alice = AEAD_DEC(masterSecret2Alice, n5, secretBoxM2Bob, nil)?
	]

The model now contains the complete handshake and one application message in each direction.

Queries and Analysis

Express the four security goals as queries:

queries[
		confidentiality? n
		confidentiality? m1
		confidentiality? m2
		confidentiality? longTermAPub
		authentication? Alice -> Bob: secretBox1Alice
		authentication? Alice -> Bob: secretBox2Alice
		authentication? Bob -> Alice: secretBox1Bob
		authentication? Alice -> Bob: secretBoxM1Alice
		authentication? Bob -> Alice: secretBoxM2Bob
		equivalence? masterSecret2Alice, masterSecret2Bob
	]

The equivalence query is not one of the four documented goals, but a key exchange must also give both participants the same key. Confidentiality and authentication queries do not directly test this agreement.

The initial model produces these verdicts:

Pass ✓ confidentiality? n
Pass ✓ confidentiality? m1
Pass ✓ confidentiality? m2
Pass ✓ confidentiality? longtermapub
Pass ✓ authentication? Alice -> Bob: secretbox1alice
Pass ✓ authentication? Alice -> Bob: secretbox2alice
Pass ✓ authentication? Bob -> Alice: secretbox1bob
Fail ✗ authentication? Alice -> Bob: secretboxm1alice
Fail ✗ authentication? Bob -> Alice: secretboxm2bob
Fail ✗ equivalence? mastersecret2alice, mastersecret2bob

Fail ✗ 3 of 10 queries failed.

The passing queries exhaust the search at two sessions; their envelopes are omitted from this summary. Both application-message authentication queries fail at one session as well. The equivalence failure requires the second session. The following sections explain why.

Using a Ciphertext in the Wrong Position

The attacker records Bob’s handshake signature box, secretBox1Bob, together with its nonce n3. It can substitute that pair in either application-message position:

Attacker replaces n4, secretboxm1alice (sent by Alice to
Bob) with n3, secretbox1bob.

Attacker replaces n5, secretboxm2bob (sent by Bob to Alice)
with n3, secretbox1bob.

These are excerpts from two separate traces. In the first, Bob decrypts his own earlier signature box where he expects Alice’s application message. In the second, Alice decrypts Bob’s signature box again where she expects his application reply. The attacker neither learns the key nor constructs a new ciphertext.

The substitutions succeed because all three positions use equivalent keys and the same nil associated data. Each supplied ciphertext has the correct nonce, so authenticated decryption succeeds. Nothing in that operation tells the recipient that the plaintext belongs to a handshake rather than an application message.

This is a useful distinction between ciphertext integrity and protocol authentication. An intact ciphertext can be accepted in the wrong place. To represent a protocol that prevents this, include the direction and message role in the authenticated data or use the direction-specific keys that the protocol actually derives. Then query the resulting model again. Adding tags is a protocol change unless the deployment already provides them.

The earlier secretBox1Bob authentication query passes at both tested counts. A tempting replacement would use Bob’s later application box. That value is emitted only after earlier checks and messages have been reached. The validator also requires knowledge learned from one execution of a run to be compatible with the execution against which it is used. Merely finding a ciphertext under the same key, or adding a second session, does not make that substitution an executable attack.

What the Second Session Adds

The additional failure at two sessions is the equivalence query. The attacker routes a hello and sealed flight from Alice’s second run to Bob, with the corresponding ephemeral-key and MAC deliveries. Bob derives a master secret with that Alice run. The named masterSecret2Alice still denotes the first Alice run’s value, so the compared terms differ.

This result is about the particular pair named by the query. Session clones represent runs of the same actor, and exchanging messages with another matching run does not by itself forge that actor’s identity. The equivalence query nevertheless asks whether these two stored values agree. If the intended property is agreement with whichever peer run actually answered, this comparison is too specific to establish it; examine authentication and the protocol’s session binding as well.

At one session, the routing has no second Alice run to draw on. An incompatible replacement instead causes a check to fail before the needed comparison is reached. A halted run’s uncomputed master secret does not count as a divergent value (Equivalence Queries).

Changing the Trust Assumptions

First remove only the guard from longTermBPub. No verdict changes at either tested count. The private network identifier n still prevents the attacker from constructing a hello MAC for a key of its own. This measures the guard’s effect under the other assumptions; it does not make identity-key authentication unnecessary in another model.

Next restore the guard and change both declarations of n to knows public. This admits an attacker that knows the network identifier, as a network member would.

Fail ✗ confidentiality? n
Pass ✓ confidentiality? m1
Fail ✗ confidentiality? m2
Pass ✓ confidentiality? longtermapub
Fail ✗ authentication? Alice -> Bob: secretbox1alice
Fail ✗ authentication? Alice -> Bob: secretbox2alice
Pass ✓ authentication? Bob -> Alice: secretbox1bob
Fail ✗ authentication? Alice -> Bob: secretboxm1alice
Fail ✗ authentication? Bob -> Alice: secretboxm2bob
Fail ✗ equivalence? mastersecret2alice, mastersecret2bob

Fail ✗ 7 of 10 queries failed.

All seven failures are also found at one session. The confidentiality failure for n is expected: it is now explicitly public. Bob’s application plaintext m2 is disclosed through an impersonation of Alice. Removing Bob’s identity-key guard in this variant again changes no verdict.

How the Attacker Reads Bob’s Reply

The public-identifier trace for m2 constructs a complete forged exchange. The following walkthrough groups its 26 steps by purpose; the full numbered trace is available by running scuttlebutt-public.vp.

1. The attacker replaces Alice’s ephemeral key with PUBKEY(nil) and supplies MAC(n, PUBKEY(nil)). Because n is public, Bob’s hello check passes.

2. Using Bob’s public keys and nil, the attacker computes the two Diffie–Hellman terms that form Bob’s first master secret. It can therefore encrypt values that Bob will decrypt.

3. The attacker supplies its own identity key, PUBKEY(nil), in the identity box and signs the expected transcript with nil in the signature box. It encrypts both under Bob’s first master secret and uses the observed nonces. Both decryptions and the signature check pass on these concrete replacements.

4. Bob’s third Diffie–Hellman term now uses the attacker-supplied identity key. The attacker can derive the second master secret too.

5. The attacker replaces Alice’s application message with an encryption of nil under that secret. Bob accepts it and reaches the send of his reply.

6. The attacker records Bob’s reply and its nonce, then decrypts the reply with the second master secret to obtain m2.

The replacement identity and transcript signature are essential. Without them, Bob would halt before sending the reply the attacker wants to read. The current trace supplies ciphertexts that pass the checks directly; it needs no bypass or unconfirmed-witness note.

Bob’s checks establish consistency with the identity key inside the received box. They do not establish that this key belongs to the Alice named in the authentication query. Guarding Bob’s key authenticates Bob to Alice, but supplies no independent authentication of Alice to Bob.

The m1 and longTermAPub queries remain uncontradicted. That reports the outcome of this search; it does not prove those values confidential against every strategy. The replay, term-basis and depth limits of How analysis works still apply.

A Later Identity-Key Disclosure

Return to private n and guarded longTermBPub. Immediately before the queries, add:

phase[1]
principal Alice[
	leaks longTermA
]

The scuttlebutt-leak.vp variant has four failing queries at two sessions. The three base-model failures persist, and confidentiality? longTermAPub now fails because the attacker can compute the public key from the disclosed private key. Both application-message confidentiality queries still pass.

This is a specific forward-secrecy experiment: disclose Alice’s identity private key after the exchange and ask about the earlier messages. It does not disclose ephemeral secrets or all device memory. The model retains these values internally; omitting them from the leak expresses the compromise assumption, not an implemented erasure operation.

Moving the same leak into phase 0 changes no verdict in this model. The private network identifier still prevents the attacker from generating a suitable initial hello for its own key. Keep the later phase when stating forward secrecy, since it records the intended timing even when this variant happens to produce the same code.

Comparing the Variants

The traces explain more than these counts. Two failures arise from using an intact ciphertext in the wrong protocol position. Another compares values belonging to different paired runs. Making the network identifier public permits a forged exchange with Bob. The later key leak discloses Alice’s public identity but does not expose either application plaintext in the explored executions. Each finding depends on a different part of the model.