Project topics and materials
Get Complete Project Material File(s) Now! »
Mathematical background
Elliptic curves definitions
Definition 2.1 (Projective plane). The projective plane P2 over F is the quotient P2 = (F3\(0,0,0))/∼ where (x, y, z) ∼ (x0, y0, z0) if and only if there exists a λ ∈ F∗ such that (x0, y0, z0) = (λx, λy, λz). Definition 2.2 (Curve of the projective plane). A curve of the projective plane is the set of projective points (x : y : z) whose coordinates are a solution of a homogeneous equation f(x, y, z) = 0.
A curve represented by the homogeneous equation f(x, y, z) = 0 is smooth or non-singular if the partial derivatives of f with respect to x, y, z do not all vanish simultaneously on the curve. If a curve is smooth, then there are no singular points, i.e. no cusps or nodes (self-intersections).
The definition of an elliptic curve in full generality is the following:
Definition 2.3 (Elliptic Curve). An elliptic curve E over some field F is a smooth projective plane curve over F of the form Y 2Z + a1XY Z + a3Y Z2 = X3 + a2X2Z + a4XZ2 + a6Z3
with the ai ∈ F. This form is called a Generalized Weierstrass form.
There exists a one-to-one correspondence between the projective plane P2 and the union of an affine plane F2 and the projective line at infinity. (To be more precise, there exists an isomorphism of algebraic varieties between the projective plane and the above union). Indeed, let v = (x, y, z) be a non zero vector of F3. If z =6 0 then the equivalence class of v (denoted here [v]) is [v] = [z−1v] = ( xz : yz : 1) and there exists a unique representative of the class of the form (x0, y0, 1). Hence, there is a 1-to-1 map between the set of projective points with z =6 0 and F2. If z = 0, then x and y cannot both be zero because v is a non zero vector. Moreover, if x =6 0 then [v] = [x−1v] = ( xx : xy : 0) and so there exists a unique representative of the class of the form (1, y0, 0). So, there exists a 1-to-1 map between the set of projective points with z, x =6 0 and F. If z = 0 and x = 0 then [v] = [y−1v] = [0, yy , 0] = (0 : 1 : 0). Hence, P2 =∼F2∪F∪{(0:1:0)}.
In this setting, an elliptic curve of equation Y 2Z + a1XY Z + a3Y Z2 = X3 + a2X2Z + a4XZ2 + a6Z3 in projective coordinates is isomorphic to the curve of equation y2 + a1xy + a3y = x3 + a2x2 + a4x + a6 of the affine plane, together with a separate point O called the point at infinity. A projective point of the elliptic curve with z = 0 is of the form (0 : y : 0), and since a projective point is an equivalence class, we can choose the representative (0, 1, 0) for this class. This is the point at infinity (0 : 1 : 0) in projective coordinates, which plays an important role when moving to the definition of the group law. This part is explained in details in Chapter 3.
If the characteristic of the field F is not 2 or 3, then by an appropriate change of variables [Sil09], an elliptic curve can be written in the form y2z = x3 +axz2 +bz3, where a and b are elements of F. The condition that the curve is smooth reduces to Δ = 4a3 + 27b2 =6 0.
Most of the time, when introducing elliptic curves in a cryptographic context, we use its short Weierstrass form:
Definition 2.4 (Elliptic Curve Short Weierstrass Form). An elliptic curve E over some field F with characteristic different from 2 and 3 is an affine curve of equation y2 = x3 + ax + b together with a separate point O called the point at infinity, where a, b ∈ F satisfy Δ = 4a3 + 27b2 =6 0.
In standard elliptic curve implementations we often use projective coordin-ate systems when performing cryptographic operations in order to improve performance and avoid expensive field inversions.
The below remarks are not necessary to understand the mathematics of our development and the reader may skip them, but they provide interesting context to elliptic curve theory.
Remark 1 : Isomorphisms of algebraic curves
The notion of isomorphism of curves is much stronger than bijection of sets of points, and reveals more about the relationship between two curves. One of the reasons that isomorphisms are more interesting is that they are defined by polynomials (or rational functions), so they’re something that one might actually compute while bijections are much looser. In particular, every isomorphism induces a bijection of sets of points, but the converse does not hold.
For example, if we take two 256-bit primes p and q that are very close together, then their Hasse intervals (p+ 1−2√p, p+ 1 + 2√p) and (q + 1−2√q, q + 1 + 2√q) intersect, and we can hope to find a prime r in the intersection. Then there must exist (by Deuring’s theorem) [Sch87] a curve Ep over Fp and a curve Eq over Fq such that r = #Ep(Fp) = #Eq(Fq). These groups have the same order, so there exists a bijection between them. But since the curves are defined over different fields, there is simply no way that we can efficiently realize that bijection as a polynomial mapping. In general, we cannot compute such a bijection without solving discrete logarithms which is cryptographically hard.
Remark 2 : The Projective space
The construction of the projective plane is a special case of a projective space:
Definition 2.5 (Projective space). Let F be a field. The Projective n-space over F, denoted Pn, is the set of all lines through (0, 0, …, 0) in Fn+1.
Two non zero points A = (a1, a2, …, an+1), B = (b1, b2, …, bn+1) determine the same line if there exists a λ ∈ F∗ such that ∀i, ai = λbi. Hence, we can altern-atively define the projective space Pn as the quotient set Pn = (Fn+1\(0,…,0))/∼, where (a1, a2, . . . , an+1) ∼ (b1, b2, . . . , bn+1) if and only if there exists a λ ∈ F∗ such that ai = λbi, ∀i. Elements of Pn are equivalence classes of the quotient set (i.e. lines from a geometric point of view), and are called points of the projective space. If (x1, x2, …, xn+1) is a representative of a certain class of Pn we say that (x1, x2, …, xn+1) is a set of homogeneous coordinates for this class and we denote the projective point (x1 : x2 : … : xn+1). It can be shown that there is an isomorphism between a projective n-space Pn and the union of an affine n-space and a hyperplane at infinity. More precisely, Pn =∼ Fn ∪ H∞, where H∞ = {(x1 : x2 : …, xn : xn+1) | xn+1 = 0}, i.e. H∞ =∼ Pn−1. For more details, see [Ful89].
Remark 3 : The genus of a curve
The genus of a curve can be intuitively understood as a measure of the curve’s geometric complexity.
One reasonable classification of algebraic curves could be according to the degree of the curve (i.e. the degree of the polynomial that defines the curve equation), but unfortunately it does not work for curves of higher degree. For example, let us consider the non-singular curves L : y = 0 and C : yz − x2 = 0. The curves L and C are isomorphic: There exists a mapping m : (x : y : z) 7→ (x : 0 : z) from C to L and a mapping n : (x : y : z) 7→(xz : x2 : z2) from L to C such that (m ◦ n)(x : y : z) = (x : y : z) for all (x : y : z) ∈ L and (n ◦ m)(x : y : z) = (x : y : z) for all (x : y : z) ∈ C. One would want the measure that characterizes the geometric complexity of algebraic curves to be invariant under isomorphism. Nevertheless, in this case L is of degree 1 and C is of degree 2.
The genus is a non-negative integer that can be associated to any algebraic curve and characterizes the geometric complexity of the curve. For example:
— the curve C1 : y = x has genus 0,
— the curve C2 : y2 = x2 + Bz2 has genus 0,
— the curve C3 : y2z = x3 + Axz2 + Bz3 has genus 1,
— the curve C4 : y2z2 = x4 has genus 1, and
— the curve C5 : y2z3 = x5 + xz4 has genus 2.
To compute the genus of a non-singular curve, we can use the formula (d−1)(d−2) , where d is the degree of the curve. For singular curves, which is out of scope for this thesis, see [Cas91].
A smooth projective plane curve of genus 1 is a cubic defined by a homogen-eous polynomial of the form f(x, y, z) = Ax3+By3+Cz3+Dx2y+ Ex2z+F y2x+Gy2z+Hz2x+Iz2y+Jxyz.
This is a direct consequence of the Riemann–Roch theorem which will be explained in the end of this section. An equivalent definition of an elliptic curve is the following:
Definition 2.6. An elliptic curve E over some field F is defined as a smooth projective plane curve of genus 1 together with a point O ∈ E(F).
Remark 4 : Abelian Varieties and Elliptic Curves
An alternative definition of an elliptic curve, in a more algebraic context, is that an elliptic curve is an abelian variety of dimension one. To give some intu-ition, a variety is the zeros of a set of polynomials subject to some irreducibility conditions. For a precise definition and further details, see [Ful89]. A variety of dimension one is a curve. An abelian variety is a smooth projective variety where one can define a group operation by ratio of polynomials. This operation makes the variety a commutative group. In this sense, an abelian variety of dimension one is a smooth projective curve equipped with a group operation defined by polynomial fractions, and it can be shown that every such curve is an elliptic curve.
Defining addition
From this point on, we consider fields with characteristic different from 2, 3 and so we are free to interchange between the projective and the short Weierstrass form of elliptic curves.
To understand the group law, one first needs to understand Bézout’s theorem for elliptic curves:
Lemma 2.1 (Bézout for elliptic curves). Let F be an algebraically closed field, and f ∈ F[X, Y, Z] a homogeneous polynomial of degree 3. Let E be the elliptic curve defined by the equation E : Y Z = X3 + aXZ2 + bZ3 and L a line (not contained in E). Then L ∩ E has exactly 3 points counted with multiplicity.
More precisely, a line in the projective space is the set of projective points (X : Y : Z) which are the solutions of the equation kX + lY + mZ = 0 for some k, l, m ∈ F (k, l, m not all zero). Given an elliptic curve E of equation E : Y Z = X3 + aXZ2 + bZ3, there exist three different kinds of lines:
1. the line of equation Z = 0, which intersects the elliptic curve E at the point at infinity (0 : 1 : 0) with multiplicity 3,
2. the line of equation X + cZ = 0 (with c =6 0) which intersects the elliptic curve E at the point at infinity and at the points (−c : p(−c)3 − ac + b : 1), (−c : −p(−c)3 − ac + b : 1) which may coincide, and
3. the line of equation kX + lY + lZ = 0, (with k, l, m =6 0) which intersects the elliptic curve E at three finite points of the form (x : y : 1), which may coincide. To compute the x, y we have to solve the system ( y2 = x3 + ax + bkx + ly + m = 0.
Bézout’s theorem allows us to geometrically define an operation on elliptic curve points. Let P and Q be points on an elliptic curve E, and l be the line through P and Q (or the tangent to the curve at P if P = Q). By the Bézout theorem, l intersects E at a third point, denoted by P Q. The sum P + Q is the opposite of P Q, obtained by taking the symmetric of P Q with respect to the x axis (in affine coordinates) or the point (x : −y : z) (in projective coordinates).
Table of contents :
1 Introduction
1.1 History of formal methods
1.2 Proof assistants
1.3 Use of formal methods in mathematics
1.4 Use of formal methods in cryptography
1.5 Elliptic curves and cryptography
1.6 Contribution of this thesis
2 Background
2.1 Mathematical background
2.1.1 Elliptic curves definitions
2.1.2 Defining addition
2.1.3 Riemann Roch and the group law
2.2 Use of elliptic curves in cryptography
2.2.1 Algorithms for scalar multiplication
2.2.2 Use of different coordinate systems
2.3 Coq and its Ssreflect extension
2.3.1 Propositions and Types
2.3.2 Coq by example
2.3.3 Functions and Equality
2.3.4 Inductive types
2.3.5 The Ssreflect extension
3 A formal library for elliptic curves
3.1 Elliptic curves definitions
3.2 The Picard group of divisors
3.2.1 The field of rational functions K(E)
3.2.2 Principal Divisors
3.2.3 Divisor of a line
3.2.4 The Picard Group
3.3 Linking Pic(E) to E(K)
3.4 The Projective Plane
3.5 Related work
4 A formalization of the GLV algorithm
4.1 The multi-exponentiation algorithm
4.2 The decomposition algorithm
4.3 Computing the endomorphisms
4.4 The GLV algorithm
4.5 Related work
4.6 Comments and Future work
5 Applications
5.1 Verifying GLV with CoqEAL (future work)
5.2 A Verified Library of Elliptic Curves in F
5.3 An Ssreflect library for monoidal algebras
6 Conclusion
References
