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 studies a simplified handshake that uses one key and empty associated data for several encrypted messages. Deployed Scuttlebutt adds key separation and box-stream framing. The substitutions shown here are attacks on this simplified model; they do not establish vulnerabilities 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.

Start with scuttlebutt.vp, which keeps the network identifier private. The variants below make it public, remove a key guard or add a later leak. Use these downloads to reproduce the results; the example in the verifier repository uses different assumptions.

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 test which properties depend on it staying secret. 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)?
]

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 also checks that both participants derive the same key. Confidentiality and authentication queries do not directly test key equality.

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
Fail ✗ authentication? Bob -> Alice: secretbox1bob
Fail ✗ authentication? Alice -> Bob: secretboxm1alice
Fail ✗ authentication? Bob -> Alice: secretboxm2bob
Fail ✗ equivalence? mastersecret2alice, mastersecret2bob

Fail ✗ 4 of 10 queries failed.

The passing queries report that the two-session search finished; those notes are omitted here. Both application-message authentication queries also fail at one session. The authentication of secretBox1Bob and the equivalence query pass at one session and fail only with the second; both failures are explained below.

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.

Authenticated encryption can accept an intact ciphertext in the wrong protocol position. Model the protocol’s defenses against this by including the direction and message role in associated data, or by using its direction-specific keys. Add tags only if they exist in the implementation or you are proposing a protocol change, then rerun the queries.

At one session the earlier secretBox1Bob authentication query passes. Bob’s application box uses the same key, but he sends it only after Alice has accepted his handshake box, so in a single run it cannot stand in for that box. A second session supplies another Bob. The attacker connects Bob#2 to Alice: it delivers her hello, its MAC and her encrypted handshake boxes to Bob#2, and Bob#2’s hello and MAC to her, so both derive the same master secrets (steps 1–13 of that trace). It then reflects Bob#2’s own handshake box back to him as Alice’s application message. Bob#2 accepts it and answers with his application box, which the attacker delivers to Alice as secretBox1Bob (steps 16–20). Alice’s decryption succeeds (step 21). Her signature check fails on the resulting plaintext, but by then she has successfully used a ciphertext that Bob produced for a different position, which is what the query tests (Authentication queries).

Comparing one and two sessions

At one session, the equivalence search finishes without finding a divergence. At two sessions the query fails through a cross-session routing.

The attacker forwards Alice’s second hello and its MAC to Bob, and delivers Bob’s hello to Alice’s second run. It then forwards that run’s encrypted handshake boxes and their nonces to Bob. Bob’s checks pass and his master secret agrees with Alice’s second run. Alice’s first run computes a different master secret, so the two values named in the query differ; the last two steps of the trace show what each resolves to.

The query compares fixed named values, even when the network connects their owners to different peer runs. This divergence does not by itself disclose a plaintext or impersonate Alice. Values computed before a later halt remain distinct from values never computed because a check failed (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 result depends on the private network identifier and does not justify removing identity-key authentication elsewhere.

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
Fail ✗ authentication? Bob -> Alice: secretbox1bob
Fail ✗ authentication? Alice -> Bob: secretboxm1alice
Fail ✗ authentication? Bob -> Alice: secretboxm2bob
Fail ✗ equivalence? mastersecret2alice, mastersecret2bob

Fail ✗ 8 of 10 queries failed.

Seven of the eight failures are also found at one session; authentication of secretBox1Bob needs the second, as in the base model. 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 as well, in scuttlebutt-public-unguarded.vp, makes all ten queries fail at both session counts. The additional failures are confidentiality of m1 and longTermAPub, and, at one session, authentication of secretBox1Bob.

The attacker replaces Bob’s identity and ephemeral public keys with PUBKEY(nil) and constructs the hello MAC using public n. It can derive Alice’s first master secret and open her identity box. It then derives her second master secret and supplies a handshake signature made with nil. Alice accepts it under the substituted identity key and sends m1, which the attacker decrypts.

How the attacker reads Bob’s reply

To obtain m2, the attacker forges an exchange with Bob. The steps below summarize the 24-step trace. Run scuttlebutt-public.vp to see the full trace.

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, with nil as each nonce. 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.

Without the replacement identity and transcript signature, Bob would stop before sending his reply. The ciphertexts in this trace pass his checks directly, as the gate steps show.

Bob verifies the signature using the identity key in the received box. He has no independent evidence 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.

With Bob’s identity key still guarded, the search finds no disclosure of m1 or longTermAPub. These passes remain subject to the search’s session, term and depth limits.

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 three failing queries at one session. The two 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. At two sessions, secretBox1Bob authentication and the equivalence query also fail, as in the base model.

This forward-secrecy experiment leaks only Alice’s identity private key after the exchange. It assumes that ephemeral secrets and other device memory remain unavailable to the attacker. Verifpal still stores those values internally; leaving them out of the leak does not model key erasure.

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 leak in the later phase when testing forward secrecy so that the model states the intended compromise time.

Comparing the variants