PQXDH in Lean

1. Diffie-Hellman🔗

Abstract Diffie-Hellman over any additive commutative group. We define DH(a, B) as scalar multiplication in a Module F G, where F is a field and G is an additive commutative group. All algebraic properties (commutativity, associativity, distributivity) follow from the module axioms alone, with no curve, field, or encoding mentioned. Protocol proofs (X3DH, PQXDH) import only this file.

  1. 1.1. Definition
  2. 1.2. Notation
  3. 1.3. Algebraic properties