spake2 #

SPAKE2 and SPAKE2+ password-authenticated key exchange over P-256, in OCaml.

Pairing a device with a short PIN, or logging in without sending the password, needs a key exchange that turns a low-entropy secret into a strong shared key. A plain Diffie-Hellman exchange authenticated by a password hash leaks enough for an eavesdropper to run an offline dictionary attack: when the transcript holds any value computable from the password alone, such as H(password, nonce), the eavesdropper hashes every word of a dictionary and compares, with no further contact. A password-authenticated key exchange (PAKE) does not: each run lets an active attacker test one password guess and a passive one learn nothing. SPAKE2 blinds each Diffie-Hellman share with the password scalar w, sending X = x·G + w·M for a fixed point M whose discrete logarithm nobody knows. Every candidate w is consistent with X, and testing a guess needs the ephemeral secret x, which never leaves the party.

This library implements two PAKEs:

SPAKE2 (RFC 9382), where both parties derive the same values from the password.
SPAKE2+ (draft-bar-cfrg-spake2plus-02), an augmented PAKE where the server stores a verifier instead of password-equivalent data. Matter, the Connectivity Standards Alliance's smart-home protocol, uses it to commission devices: a controller such as a phone adds a new device to its network by proving it knows the setup PIN printed on the device, and derives the first session key from it.

Both run the key confirmation round the specifications require and release the shared key only once the peer's confirmation has verified. Each protocol is also available as a state machine (Spake2.Control) that sequences the messages for the caller.

SPAKE2+ follows draft 02 because Matter R1.4 cites that version normatively. TT is the transcript: the context, the identities, M, N, both shares and the two Diffie-Hellman results, each prefixed by its length. Draft 02 splits its SHA-256 digest as Ka || Ke = Hash(TT) (section 4): Ka keys the confirmation MACs and Ke, sixteen octets, is the shared key the application uses. It applies no KDF (key derivation function, such as HKDF) between the digest and the shared secret. Later drafts derive the confirmation keys from the whole digest and call the output SharedKey, so they agree with draft 02 on the transcript and differ after it. The test suite runs the draft 02 Appendix B vectors through the protocol to hold the version.

Security #

The P-256 point operations come from mirage-crypto-ec, whose field arithmetic is generated by fiat-crypto and runs in constant time. Scalar arithmetic uses Zarith, which is not constant time; it computes protocol values but never branches on a secret. Zarith's running time still depends on the size of its operands, and those include secret scalars (w0, w1 and the ephemeral x and y), so the scalar arithmetic is not hardened against a timing measurement. Confirmation MACs are compared in constant time inside the library, and the caller never sees the expected value.

Installation #

Install with opam:

$ opam install spake2

If opam cannot find the package, it may not yet be released in the public opam-repository. Add the overlay repository, then install it:

$ opam repo add samoht https://tangled.org/gazagnaire.org/opam-overlay.git
$ opam update
$ opam install spake2

Usage #

SPAKE2 #

RFC 9382 section 3.3 has two rounds. The parties first exchange shares, then each MUST send a MAC over the transcript and MUST NOT consider the protocol complete until the peer's MAC has verified. Spake2.exchange runs both rounds. It executes the Spake2.Control.Party state machine, and it releases the shared secret Ke only on the transition that verifies the peer's confirmation.

let () = Crypto_rng_unix.use_default ()

let password = "secret"

(* Each party computes its share and sends it. *)
let state_a, share_a = Spake2.init ~password `A
let state_b, share_b = Spake2.init ~password `B

let a = Spake2.exchange ~id_a:"alice" ~id_b:"bob" state_a
let b = Spake2.exchange ~id_a:"alice" ~id_b:"bob" state_b

let recv what exchange octets =
  match Spake2.Exchange.recv exchange octets with
  | Ok step -> step
  | Error _ -> failwith ("the exchange refused " ^ what)

(* The peer's share derives the key schedule and puts this party's confirmation
   on the wire. No key comes out yet: nobody has been authenticated. *)
let a1 = recv "B's share" a share_b
let b1 = recv "A's share" b share_a
let () = assert (a1.key = None)

