PQXDH in Lean

 PQXDH in Lean🔗

Christiano Braga

A Lean 4 formalization of Signal's X3DH and PQXDH key agreement protocols, following Bhargavan et al. (USENIX Security 2024).

The formalization uses Mathlib's Module F G for Diffie-Hellman and VCV-io for security game definitions (DDH, advantage bounds).

The source code is available on GitHub.

Contents

  1. 1. Diffie-Hellman
  2. 2. Key Derivation Function
  3. 3. Authenticated Encryption with Associated Data
  4. 4. Key Encapsulation Mechanism
  5. 5. The X3DH Protocol
  6. 6. The PQXDH Protocol
  7. 7. Security Definitions
  8. Dependency Graph
  9. Blueprint Summary