Address PR #473 review feedback

- Rename Diffie-Hellman.lean → DiffieHellman.lean (valid module name).
- Align namespaces under ...Cryptographic.KeyExchange; DH lives in
  ...KeyExchange.DH as a sibling sub-namespace.
- Tighten the DiffieHellman class with [Fintype G], hq : Fintype.card G = q,
  and hg : orderOf g = q, so that g is a generator of a cyclic group of
  order q (previously under-constrained).
- Remove dead Fact q.Prime hypothesis.
- Rewrite module docstrings to match the actual generality of the code and
  add an explicit Scope note: correctness only, not DLP/CDH/DDH.
- Upgrade pow_mod_q / secret_eq prose to /-- ... -/ doc-strings.
- references.bib: switch BonehShoup entry to the online draft with URL.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: ChristianoBraga

Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Basic.lean

@@ -13,27 +13,27 @@ public import Mathlib.Tactic
 /-!
 # Key Exchange Protocol
 
-A *key exchange protocol* allows two parties (Alice and Bob) to establish a shared secret
-over an insecure channel.
+An abstract typeclass capturing the structure of a two-party key-exchange protocol. A
+protocol is given by three types — `PrivateKey`, `PublicValue`, `SharedSecret` — together
+with:
 
-The protocol proceeds as follows:
+* `pub : PrivateKey → PublicValue`, the value a party publishes;
+* `sharedSecret : PublicValue → PrivateKey → SharedSecret`, what each party computes from
+  the peer's public value and its own private key;
+* `agreement`, the correctness law
+  `sharedSecret (pub β) α = sharedSecret (pub α) β` for all `α, β`.
 
-1. Alice picks a private key α, computes her public value pub(α), and sends it to Bob.
-2. Bob picks a private key β, computes his public value pub(β), and sends it to Alice.
-3. Alice computes the shared secret as sharedSecret(pub(β), α).
-4. Bob computes the shared secret as sharedSecret(pub(α), β).
+Concrete protocols (e.g. Diffie-Hellman) arise by instantiating the three types and
+supplying the three fields. This file captures only the correctness equation; security
+assumptions belong to concrete instances.
 
-The fundamental correctness property (*agreement*) states that both parties compute the same
-shared secret:
+## Reference
 
-  sharedSecret(pub(β), α) = sharedSecret(pub(α), β)
-
-Reference:
-
-* [D. Boneh and V. Shoup,V., *A Graduate Course in Applied Cryptography*][BonehShoup],
-  Section 10.4.
+* [Boneh, Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup], Section 10.4.1
 -/
 
+namespace Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange
+
 universe u v w
 
 class KeyExchangeProtocol
@@ -46,3 +46,5 @@ class KeyExchangeProtocol
   /-- Agreement: both parties compute the same shared secret. -/
   agreement : ∀ (α β : PrivateKey),
     sharedSecret (pub β) α = sharedSecret (pub α) β
+
+end Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange

Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Diffie-Hellman.lean

@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2026 Christiano Braga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christiano Braga
+-/
+
+module
+
+public import Mathlib.Tactic
+public import Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange.Basic
+
+@[expose] public section
+
+/-!
+# Diffie-Hellman protocol
+
+Diffie-Hellman key exchange as an instance of `KeyExchangeProtocol` in a finite cyclic
+group `G` of cardinality `q` with a generator `g`. Two parties sample private keys
+`α, β : ZMod q`, publish `g ^ α.val` and `g ^ β.val`, and each raises the peer's public
+value to its own private key. Correctness: both arrive at `g ^ (α · β).val`.
+
+## Scope
+
+This file formalizes only the *correctness* (agreement) of the exchange.
+
+## Main declarations
+
+* `DiffieHellman g q hq hg` — the protocol, extending `KeyExchangeProtocol (ZMod q) G G`.
+  Two setup invariants are carried as fields:
+  - `hq : Fintype.card G = q` pins down `q` as the cardinality of `G`. This is what lets
+    private keys live in `ZMod q` faithfully: by Lagrange `x ^ Fintype.card G = 1` for every
+    `x : G`, hence `hq` gives `x ^ q = 1`, so exponents depend only on their residue
+    modulo `q`.
+  - `hg : orderOf g = q` says `g` has order `q`. Combined with `hq`, it means
+    `orderOf g = Fintype.card G`, which in a cyclic group is exactly the statement that `g`
+    is a generator.
+* `secret_eq` — `(g ^ β.val) ^ α.val = g ^ (α * β).val`: the algebraic core of agreement.
+
+## Reference
+
+* [Boneh, Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup], Section 10.4.2
+-/
+
+namespace Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange.DH
+
+open KeyExchange
+
+class DiffieHellman {G : Type u} [Group G] [Fintype G] [IsCyclic G]
+    (g : G) (q : ℕ) (hq : Fintype.card G = q) (hg : orderOf g = q)
+    extends KeyExchangeProtocol (ZMod q) G G where
+  pub α := g ^ α.val
+  sharedSecret u α := u ^ α.val
+  agreement := by
+    intro α β
+    show (g ^ β.val) ^ α.val = (g ^ α.val) ^ β.val
+    rw [← pow_mul, ← pow_mul, mul_comm]
+
+variable {G : Type u} [Group G] [Fintype G]
+variable (g : G) (q : ℕ) (hq : Fintype.card G = q)
+include hq
+
+/-- In a finite group of cardinality `q`, exponents may be reduced modulo `q`. Together with
+`ZMod.val_mul` this lets `ℕ`-valued exponents be treated as living in `ZMod q`. -/
+private lemma pow_mod_q (x : G) (n : ℕ) :
+    x ^ (n % q) = x ^ n := by
+  conv_rhs => rw [← Nat.div_add_mod n q]
+  have hxq : x ^ q = 1 := hq ▸ pow_card_eq_one
+  rw [pow_add, pow_mul, hxq, one_pow, one_mul]
+
+/-- The Diffie-Hellman shared secret `(g ^ β.val) ^ α.val` equals `g ^ (α * β).val`,
+independently of which party computes it. This is the algebraic core of `agreement`. -/
+theorem secret_eq (α β : ZMod q) :
+    (g ^ β.val) ^ α.val = g ^ (α * β).val := by
+  rw [← pow_mul, ZMod.val_mul, mul_comm β.val α.val, pow_mod_q q hq]
+
+end Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange.DH

Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/DiffieHellman.lean

@@ -264,3 +264,14 @@ @article{         ShepherdsonSturgis1963
   publisher    = {Association for Computing Machinery},
   address      = {New York, NY, USA}
 }
+
+@online{          BonehShoup,
+  author       = {Boneh, Dan and Shoup, Victor},
+  title        = {A Graduate Course in Applied Cryptography},
+  month        = {Jan.}
+  year         = {2023},
+  edition      = {Version 0.6},
+  note         = {Free online},
+  url          = {https://toc.cryptobook.us/},
+  urldate      = {2026-04-22}
+}