(* The peer's confirmation is what completes the protocol. *)
let a2 = recv "B's confirmation" a1.exchange (Option.get b1.send)
let b2 = recv "A's confirmation" b1.exchange (Option.get a1.send)

let () =
  match (a2.key, b2.key) with
  | Some key_a, Some key_b -> assert (String.equal key_a key_b)
  | _ -> failwith "no key was delivered"

Spake2.finish is the key agreement underneath and returns Ke without any confirmation. A caller that stops there shares a key with a peer it has not yet authenticated.

SPAKE2+ #

derive_w runs PBKDF2-SHA256 over the password and the salt for iterations rounds, cuts the 80-byte output into two 40-byte halves and reduces each modulo the P-256 group order, which gives w0 and w1. The verifier stores w0 and L = w1·G. The prover needs w1 itself to compute the shared value, and recovering w1 from L is a discrete logarithm, so a stolen server record does not let an attacker log in as the client.

let password = "secret"

(* Setup: derive the two password scalars. The verifier keeps w0 and l, and
   never w1 -- the fields are named and the two have different types, so it
   cannot keep the wrong one. *)
let salt = Spake2.Plus.generate_salt ()
let iterations = 1000
let { Spake2.Plus.w0; w1 } = Spake2.Plus.derive_w ~password ~salt ~iterations
let l = Spake2.Plus.compute_l ~w1

(* Protocol run: exchange pa and pb between prover and verifier. *)
let context = "myapp"
let prover_state, pa = Spake2.Plus.prover_init ~w0 ~w1 ~context
let verifier_state, pb = Spake2.Plus.verifier_init ~w0 ~l ~context

(* Each role's key confirmation round: the MAC it owes the peer goes on the
   wire, and the peer's is what releases the key. The expected MAC never leaves
   the library, so there is no comparison for a caller to get wrong. *)
let () =
  match
    ( Spake2.Plus.prover_finish prover_state pb,
      Spake2.Plus.verifier_finish verifier_state pa )
  with
  | Ok prover, Ok verifier -> (
      let confirm_p = Spake2.Confirmation.to_send prover in
      let confirm_v = Spake2.Confirmation.to_send verifier in
      match
        ( Spake2.Confirmation.confirm prover ~peer:confirm_v,
          Spake2.Confirmation.confirm verifier ~peer:confirm_p )
      with
      | Ok ke_prover, Ok ke_verifier ->
          assert (String.equal ke_prover ke_verifier)
      | _ -> failwith "a genuine confirmation was refused")
  | _ -> failwith "spake2+ exchange failed"

SPAKE2+ as an exchange #

prover_finish and verifier_finish leave the order of messages to the caller. The verifier sends confirmV as soon as it has received shareP, and the prover sends confirmP only once confirmV has verified. Spake2.Plus.prover and Spake2.Plus.verifier run the same protocol and enforce that order themselves. Each executes its Spake2.Control state machine and releases the key only on the transition the draft allows.

let prover = Spake2.Plus.prover prover_state
let verifier = Spake2.Plus.verifier verifier_state
let share_p = pa
let share_v = pb

(* A refusal is an answer: the phase stands and [exchange] is still the
   exchange. Here anything but progress is a test failure. *)
let step what exchange octets =
  match Spake2.Exchange.recv exchange octets with
  | Ok step -> step
  | Error _ -> failwith ("the exchange refused " ^ what)

(* The verifier answers shareP with confirmV, a step before the prover's. *)
let v1 = step "shareP" verifier share_p
let confirm_v = Option.get v1.send

(* The prover derives on shareV and holds confirmP back; confirmV is what lets
   it out, and the key with it. *)
let p1 = step "shareV" prover share_v
let () = assert (p1.send = None && p1.key = None)

let p2 = step "confirmV" p1.exchange confirm_v
let confirm_p = Option.get p2.send
let v2 = step "confirmP" v1.exchange confirm_p

let () =
  match (p2.key, v2.key) with
  | Some k_prover, Some k_verifier -> assert (String.equal k_prover k_verifier)
  | _ -> failwith "no key was delivered"

When a confirmation does not verify, the exchange moves to Aborted, sends nothing and delivers no key. The comparison runs inside the library in constant time.

API #

SPAKE2 #

Spake2.init ~password role: Start as `A or `B
Spake2.init_with ~w ~scalar role: Start over scalars supplied directly
Spake2.finish ?context ?id_a ?id_b state peer_msg: Agree Ke (no confirmation)

SPAKE2+ #

Spake2.Plus.derive_w ~password ~salt ~iterations: Derive { w0; w1 } from password
Spake2.Plus.compute_l ~w1: Compute L for server storage
Spake2.Plus.W0.of_octets / W1.of_octets / L.of_octets: Read a stored value back
Spake2.Plus.prover_init ~w0 ~w1 ~context: Initialize as prover (client)
Spake2.Plus.verifier_init ~w0 ~l ~context: Initialize as verifier (server)
Spake2.Plus.prover_finish state pb: The prover's key confirmation round
Spake2.Plus.verifier_finish state pa: The verifier's key confirmation round

Key confirmation #

Spake2.Confirmation.to_send t: The MAC this role owes the peer
Spake2.Confirmation.confirm t ~peer: Check the peer's, in constant time, and release Ke