|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Christiano Braga. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Christiano Braga |
| 5 | +-/ |
| 6 | + |
| 7 | +module |
| 8 | + |
| 9 | +public import Mathlib.Tactic |
| 10 | +public import Cslib.Systems.Distributed.Protocols.Cryptographic.KeyExchange.Basic |
| 11 | + |
| 12 | +@[expose] public section |
| 13 | + |
| 14 | +/-! |
| 15 | +# Diffie-Hellman protocol |
| 16 | +
|
| 17 | +Suppose p is a large prime and that q is a large prime dividing p − 1 (think of p as being very |
| 18 | +large random prime, say 2048 bits long, and think of q as being about 256 bits long). We will be |
| 19 | +doing arithmetic mod p, that is, working in ℤₚ. Recall that ℤₚ* is the set of nonzero elements |
| 20 | +of ℤₚ. An essential fact is that since q divides p − 1, ℤₚ* has an element g of order q. |
| 21 | +This means that gᑫ = 1 and that all of the powers gᵃ, for a = 0, …, q − 1, are distinct. |
| 22 | +Let G := {gᵃ : a = 0, …, q − 1}, so that G is a subset of ℤₚ* of cardinality q. It is not hard |
| 23 | +to see that G is closed under multiplication and inversion; that is, for all u, v ∈ G, |
| 24 | +we have u·v ∈ G and u⁻¹ ∈ G. Indeed, gᵃ · gᵇ = gᵃ⁺ᵇ = gᶜ with c := (a + b) mod q, and (gᵃ)⁻¹ = gᵈ |
| 25 | +with d := (−a) mod q. In the language of algebra, G is called a subgroup of the group ℤₚ*. |
| 26 | +
|
| 27 | +For every u ∈ G and integers a and b, it is easy to see that uᵃ = uᵇ if a ≡ b mod q. |
| 28 | +Thus, the value of uᵃ depends only on the residue class of a modulo q. Therefore, |
| 29 | +if α = [a]_q ∈ ℤ_q is the residue class of a modulo q, we can define uᵅ := uᵃ and this definition |
| 30 | +is unambiguous. From here on we will frequently use elements of ℤ_q as exponents applied to |
| 31 | +elements of G. |
| 32 | +
|
| 33 | +So now we have everything we need to describe the Diffie-Hellman key exchange protocol. |
| 34 | +We assume that the description of G, including g ∈ G and q, is a system parameter that is |
| 35 | +generated once and for all at system setup time and shared by all parties involved. |
| 36 | +The protocol runs as follows: |
| 37 | +
|
| 38 | +1. Alice computes α ←ᴿ ℤ_q, u ← gᵅ, and sends u to Bob. |
| 39 | +2. Bob computes β ←ᴿ ℤ_q, v ← gᵝ, and sends v to Alice. |
| 40 | +3. Upon receiving v from Bob, Alice computes w ← vᵅ. |
| 41 | +4. Upon receiving u from Alice, Bob computes w ← uᵝ. |
| 42 | +
|
| 43 | +The secret shared by Alice and Bob is: |
| 44 | +
|
| 45 | + w = vᵅ = gᵅᵝ = uᵝ |
| 46 | +
|
| 47 | +Reference: |
| 48 | +
|
| 49 | +* [D. Boneh and V. Shoup,V., *A Graduate Course in Applied Cryptography*, One-time pad][BonehShoup], |
| 50 | + Section 10.4. |
| 51 | +-/ |
| 52 | + |
| 53 | +instance DiffieHellmanKE {G : Type u} [CommGroup G] (g : G) (q : ℕ) : |
| 54 | + KeyExchangeProtocol (ZMod q) G G where |
| 55 | + pub := fun α => g ^ α.val |
| 56 | + sharedSecret := fun u α => u ^ α.val |
| 57 | + agreement := by |
| 58 | + intro α β |
| 59 | + show (g ^ β.val) ^ α.val = (g ^ α.val) ^ β.val |
| 60 | + rw [← pow_mul, ← pow_mul, mul_comm] |
| 61 | + |
| 62 | +namespace Cslib.Systems.Distributed.Protocols.Cryptographic.DH |
| 63 | + |
| 64 | +variable {G : Type u} [CommGroup G] {q : ℕ} [Fact q.Prime] |
| 65 | +variable (g : G) (hG : ∀ x : G, x ^ q = 1) |
| 66 | +include hG |
| 67 | + |
| 68 | +/- |
| 69 | +pow_mod_q — Exponents can be reduced mod q |
| 70 | + x ^ (n % q) = x ^ n |
| 71 | +
|
| 72 | +What it says: Exponentiating by n is the same as exponentiating by n mod q. |
| 73 | +
|
| 74 | +Why it's true: By the division algorithm, n = q · (n / q) + (n mod q). So: |
| 75 | + x^n = x^(q·(n/q) + n mod q) = x^(q·(n/q)) · x^(n mod q) |
| 76 | + = (x^q)^(n/q) · x^(n mod q) = 1^(n/q) · x^(n mod q) = x^(n mod q) |
| 77 | +
|
| 78 | +Why it matters: It lets you treat ℕ-valued exponents as living in ZMod q, |
| 79 | +bridging Lean's natural number arithmetic with modular arithmetic. |
| 80 | +-/ |
| 81 | +omit [Fact q.Prime] in |
| 82 | +private lemma pow_mod_q (x : G) (n : ℕ) : x ^ (n % q) = x ^ n := by |
| 83 | + conv_rhs => rw [← Nat.div_add_mod n q] |
| 84 | + rw [pow_add, pow_mul, hG x, one_pow, one_mul] |
| 85 | + |
| 86 | +/- |
| 87 | +secret_eq — The shared secret (gᵝ)ᵅ equals g^(α·β) |
| 88 | +Computing the shared secret from the other party's public value |
| 89 | +is the same as exponentiating the generator by the product of both private keys. |
| 90 | +This is the key algebraic fact underlying the protocol — it |
| 91 | +shows the shared secret can be characterized as g^(α·β), independent of which |
| 92 | +party computes it. |
| 93 | +-/ |
| 94 | +omit [Fact q.Prime] in |
| 95 | +theorem secret_eq (α β : ZMod q) : |
| 96 | + (g ^ β.val) ^ α.val = g ^ (α * β).val := by |
| 97 | + rw [← pow_mul, ZMod.val_mul, mul_comm β.val α.val, pow_mod_q hG] |
| 98 | + |
| 99 | +end Cslib.Systems.Distributed.Protocols.Cryptographic.DH |
0 commit comments