5.2. Shared secret computation🔗

Alice and Bob each compute four DH values:

• DH1 = DH(ikₐ, SPKᵦ) — mutual authentication (Alice's identity)

• DH2 = DH(ekₐ, IKᵦ) — mutual authentication (Bob's identity)

• DH3 = DH(ekₐ, SPKᵦ) — forward secrecy

• DH4 = DH(ekₐ, OPKᵦ) — replay protection (when OPK is present)

When OPK is absent, DH4 defaults to 0 (the group identity).

def X3DH_Alice
    (ikₐ ekₐ : F) (IKᵦ SPKᵦ : G) (OPKᵦ : Option G) : G × G × G × G :=
  (DH ikₐ SPKᵦ, DH ekₐ IKᵦ, DH ekₐ SPKᵦ, DH ekₐ (OPKᵦ.getD 0))

def X3DH_Bob
    (ikᵦ spkᵦ : F) (opkᵦ : Option F) (IKₐ EKₐ : G) : G × G × G × G :=
  (DH spkᵦ IKₐ, DH ikᵦ EKₐ, DH spkᵦ EKₐ, DH (opkᵦ.getD 0) EKₐ)