5.1. Key pairs🔗

A key pair binds a private scalar (in a field F) to its public key (a group element), derived from a shared generator. The generator is a type parameter, enforcing that all key pairs in a session share the same generator by construction.

structure KeyPair (F G : Type _) [Field F] [AddCommGroup G] [Module F G]
    (G₀ : G) where
  priv : F
  pub : G
  pub_eq : pub = DH priv G₀