5.3. Correctness🔗

If all key pairs are honestly generated from the same generator, then Alice and Bob compute identical DH tuples:

theorem X3DH_agree
    {G₀ : G}
    (ikₐ ekₐ : KeyPair F G G₀)
    (ikᵦ spkᵦ : KeyPair F G G₀)
    (opkᵦ : Option (KeyPair F G G₀)) :
    X3DH_Alice ikₐ.priv ekₐ.priv ikᵦ.pub spkᵦ.pub (opkᵦ.map KeyPair.pub) =
    X3DH_Bob ikᵦ.priv spkᵦ.priv (opkᵦ.map KeyPair.priv) ikₐ.pub ekₐ.pub

The proof works by cases on OPK, then applies simp with the Module F G lemmas (smul_smul, mul_comm) plus each key pair's generation equation.

Session key derivation

Both parties feed the DH tuple into a KDF to obtain a session key:

def X3DH_SK_Alice (kdf : KDF (G × G × G × G) SK)
    (ikₐ ekₐ : F) (IKᵦ SPKᵦ : G) (OPKᵦ : Option G) : SK :=
  kdf.derive (X3DH_Alice ikₐ ekₐ IKᵦ SPKᵦ OPKᵦ)

Since the DH tuples are equal (by X3DH_agree), the derived session keys are equal (X3DH_session_key_agree).

Handshake correctness

End-to-end correctness: Bob can decrypt Alice's first message.

theorem X3DH_handshake_correct
    (kdf : KDF (G × G × G × G) SK)
    (aead : AEAD SK PT CT_aead (G × G))
    {G₀ : G}
    (ikₐ ekₐ ikᵦ spkᵦ : KeyPair F G G₀)
    (opkᵦ : Option (KeyPair F G G₀))
    (msg : PT) (ct : CT_aead)
    (h_enc : ct = aead.encrypt (X3DH_SK_Alice kdf ...) msg (ikₐ.pub, ikᵦ.pub)) :
    aead.decrypt (X3DH_SK_Bob kdf ...) ct (ikₐ.pub, ikᵦ.pub) = some msg

This composes DH agreement, session key agreement via KDF, and AEAD correctness.