import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point import Mathlib.Tactic -- ============================================================================ -- Elliptic Curves over Finite Fields -- ============================================================================ -- -- An elliptic curve over a field K is the set of solutions (x, y) ∈ K × K of -- the general Weierstrass equation -- y² + a₁·x·y + a₃ · y = x³ + a₂·x² + a₄·x + a₆ -- -- together with one extra "point at infinity" O. Over a field of char ≠ 2, 3 -- the cross terms a₁, a₂, a₃ can be eliminated, collapsing to the SHORT form: -- y² = x³ + a·x + b -- TODO: Demonstrate this collapse -- 𝔽₅ has char 5, so we may use the short form here. (Char of ZMod p is p — -- see Galois.lean §3.) -- -- Two extras turn this set into the object cryptography cares about: -- * a NONDEGENERACY condition (discriminant Δ ≠ 0) ruling out cusps and -- self-intersections — §2; -- * a GROUP LAW (chord-and-tangent) making the points into an abelian -- group — §4. -- -- That group is the workhorse of ECDH (§7), the elliptic-curve analog of -- DiffieHellman.lean. Same protocol, harder discrete log, smaller keys. notation "𝔽₅" => ZMod 5 instance : Fact (Nat.Prime 5) := ⟨by norm_num⟩ open WeierstrassCurve Affine -- ============================================================================ -- Section 1: Defining a curve -- ============================================================================ -- -- We pick E : y² = x³ + x + 1 over 𝔽₅. In general Weierstrass form this is -- a₁ = a₂ = a₃ = 0, a₄ = 1, a₆ = 1. abbrev E : WeierstrassCurve 𝔽₅ := { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 1 } -- ============================================================================ -- Section 2: The discriminant — keeping the curve smooth -- ============================================================================ -- -- For the short form y² = x³ + a·x + b the discriminant is -- Δ = -16 · (4a³ + 27b²). -- TODO: Clarify where this values comes from. -- -- An elliptic curve REQUIRES Δ ≠ 0 (equivalently, Δ is a unit). When Δ = 0 -- the cubic x³ + a·x + b has a repeated root and the curve develops a -- singular point — a cusp or a self-intersection — where the "tangent line" -- in §4 is no longer well-defined: -- -- smooth cusp (Δ=0) node (Δ=0) -- y²=x³+x+1 y²=x³ y²=x³+x² -- -- __/ / \ / -- / / \/ -- | < /\ -- \__ \ / \ -- \ \ / \ -- -- Geometrically Δ ≠ 0 says "the curve never crosses itself or pinches" — -- algebraically it's exactly what we need for the group law to be defined -- at every point. Without it, addition can land on a singular point with -- no tangent and the construction collapses. -- -- For our curve: Δ = -16·(4·1³ + 27·1²) = -16·31 = -496 ≡ 4 (mod 5) ≠ 0. example : IsUnit E.Δ := by decide instance : E.IsElliptic := ⟨by decide⟩ -- ============================================================================ -- Section 3: Points on the curve -- ============================================================================ -- -- A point (x, y) ∈ 𝔽₅ × 𝔽₅ is ON E iff y² = x³ + x + 1 holds in 𝔽₅. Squares -- in 𝔽₅ are {0, 1, 4}, so we sweep x = 0, 1, 2, 3, 4 and check whether the -- right-hand side lands in {0, 1, 4}. Each hit gives two y-values (±√rhs). -- (QuadraticResidues.lean gives the general theory of which elements of -- 𝔽ₚ are squares — Euler's criterion and the Legendre symbol.) -- x = 0: rhs = 0³ + 0 + 1 = 1. Squares: ±1 = {1, 4}. ⟹ (0,1), (0,4) example : (1 : 𝔽₅) ^ 2 = (0 : 𝔽₅) ^ 3 + 0 + 1 := by decide example : (4 : 𝔽₅) ^ 2 = (0 : 𝔽₅) ^ 3 + 0 + 1 := by decide -- x = 1: rhs = 1 + 1 + 1 = 3. Not a square — no points (no solution). example : ¬ ∃ y : 𝔽₅, y ^ 2 = (1 : 𝔽₅) ^ 3 + 1 + 1 := by decide -- x = 2: rhs = 8 + 2 + 1 = 11 ≡ 1. ⟹ (2,1), (2,4) example : (1 : 𝔽₅) ^ 2 = (2 : 𝔽₅) ^ 3 + 2 + 1 := by decide example : (4 : 𝔽₅) ^ 2 = (2 : 𝔽₅) ^ 3 + 2 + 1 := by decide -- x = 3: rhs = 27 + 3 + 1 = 31 ≡ 1. ⟹ (3,1), (3,4) example : (1 : 𝔽₅) ^ 2 = (3 : 𝔽₅) ^ 3 + 3 + 1 := by decide example : (4 : 𝔽₅) ^ 2 = (3 : 𝔽₅) ^ 3 + 3 + 1 := by decide -- x = 4: rhs = 64 + 4 + 1 = 69 ≡ 4. ⟹ (4,2), (4,3) example : (2 : 𝔽₅) ^ 2 = (4 : 𝔽₅) ^ 3 + 4 + 1 := by decide example : (3 : 𝔽₅) ^ 2 = (4 : 𝔽₅) ^ 3 + 4 + 1 := by decide -- Total: 8 affine points, plus the point at infinity O (introduced in §4): -- -- E(𝔽₅) = { O, (0,1), (0,4), (2,1), (2,4), (3,1), (3,4), (4,2), (4,3) } -- -- ⟹ #E(𝔽₅) = 9. We will see in §6 why this number is no surprise. -- -- Notice the SYMMETRY: every affine point appears with its mirror image -- (x, y) and (x, -y). That mirror image is exactly the group inverse (§4). -- ============================================================================ -- Section 4: The chord-and-tangent group law -- ============================================================================ -- -- The points of E form an abelian group with the following rules. Geometric -- intuition (over ℝ): to add P and Q, draw the line through them, intersect -- with the curve at a third point R', then REFLECT across the x-axis to get -- P + Q := R = -R'. -- -- P * -- ╲ -- ╲ -- ╲ * R = P + Q (below x-axis if R' above) -- * Q ⋮ -- ╲ ⋮ -- ──────────────────╲──⋮───────────────────── x-axis -- ╲ ⋮(reflect) -- ╲⋮ -- * -R' = third intersection (on curve) -- -- Three special cases: -- (a) Q = P: the "chord" degenerates to the TANGENT at P. Same recipe, -- same picture — used to compute 2P (DOUBLING, §5). -- (b) Q = -P: the line through P and -P is vertical, hits no third affine -- point, so we declare R = O, the POINT AT INFINITY. This makes O the -- group identity by fiat. -- (b') if y₁ = 0 then P = -P, so 2P = O. (Tangent formula would divide -- by zero; geometrically the tangent is vertical.) -- TODO: Remove this point? -- (c) Negation: -(x, y) = (x, -y) — reflection across the x-axis. -- -- ---------------------------------------------------------------------------- -- The formulas -- ---------------------------------------------------------------------------- -- -- For short Weierstrass y² = x³ + a·x + b, given P = (x₁,y₁), Q = (x₂,y₂): -- -- SLOPE λ = ⎧ (y₂ - y₁) / (x₂ - x₁) if x₁ ≠ x₂ (chord) -- ⎩ (3·x₁² + a) / (2·y₁) if P = Q (tangent) -- -- x₃ = λ² - x₁ - x₂ -- y₃ = λ·(x₁ - x₃) - y₁ -- -- Then P + Q = (x₃, y₃). Both branches DIVIDE — which is why we need a -- field. (Ideals.lean §9: 𝔽ₚ is a field exactly because (p) is maximal.) -- -- TODO: mention Edwards and Montgomery curves as alternatives. -- ============================================================================ -- Section 5: A worked addition in E(𝔽₅) -- ============================================================================ -- -- Take P = (0, 1) and Q = (4, 2). Since x₁ ≠ x₂ we use the chord branch. -- Recall in 𝔽₅: 4⁻¹ = 4 (because 4·4 = 16 ≡ 1). -- -- λ = (2 - 1) / (4 - 0) = 1 / 4 = 4 in 𝔽₅ -- x₃ = 4² - 0 - 4 = 16 - 4 = 12 ≡ 2 -- y₃ = 4·(0 - 2) - 1 = -9 ≡ 1 -- -- So P + Q = (2, 1). Sanity check that (2, 1) is on E (we already did this -- in §3, but here it is from the addition formula): example : ((4 : 𝔽₅) * (0 - 2) - 1) ^ 2 = ((4 : 𝔽₅) ^ 2 - 0 - 4) ^ 3 + ((4 : 𝔽₅) ^ 2 - 0 - 4) + 1 := by decide -- ---------------------------------------------------------------------------- -- Doubling: compute 2P with P = (0, 1) -- ---------------------------------------------------------------------------- -- -- Now the tangent branch (Q = P): in 𝔽₅, 2⁻¹ = 3 (because 2·3 = 6 ≡ 1). -- -- λ = (3·0² + 1) / (2·1) = 1 / 2 = 3 in 𝔽₅ -- x₃ = 3² - 0 - 0 = 9 ≡ 4 -- y₃ = 3·(0 - 4) - 1 = -13 ≡ 2 -- -- So 2P = (4, 2). Verify (4, 2) is on E from the doubling formula directly: example : ((3 : 𝔽₅) * (0 - 4) - 1) ^ 2 = ((3 : 𝔽₅) ^ 2 - 0 - 0) ^ 3 + ((3 : 𝔽₅) ^ 2 - 0 - 0) + 1 := by decide -- ============================================================================ -- Section 6: The group structure and Hasse's bound -- ============================================================================ -- -- Mathlib packages all of §4–§5 into an `AddCommGroup` instance on the type -- of points. We get +, -, 0 (= O), associativity, commutativity, inverses -- for free. (Associativity is the hard one — it's a substantial theorem.) noncomputable instance : AddCommGroup (Point E.toAffine) := inferInstance -- The identity is the point at infinity: #check (0 : Point E.toAffine) example : (0 : Point E.toAffine) = Point.zero := rfl -- ---------------------------------------------------------------------------- -- Hasse's bound -- ---------------------------------------------------------------------------- -- -- We counted 9 points in §3. Hasse (1933) says: for any elliptic curve E -- over 𝔽_p, -- -- |#E(𝔽_p) - (p + 1)| ≤ 2·√p. -- -- For p = 5: p + 1 = 6 and 2√5 ≈ 4.47, so #E(𝔽₅) ∈ [2, 10]. Our 9 lands -- comfortably in range: -- 2√5 < 5, so the inequality is `|9 - 6| ≤ 5`, i.e. `3 ≤ 5`. Equivalently, -- squaring both sides of `|#E - (p+1)| ≤ 2·√p` gives `(#E - p - 1)² ≤ 4p`: example : ((9 : ℤ) - (5 + 1)) ^ 2 ≤ 4 * 5 := by decide -- Why this matters for crypto: Hasse pins #E(𝔽_p) near p, but the EXACT -- count varies curve-by-curve. We pick curves (e.g. secp256k1) whose order -- is prime (or has a large prime factor) — that's what guarantees the -- group is cyclic of large prime order, which is what ECDLP relies on. -- ============================================================================ -- Section 7: ECDH — Diffie–Hellman on E(𝔽₅) -- ============================================================================ -- -- The DH identity from DiffieHellman.lean §3 was -- (g^b)^a = (g^a)^b in any monoid. -- -- Elliptic curves are written ADDITIVELY, so `g^n` becomes `n • P` and the -- identity becomes -- a • (b • P) = b • (a • P) -- -- Free algebra: `smul_smul` + ℕ-commutativity. Same proof shape as -- `dh_correctness` in DiffieHellman.lean §3. theorem ecdh_correctness {G : Type*} [AddCommMonoid G] (P : G) (a b : ℕ) : a • (b • P) = b • (a • P) := by calc a • (b • P) = (a * b) • P := by rw [smul_smul] _ = (b * a) • P := by rw [Nat.mul_comm] _ = b • (a • P) := by rw [← smul_smul] -- ---------------------------------------------------------------------------- -- The cyclic subgroup generated by (0, 1) -- ---------------------------------------------------------------------------- -- -- The protocol picks a public BASE POINT P of large prime order and works -- inside ⟨P⟩, the cyclic subgroup it generates. Computing once by hand -- with the formulas from §5, starting from P = (0, 1): -- -- 1P = (0, 1) 6P = (2, 4) -- 2P = (4, 2) 7P = (4, 3) -- 3P = (2, 1) 8P = (0, 4) = -P -- 4P = (3, 4) 9P = O (identity) -- 5P = (3, 1) -- -- So P has order 9 and ⟨P⟩ = E(𝔽₅). In particular E(𝔽₅) ≅ ℤ/9ℤ — a cyclic -- group (Cyclic.lean), exactly the setting ECDH needs. -- -- ---------------------------------------------------------------------------- -- Protocol — concrete run -- ---------------------------------------------------------------------------- -- -- Public: curve E, base point P. Alice's secret a = 2; Bob's secret b = 5. -- Alice sends A := 2·P = (4, 2). -- Bob sends B := 5·P = (3, 1). -- -- Shared secret: a·B = 2·(5P) = 10·P = 1·P = (0, 1) -- = b·A = 5·(2P) = 10·P = (0, 1). -- TODO: Demonstrate this with Lean -- -- Correctness is `ecdh_correctness` applied to G = Point E.toAffine. -- -- (We won't ask Lean to *evaluate* `(2 : ℕ) • P` here because the group -- instance is `noncomputable`. The protocol's CORRECTNESS holds anyway — -- it's the abstract identity above.) -- ============================================================================ -- Section 8: Why ECC dominates — ECDLP vs DLP -- ============================================================================ -- -- Same protocol as DH, three sharper properties: -- -- 1. The eavesdropper sees (P, a·P, b·P) and needs a·b·P. Recovering a -- from a·P is the ELLIPTIC-CURVE DISCRETE LOG PROBLEM (ECDLP). Unlike -- plain DLP in 𝔽_pˣ, no subexponential algorithm is known — the best -- generic attack is Pollard ρ at √n. -- -- 2. Consequence: 256-bit curve ≈ 3072-bit RSA / DH for the same security. -- Smaller keys → faster signatures, less bandwidth, less power. ECDSA -- and X25519 dominate TLS, SSH, and Bitcoin/Ethereum for this reason. -- -- 3. Curve choice matters. We need #E(𝔽_p) divisible by a large prime to -- avoid Pohlig–Hellman (which reduces ECDLP to subgroups of prime-power -- order). Standard curves (Curve25519, secp256k1, NIST P-256) are -- chosen with this — and a long list of subtler — properties in mind. -- -- ============================================================================ -- TODO: prove `E(𝔽₅) ≅ Multiplicative (ZMod 9)` (cyclicity of the point -- group), connecting this file back to Cyclic.lean. -- TODO: state Hasse's theorem as a Mathlib lemma, not just a comment. -- TODO: instantiate ECDH on a larger curve where `native_decide` can -- actually run the protocol end-to-end.