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 PermDraws Tactic
  7. 7. The PQXDH Protocol
  8. 8. Security Definitions