feat(Crypto/Primitives/ECC): Edwards Curves

Cslib.lean

@@ -54,6 +54,8 @@ public import Cslib.Computability.URM.Defs
 public import Cslib.Computability.URM.Execution
 public import Cslib.Computability.URM.StandardForm
 public import Cslib.Computability.URM.StraightLine
+public import Cslib.Crypto.Primitives.ECC.Basic
+public import Cslib.Crypto.Primitives.ECC.TwistedEdwardsCurve
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption

Cslib/Crypto/Primitives/ECC/Basic.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2026 Chris Anto Fröschl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Anto Fröschl
+-/
+
+module
+
+public import Cslib.Init

Cslib/Crypto/Primitives/ECC/TwistedEdwardsCurve.lean

@@ -0,0 +1,120 @@
+/-
+Copyright (c) 2026 Chris Anto Fröschl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Anto Fröschl
+-/
+
+module
+
+public import Cslib.Crypto.Primitives.ECC.Basic
+public import Mathlib.Algebra.Ring.Commute
+public import Mathlib.Data.Set.Defs
+
+/-!
+# Twisted Edwards curves
+
+This file contains the curve-level definitions that are independent of any specific Elligator.
+A twisted Edwards curve with coefficients `a` and `d` has affine equation
+`a * x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2`.
+
+The definitions are made over a commutative ring. Finiteness and the hypotheses used by a
+particular cryptographic construction belong in that construction, rather than in the definition
+of a curve or its affine points.
+
+Mathlib's elliptic-curve API is currently centred on Weierstrass models. A twisted Edwards model
+is not itself a Weierstrass equation, so using `WeierstrassCurve.Affine.Equation` here would require
+a birational coordinate conversion and extra invertibility hypotheses.  The API below follows the
+same useful separation as that API: coefficients, an affine equation, a set of affine points, and
+a bundled point type.
+
+## Main definitions
+
+* `TwistedEdwardsCurve`: the coefficients `a`, `d` of a twisted Edwards model, with its equation
+  `TwistedEdwardsCurve.Equation`, its affine points `TwistedEdwardsCurve.affinePoints` and the
+  nonsingularity condition `TwistedEdwardsCurve.IsValid`.
+* `edwardsCurve d`: the untwisted Edwards curve `x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2`.
+
+## TODO
+
+- Move into mathlib next to Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
+
+## References
+
+* [Bernstein2007a], Section 2.
+* [Bernstein2008a], Section 2, Definition 2.1.
+
+-/
+
+@[expose] public section
+namespace Cslib.Crypto.Primitives.ECC
+
+/-- Coefficients of the twisted Edwards equation
+`a * x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2`. -/
+@[ext]
+structure TwistedEdwardsCurve (R : Type*) where
+  /-- left hand side coefficient -/
+  a : R
+  /-- right hand side coefficient -/
+  d : R
+
+variable {R : Type*} [CommRing R]
+
+namespace TwistedEdwardsCurve
+
+/-- The proposition that `(x, y)` is an affine point of a twisted Edwards curve. -/
+def Equation (E : TwistedEdwardsCurve R) (x y : R) : Prop :=
+    E.a * x ^ 2 + y ^ 2 = 1 + E.d * x ^ 2 * y ^ 2
+
+/-- The set of affine coordinate pairs on a twisted Edwards curve. -/
+def affinePoints (E : TwistedEdwardsCurve R) : Set (R × R) := {p | E.Equation p.1 p.2}
+
+/-- A bundled affine point on a twisted Edwards curve. -/
+abbrev Point (E : TwistedEdwardsCurve R) := {p : R × R // p ∈ E.affinePoints}
+
+/-- The neutral affine coordinate pair `(0, 1)`.  It lies on every twisted Edwards equation. -/
+def zero : R × R := (0, 1)
+
+lemma zero_mem_affinePoints (E : TwistedEdwardsCurve R) : zero ∈ E.affinePoints := by
+  change E.a * 0 ^ 2 + 1 ^ 2 = 1 + E.d * 0 ^ 2 * 1 ^ 2
+  simp
+
+/-- The neutral point, bundled as an affine point of `E`. -/
+def zeroPoint (E : TwistedEdwardsCurve R) : E.Point := ⟨zero, E.zero_mem_affinePoints⟩
+
+/-- Negation of affine coordinates on a twisted Edwards curve. -/
+def neg (p : R × R) : R × R := (-p.1, p.2)
+
+lemma neg_mem_affinePoints (E : TwistedEdwardsCurve R) (p : R × R) :
+    neg p ∈ E.affinePoints ↔ p ∈ E.affinePoints := by
+  change E.a * (-p.1) ^ 2 + p.2 ^ 2 = 1 + E.d * (-p.1) ^ 2 * p.2 ^ 2 ↔
+    E.a * p.1 ^ 2 + p.2 ^ 2 = 1 + E.d * p.1 ^ 2 * p.2 ^ 2
+  rw [neg_sq]
+
+/-- The usual coefficient conditions for a nonsingular twisted Edwards model over a field.
+Keeping this predicate separate from `TwistedEdwardsCurve` permits the equation and its points to
+be used over more general rings and also permits partially specified curves during developments.
+-/
+def IsValid (E : TwistedEdwardsCurve R) : Prop := E.a ≠ 0 ∧ E.d ≠ 0 ∧ E.a ≠ E.d
+
+end TwistedEdwardsCurve
+
+/-- The (untwisted) Edwards curve with coefficient `d`, obtained by setting `a = 1`. -/
+def edwardsCurve (d : R) : TwistedEdwardsCurve R where
+  a := 1
+  d := d
+
+/-- The equation of `edwardsCurve d`, written out. -/
+lemma edwardsCurve_equation_iff (d x y : R) :
+    (edwardsCurve d).Equation x y ↔ x ^ 2 + y ^ 2 = 1 + d * x ^ 2 * y ^ 2 := by
+  simp [TwistedEdwardsCurve.Equation, edwardsCurve]
+
+/-- `edwardsCurve d` is a valid (nonsingular) model exactly when `d ≠ 0` and `d ≠ 1`. -/
+lemma edwardsCurve_isValid_iff [Nontrivial R] (d : R) :
+    (edwardsCurve d).IsValid ↔ d ≠ 0 ∧ d ≠ 1 := by
+  constructor
+  · rintro ⟨_, hd, had⟩
+    exact ⟨hd, fun h ↦ had h.symm⟩
+  · rintro ⟨hd, hd1⟩
+    exact ⟨one_ne_zero, hd, fun h ↦ hd1 h.symm⟩
+
+end Cslib.Crypto.Primitives.ECC

references.bib

@@ -551,3 +551,34 @@ @book{Papadimitriou94
   publisher={Addison-Wesley},
   address={Reading, Massachusetts}
 }
+
+@inproceedings{Bernstein2008a,
+  author={Daniel J. Bernstein and Peter Birkner and Marc Joye and Tanja Lange and Christiane Peters},
+  title={Twisted Edwards Curves},
+  booktitle={Progress in Cryptology - {AFRICACRYPT} 2008, First International Conference
+               on Progress in Cryptology, Casablanca, Morocco, June 11-14, 2008.
+               Proceedings},
+  series={Lecture Notes in Computer Science},
+  volume={5023},
+  isbn="978-35-40-68159-5",
+  pages= {389--405},
+  publisher={Springer Verlag, Berlin},
+  year={2008},
+  doi={10.1007/978-3-540-68164-9\_26}
+}
+
+@inproceedings{Bernstein2007a,
+  author={Bernstein, Daniel J. and Lange, Tanja},
+  title={Faster addition and doubling on elliptic curves},
+  year={2007},
+  isbn={3540768998},
+  publisher={Springer-Verlag},
+  address={Berlin, Heidelberg},
+  abstract={Edwards recently introduced a new normal form for elliptic curves. Every elliptic curve over a non-binary field is birationally equivalent to a curve in Edwards form over an extension of the field, and in many cases over the original field.This paper presents fast explicit formulas (and register allocations) for group operations on an Edwards curve. The algorithm for doubling uses only 3M + 4S, i.e., 3 field multiplications and 4 field squarings. If curve parameters are chosen to be small then the algorithm for mixed addition uses only 9M + 1S and the algorithm for non-mixed addition uses only 10M + 1S. Arbitrary Edwards curves can be handled at the cost of just one extra multiplication by a curve parameter.For comparison, the fastest algorithms known for the popular "a4=-3 Jacobian" form use 3M + 5S for doubling; use 7M + 4S for mixed addition; use 11M + 5S for non-mixed addition; and use 10M + 4S for non-mixed addition when one input has been added before.The explicit formulas for non-mixed addition on an Edwards curve can be used for doublings at no extra cost, simplifying protection against side-channel attacks. Even better, many elliptic curves (approximately 1/4 of all isomorphism classes of elliptic curves over a non-binary finite field) are birationally equivalent--over the original field--to Edwards curves where this addition algorithm works for all pairs of curve points, including inverses, the neutral element, etc.This paper contains an extensive comparison of different forms of elliptic curves and different coordinate systems for the basic group operations (doubling, mixed addition, non-mixed addition, and unified addition) as well as higher-level operations such as multi-scalar multiplication.},
+  booktitle={Proceedings of the Advances in Crypotology 13th International Conference on Theory and Application of Cryptology and Information Security},
+  pages={29–50},
+  numpages={22},
+  keywords={unified addition formulas, sidechannel countermeasures, scalar multiplication, register allocation, performance evaluation, multi-scalar multiplication, explicit formulas, elliptic curves, efficient implementation, doubling, complete addition formulas, addition},
+  location={Kuching, Malaysia},
+  series={ASIACRYPT'07}
+}