PQXDH in Lean

6. The PQXDH Protocol🔗

The PQXDH (Post-Quantum Extended Diffie-Hellman) protocol extends X3DH by adding a post-quantum KEM layer. Alice appends the KEM shared secret to her KDF input, and Bob recovers the same secret by decapsulation. The resulting session key depends on both classical DH and post-quantum KEM contributions.

  1. 6.1. Protocol bundle
  2. 6.2. Shared secret computation
  3. 6.3. Session key derivation
  4. 6.4. Agreement
  5. 6.5. Security properties