A full handshake

For two devices with any keys, preshared key, clocks and randomness, every step of a full handshake returns the model's result and writes the model's bytes. When both identities are usable, the Diffie-Hellman values agree and none of them is zero, the timestamp is not zero, B's boot clock is at least 20 ms and the one allocation succeeds, every step succeeds and each side's sending key is the other's receiving key. Clearing the keypairs frees everything.

That a completed handshake ends with the keys crossed over and the initiator's timestamp at the responder needs the two sides' Diffie-Hellman values to agree. For X25519 this is proved, because the proof's model of the Curve25519 code refines fiat-crypto's verified Montgomery ladder.
The spec states its completeness only for the case where the Diffie-Hellman values agree, which is why its first comment calls the agreement "not proved here".

spec: x_handshake
length: 339 lines of C
own proof: 17,673 lines of Rocq
status: Proved; 20 of 38

On this page

The spec

The property is stated by the C program harness/x_handshake.c, 339 lines. Here is its main cut down to the inputs it draws, the calls into the code under test and the checks (lines 33–339; ... marks lines left out). The checks call helpers and the model in the spec and in harness/common.h.

int main(void)
{
	...
	wg_shim_boottime_ns = draw_boottime();
	...
	wg_noise_init();
	nondet_bytes(raw_a, 32);
	nondet_bytes(raw_b, 32);
	...
	CHECK(wa.static_identity.has_identity == ia.ok && wb.static_identity.has_identity == ib.ok);
		...
		CHECK(!ok1 && hs_same(&snap, &pb.handshake));
	...
	CHECK(pb.handshake.state == HANDSHAKE_CREATED_INITIATION);
	...
	wg_cookie_add_mac_to_packet(m1, sizeof(*m1), &pb);
	...
	ret = wg_noise_handshake_consume_initiation(m1, &wb);
		...
		CHECK(bytes_eq(pa.handshake.latest_timestamp, ci.ts, 12) && bytes_eq(ci.ts, ts, 12));
	...
	CHECK(table_has(&itb, &pa.handshake.entry) && table_index_unique(&itb, m2->sender_index) && table_len(&itb) == 1);
	...
	wg_cookie_add_mac_to_packet(m2, sizeof(*m2), &pa);
	...
	ret = wg_noise_handshake_consume_response(m2, &wa);
		...
		CHECK(ret == &pb && pb.refcount.refcount == 2);
		...
		CHECK(bytes_eq(ka->sending.key, first, 32) && bytes_eq(ka->receiving.key, second, 32));
		...
		rb = wg_noise_handshake_begin_session(&pa.handshake, &pa.keypairs);
			...
			wg_noise_keypairs_clear(&pb.keypairs);
		...
		CHECK(bytes_eq(kb->receiving.key, first, 32) && bytes_eq(kb->sending.key, second, 32));
	...
	wg_noise_keypairs_clear(&pa.keypairs);
	...
	CHECK(pa.refcount.refcount == 1 && pb.refcount.refcount == 1);
...
}

The full spec at commit 3c1fc13 ↗

The property as the spec's first comment states it

Law `handshake`: a full Noise_IKpsk2 handshake between two devices agrees with the model at every step, and is
complete.

Setup: devices A and B with ANY static private keys (32 bytes each, as userspace sets them), each with one peer
for the other configured with the other's public key and ONE preshared key (any 32 bytes, or none); ANY boot
clock (< 2^62 ns, common.h) and real-time clock, ANY ephemeral randomness (the shim's get_random_bytes).
Steps: A wg_noise_handshake_create_initiation, A wg_cookie_add_mac_to_packet, B consume_initiation,
B create_response, B add_mac, A consume_response, A and B wg_noise_handshake_begin_session, then both
wg_noise_keypairs_clear.
Claims:
 - identities, precomputed static-static DH and cookie keys are the model's;
 - every step's result (bool / returned peer) is the model's (common.h: the WireGuard paper's handshake over the
   kernel's primitives), and when it succeeds EVERY byte it writes is the model's: all message fields (type,
   indices, ephemeral, encrypted static, encrypted timestamp = TAI64N of the real clock, encrypted empty payload,
   mac1 = MAC(HASH("mac1----" || S_pub), message up to mac1), mac2 = 0 without a cookie), the handshake state,
   hash, chaining key, ephemeral private key (= clamp(random bytes)), remote ephemeral, remote index, latest
   timestamp, last consumption time; the fields the step must not touch are unchanged (incl. the macs of a
   message before add_mac, and the message a consume reads);
 - indices: a new sender index is the random 32-bit value the table drew, hashed exactly once and unique;
   begin_session moves the handshake's index to the keypair (the handshake entry leaves the table);
 - the keypairs are the model's: initiator current / responder next, keys = KDF2(C, empty) in the
   initiator/responder order, remote index, birthdate = now, valid, fresh counters, references, and the peer
   references taken by the consume functions are balanced;
 - COMPLETENESS: if the Diffie-Hellman values of the two sides agree pairwise (DH(a, B) = DH(b, A) for the four
   pairs ee, es, se, ss - a property of X25519, not proved here: this law is relative to the primitives), none
   of them is zero, both identities are usable, the timestamp is not zero and B's clock is at least 20 ms, then
   every step succeeds (unless the one allocation fails), both sides end with the same chaining key and hash,
   and A's sending key is B's receiving key and vice versa;
 - clear frees both keypairs and empties both index tables; no allocation is left (the harness frees its own).

The code it is about

wg_noise_handshake_begin_session in drivers/net/wireguard/noise.c, lines 827–875 (... marks lines left out):

bool wg_noise_handshake_begin_session(struct noise_handshake *handshake,
				      struct noise_keypairs *keypairs)
{
	struct noise_keypair *new_keypair;
	bool ret = false;

	down_write(&handshake->lock);

	/* QUICKPROOF P07: `goto out` is `break` out of this block (VST has no goto); same statements in the same order */
	do {
	if (handshake->state != HANDSHAKE_CREATED_RESPONSE &&
	    handshake->state != HANDSHAKE_CONSUMED_RESPONSE)
		break;

	new_keypair = keypair_create(handshake->entry.peer);
	if (!new_keypair)
		break;
	new_keypair->i_am_the_initiator = handshake->state ==
					  HANDSHAKE_CONSUMED_RESPONSE;
	new_keypair->remote_index = handshake->remote_index;

	if (new_keypair->i_am_the_initiator)
		derive_keys(&new_keypair->sending, &new_keypair->receiving,
			    handshake->chaining_key);
	else
		derive_keys(&new_keypair->receiving, &new_keypair->sending,
			    handshake->chaining_key);

	handshake_zero(handshake);
	rcu_read_lock_bh();
	if (likely(!READ_ONCE(container_of(handshake, struct wg_peer,
					   handshake)->is_dead))) {
		add_new_keypair(keypairs, new_keypair);
		net_dbg_ratelimited("%s: Keypair %llu created for peer %llu\n",
				    handshake->entry.peer->device->dev->name,
				    new_keypair->internal_id,
				    handshake->entry.peer->internal_id);
		ret = wg_index_hashtable_replace(
			handshake->entry.peer->device->index_hashtable,
			&handshake->entry, &new_keypair->entry);
	} else {
		kfree_sensitive(new_keypair);
	}
...
}

This is the code under test as the proof sees it: Linux at 551c722f with the two lib/crypto patches, and with the idiom rewrites that VST needs, each marked QUICKPROOF in the code and listed in DEVIATIONS.md.

The theorem

QuickProof generated this statement from the spec in src/contracts/x_handshake.v:

Rocq

Theorem x_handshake : harness_safe whole_prog.

whole_prog is the spec linked with the code under test. The 19 x_ specs are proved together, as the theorem suite_x, from one specification of every function of the code. src/contracts/laws.v states each spec on its own program and takes it from suite_x:

Rocq

Theorem x_handshake : harness_safe WgNoise.contracts.x_handshake.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 WgNoise.contracts.suite.suite_x)))))))). Qed.

qp verify checks that this statement is the one generated from the spec at the contract commit, and that its proof uses no axiom beyond the 13 that every spec here uses: standard logical axioms and VST's abstract malloc library.

The C files (units) its program links

drivers/net/wireguard/noise.c
drivers/net/wireguard/cookie.c
patch/counter_validate.c
lib/crypto/blake2s.c
lib/crypto/chacha.c
lib/crypto/chacha-block-generic.c
lib/crypto/poly1305.c
lib/crypto/poly1305-donna32.c
lib/crypto/chacha20poly1305.c
lib/crypto/curve25519.c
lib/crypto/curve25519-fiat32.c
patch/wg_shim.c
quickproof/libc/libc.c
quickproof/libc/malloc_unit.c

What it leaves out

Like every spec of this proof: runs of more than one thread (locks and RCU are those of a single thread), termination (a run that never returns is not a counterexample), and binaries built by a compiler (the theorem is about the code as CompCert defines C for 64-bit x86).
The kernel around the code is a shim of plain C for one thread, and the code carries rewrites of idioms that VST cannot handle. Both are tested against the kernel's code, not proved.

Recorded for this property in DEVIATIONS.md (section L, what the properties exclude or assume):

L05. The Diffie-Hellman agreement of X25519 that handshake completeness needs is proved, not assumed: the proof's model of the Curve25519 code, x25519_m, refines the verified Montgomery ladder of fiat-crypto, and X25519(a, X25519(b, 9)) = X25519(b, X25519(a, 9)) for 32-byte scalars follows from the group law of fiat-crypto's Montgomery curve (x25519fiat/, with fiat-crypto, Coqprime and Rewriter vendored unmodified in vendor/fiat-crypto/). x_handshake states completeness only when the Diffie-Hellman values agree, so its first comment calls the agreement "not proved here"; the proof of hs_matching_keys uses it, among others

The summary page lists what the proof as a whole does not cover.

How it was proved

src/proof/harness/handshake/ holds 17,673 lines of Rocq (formerly Coq) that are specific to this spec. It builds on the specifications and proofs of the functions of noise.c, cookie.c and lib/crypto, the protocol model, and the Diffie-Hellman agreement of X25519. The whole proof of the 38 specs is about 300,000 lines. AI agents wrote it, Rocq checks all of it, and nobody has to read it. What people have to read is the spec above, with harness/common.h, and the kernel shim that DEVIATIONS.md describes.

Other specs about noise.c: see the list on the left, or the summary.

The spec#

The code it is about#

The theorem#

What it leaves out#

How it was proved#

The spec

The code it is about

The theorem

What it leaves out

How it was proved