key: cord-0046572-bqd7jq42
authors: Hales, Thomas; Raya, Rodrigo
title: Formal Proof of the Group Law for Edwards Elliptic Curves
date: 2020-06-06
journal: Automated Reasoning
DOI: 10.1007/978-3-030-51054-1_15
sha: 4fef2ff9e7d7c5a174a8a156bdada64d832846e0
doc_id: 46572
cord_uid: bqd7jq42

This article gives an elementary computational proof of the group law for Edwards elliptic curves. The associative law is expressed as a polynomial identity over the integers that is directly checked by polynomial division. Unlike other proofs, no preliminaries such as intersection numbers, Bézout’s theorem, projective geometry, divisors, or Riemann Roch are required. The proof of the group law has been formalized in the Isabelle/HOL proof assistant.

Elliptic curve cryptography is a cornerstone of mathematical cryptography. Many cryptographic algorithms (such as the Diffie-Hellman key exchange algorithm which inaugurated public key cryptography) were first developed in the context of the arithmetic of finite fields. The preponderance of finite-field cryptographic algorithms have now been translated to an elliptic curve counterpart. Elliptic curve algorithms encompass many of the fundamental cryptographic primitives: pseudo-random number generation, digital signatures, integer factorization algorithms, and public key exchange.

One advantage of elliptic curve cryptography over finite-field cryptography is that elliptic curve algorithms typically obtain the same level of security with smaller keys than finite-field algorithms. This often means more efficient algorithms.

Elliptic curve cryptography is the subject of major international cryptographic standards (such as NIST). Elliptic curve cryptography has been implemented in widely distributed software such as NaCl [BLS12] . Elliptic curve algorithms appear in nearly ubiquitous software applications such as web browsers and digital currencies.

The same elliptic curve can be presented in different ways by polynomial equations. The different presentations are known variously as the Weierstrass curve (y 2 = cubic in x), Jacobi curve (y 2 = quartic in x), and Edwards curve (discussed below).

The set of points on an elliptic curve forms an abelian group. Explicit formulas for addition are given in detail below. The Weierstrass curve is the most familiar presentation of an elliptic curve, but it suffers from the shortcoming that the group law is not given by a uniform formula on all inputs. For example, special treatment must be given to the point at infinity and to point doubling: P → 2P . Exceptional cases are bad; they are the source of hazards such as side-channel attacks (timing attacks) by adversaries and implementation bugs [BJ02] .

Edwards curves have been widely promoted for cryptographic algorithms because their addition law avoids exceptional cases and their hazards. Every elliptic curve (in characteristic different from 2) is isomorphic to an elliptic curve in Edwards form (possibly after passing to a quadratic extension). Thus, there is little loss of generality in considering elliptic curves in Edwards form. For most cryptographic applications, Edwards curves suffice.

The original contributions of this article are both mathematical and formal. Our proof that elliptic curve addition satisfies the axioms of an abelian group is new (but see the literature survey below for prior work). Our proofs were designed with formalization specifically in mind. To our knowledge, our proof of associativity in Sect. 3.3 is the most elementary proof that exists anywhere in the published literature (in a large mathematical literature on elliptic curves extending back to Euler's work on elliptic integrals). Our proof avoids the usual machinery found in proofs of associativity (such as intersection numbers, Bézout's theorem, projective geometry, divisors, or Riemann Roch). Our algebraic manipulations require little more than multivariate polynomial division with remainders, even avoiding Gröbner bases in most places. Based on this elementary proof, we give a formal proof in the Isabelle/HOL proof assistant that every Edwards elliptic curve (in characteristic other than 2) satisfies the axioms of an abelian group. 1 It is natural to ask whether the proof of the associative law also avoids exceptional cases (encountered in Weierstrass curves) when expressed in terms of Edwards curves. Indeed, this article gives a two-line proof of the associative law for so-called complete Edwards curves that avoids case splits and all the usual machinery.

By bringing significant simplification to the fundamental proofs in cryptography, our paper opens the way for the formalization of elliptic curve cryptography in many proof assistants. Because of its extreme simplicity, we hope that our approach might be widely replicated and translated into many different proof assistants.

A number of our calculations are reworkings of calculations found in Edwards, Bernstein, Lange et al. [Edw07] , [BBJ+08] , [BL07] . A geometric interpretation of addition for Edwards elliptic curves appears in [ALNR11] .

Working with the Weierstrass form of the curve, Friedl was the first to give a proof of the associative law of elliptic curves in a computer algebra system (in Cocoa using Gröbner bases) [Fri98] , [Fri17] . He writes, "The verification of some identities took several hours on a modern computer; this proof could not have been carried out before the 1980s." These identities were later formalized in Coq with runtime one minute and 20 s [The07] . A non-computational Coq formalization based on the Picard group appears in [BS14] . By shifting to Edwards curves, we have eliminated case splits and significantly improved the speed of the computational proof.

An earlier unpublished note contains more detailed motivation, geometric interpretation, pedagogical notes, and expanded proofs [Hal16] . The earlier version does not include formalization in Isabelle/HOL. Our formalization uncovered and corrected some errors in the ideal membership problems in [Hal16] (reaffirming the pervasive conclusion that formalization catches errors that mathematicians miss).

Other formalizations of elliptic curve cryptography are found in Coq and ACL2 by different methods [Rus17] . After we posted our work to the arXiv, another formalization was given in Coq along our same idea [Erb17, EPG+17] . It goes further by including formalization of implementation of code, but it falls short of our work by not including the far more challenging and interesting case of projective curves.

We do not attempt to survey the various formalizations of cryptographic algorithms built on top of elliptic curves. Because of the critical importance of cryptography to the security industry, the formalization of cryptographic algorithms is rightfully a priority within the formalization community.

This section gives an elementary proof of the group axioms for addition on Edwards curves (Theorem 1). We include proofs, because our approach is not previously published.

Our definition of Edwards curve is more inclusive than definitions stated elsewhere. Most writers prefer to restrict to curves of genus one and generally call a curve with c = 1 a twisted Edwards curve. We have interchanged the x and y coordinates on the Edwards curve to make it consistent with the group law on the circle.

In this section, we work algebraically over an arbitrary field k. We assume a basic background in abstract algebra at the level of a first course (rings, fields, homomorphisms, and kernels). We set things up in a way that all of the main identities to be proved are identities of polynomials with integer coefficients.

All rings are assumed to be commutatative with identity 1 = 0. If R is an integral domain and if δ ∈ R, then we write R[ 1 δ ] for the localization of R with respect to the multiplicative set S = {1, δ, δ 2 , . . .}; that is, the set of fractions with numerators in R and denominators in S. We will need the well-known fact that if φ : R → A is a ring homomorphism sending δ to a unit in A, then φ extends uniquely to a map R[ 1 δ ] → A that maps a fraction r/δ i to φ(r)φ(δ i ) −1 .

Lemma 1 (kernel property). Suppose that an identity r = r 1 e 1 + r 2 e 2 + · · · + r k e k holds in a commutative ring R. If φ : R → A is a ring homomorphism such that φ(e i ) = 0 for all i, then φ(r) = 0.

We use the following rings:

. , x n , y n ]. We introduce the polynomial for the Edwards curve. Let

(1)

We write z i = (x i , y i ). We define a pair of rational functions that we denote using the symbol ⊕ 0 :

When specialized to c = 1 and d = 0, the polynomial e(x, y) = x 2 +y 2 −1 reduces to a circle, and (2) reduces to the standard group law on a circle. Commutativity is a consequence of the subscript symmetry 1 ↔ 2 evident in the pair of rational functions:

We often mark the imager = φ(r) of an element with a bar accent.

Let

gives us an inverse with properties developed below.

There is an obvious identity element (1, 0), expressed as follows. Under a homomorphism φ : R 2 [ 1 δ ] → A, mapping z 1 → P and z 2 → (1, 0), we have

. If e(P ) = 0, then P ⊕ 0 ι(P ) = (1, 0).

Proof. Plug P = (a, b) and ι P = (a, −b) into (2) and use e(P ) = 0.

Proof. This proof serves as a model for several proofs that are based on multivariate polynomial division. We write

for some polynomials r i ∈ R 2 . Concretely, the polynomials r i are obtained as the output of the one-line Mathematica command

The result now follows from the kernel property and (4); e(P 1 ) = e(P 2 ) = 0 implies φ(r) = 0, giving e(P 1 ⊕ 0 P 2 ) = 0.

Mathematica's PolynomialReduce is an implementation of a naive multivariate division algorithm [CLO92] . In particular, our approach does not require the use of Gröbner bases until Sect. 5.3. We write

where r − r is a rational function and S is a set of polynomials, to indicate that the numerator of r − r has zero remainder when reduced by polynomial division with respect to S using PolynomialReduce. We also require the denominator of r − r to be invertible in the localized polynomial ring. The zero remainder will give φ(r) = φ(r ) in each application. We extend the notation to n-tuples

to mean r i ≡ r i mod S for each i. Using this approach, most of the proofs in this article almost write themselves.

This next step (associativity) is generally considered the hardest part of the verification of the group law on curves. Our proof is two lines and requires little more than polynomial division. The polynomials δ x , δ y appear as denominators in the addition rule. The polynomial denominators Δ x , Δ y that appear when we add twice are more involved. Specifically, let (x 3 , y 3 ) = (x 1 , y 1 ) ⊕ 0 (x 2 , y 2 ), let (x 1 , y 1 ) = (x 2 , y 2 ) ⊕ 0 (x 3 , y 3 ), and set

Define Δ y analogously.

φ : R 3 [ 1 ΔxΔy ] → A be a homomor- phism with z i → P i . If e(P 1 ) = e(P 2 ) = e(P 3 ) = 0, then (P 1 ⊕ 0 P 2 ) ⊕ 0 P 3 = P 1 ⊕ 0 (P 2 ⊕ 0 P 3 ). Proof. By polynomial division in the ring R 3 [ 1 ΔxΔy ] ((x1, y1) ⊕0 (x2, y2)) ⊕0 (x3, y3) ≡ (x1, y1) ⊕0 ((x2, y2) ⊕0 (x3, y3)) mod {e1, e2, e3}.

Lemma 5 (affine closure). Let φ : R 2 → k be a homomorphism into a field k. If φ(δ) = e(P 1 ) = e(P 2 ) = 0, then eitherd orcd is a nonzero square in k.

The lemma is sometimes called completeness, in conflict with the usual definition of complete varieties in algebraic geometry. To avoid possible confusion, we avoid this terminology. We use the lemma in contrapositive form to give conditions ond andcd that imply φ(δ) = 0.

This forces φ(r) = 0, which by the form of r implies thatcd ord is a nonzero square.

We are ready to state and prove one of the main results of this article. This group law is expressed generally enough to include the group law on the circle and ellipse as a special cased = 0.

Theorem 1 (group law). Let k be a field, letc ∈ k be a square, and let d ∈ k ×2 . Then

is an abelian group with binary operation ⊕ 0 .

Proof. This follows directly from the earlier results. For example, to check associativity of P 1 ⊕ 0 P 2 ⊕ 0 P 3 , where P i ∈ C, we define a homomorphism φ : R 3 → k sending z i → P i and (c, d) → (c,d). By a repeated use of the affine closure lemma, φ(Δ y Δ x ) is nonzero and invertible in the field k. The universal property of localization extends φ to a homomorphism φ : R 3 [ 1 ΔyΔx ] → k. By the associativity lemma applied to φ, we obtain the associativity for these three (arbitrary) elements of C. The other group axioms follow similarly from the lemmas on closure, inverse, and affine closure.

The Mathematica calculations in this section are fast. For example, the associativity certificate takes about 0.12 s to compute on a 2.13 GHz processor.

In this section, we describe the proof implementation in Isabelle/HOL. We have formalized the two main theorems (Theorem 1 and Theorem 2). Formalization uses two different locales: one for the affine and one for the projective case. (The projective case will be discussed in Sect. 5.)

Let k be the underlying curve field. k is introduced as the type class field with the assumption that 2 = 0 (characteristic different from 2). This is not included in the simplification set, but used when needed during the proof. The formalized theorem is slightly less general than then informal statement, because of this restriction.

The formal proof fixes the curve parameters c, d ∈ k (dropping the bar accents from notation). The group addition ⊕ 0 (of Eq. 2) can be written as in Fig. 1 . In Isabelle's division ring theory, the result of division by zero is defined as zero. This has no impact on validity of final results, but gives cleaner simplifications in some proofs.

add :: 'a × 'a ⇒ 'a × 'a ⇒ 'a × 'a add (x 1,y 1) (x2,y 2) = ((x 1*x 2 -c*y 1*y 2) div (1-d*x 1*y 1*x 2*y 2), (x 1*y 2+y 1*x 2) div (1+d*x 1*y 1*x 2*y 2))

Most of the proofs in this section are straight-forward. The only difficulty was to combine the Mathematica certificates of computation, into a single process in Isabelle.

In Fig. 2 , we show an excerpt of the proof of associativity. We use the following abbreviations:

where e i = 0, since the involved points lie on the curve and

which stands for a normalized version of the associativity law after clearing denominators. We say that points are summable, if the rational functions defining their sum have nonzero denominators. Since the points p i are assumed to be summable, Δ x = 0. As a consequence, the property stated in Fig. 2 immediately implies that associativity holds in the first component of the addition. Briefly, the proof unfolds the relevant definitions and then normalizes to clear denominators. The remaining terms of Δ x are then distributed over addends. The unfolding and normalization of addends is repeated in the lemmas simp1gx and have " ∃ r1 r2 r3. gxpoly = r1 * e1 + r2 * e2 + r3 * e3" unfolding gxpoly_def g x_def Delta x_def apply(simp add: assms(1,2)) apply(rewrite in "_ / " delta_minus_def[symmetric])+ apply(simp add: divide_simps assms(9,11)) apply(rewrite left_diff_distrib) apply(simp add: simp1gx simp2gx) unfolding delta_plus_def delta_minus_def e1_def e2_def e3_def e_def by algebra Fig. 2 . An excerpt of the proof of associativity simp2gx. Finally, the resulting polynomial identity is proved using the algebra method. Note that no computation was required from an external tool.

The rewrite tactic, which can modify a goal with various rewrite rules in various locations (specified with a pattern), is used to normalized terms [NT14] . Rewriting in the denominators is sufficient for our needs.

For proving the resulting polynomial expression, the algebra proof method is used [CW07, Cha08, Wen19] .

where R is a commutative ring and x = (x 1 , . . . , x n ), the method verifies formulas ∀x.

The method is complete for such formulas that hold over all commutative rings with unit [Har07] .

By proving the group laws for a large class of elliptic curves, Theorem 1 is sufficiently general for many applications to cryptography. Nevertheless, to achieve full generality, we push forward.

This section shows how to remove the restrictiond ∈ k ×2 that appears in the group law in the previous section. By removing this restriction, we obtain a new proof of the group law for all elliptic curves in characteristics different from 2. Unfortunately, in this section, some case-by-case arguments are needed, but no hard cases are hidden from the reader. The level of exposition here is less elementary than in the previous section. Again, we include proofs, because our approach is designed with formalization in mind and has not been previously published.

The basic idea of our construction is that the projective curve E is obtained by gluing two affine curves E aff together. The associative property for E is a consequence of the associative property on affine pieces E aff , which can be expressed as polynomial identities.

In this section, we assume that c = 0 and that c and d are both squares. Let t 2 = d/c. By a change of variable y → y/ √ c, the Edwards curve takes the form

We assume t 2 = 1. Note if t 2 = 1, then the curve degenerates to a product of intersecting lines, which cannot be a group. We also assume that t = 0, which only excludes the circle, which has already been fully treated. Shifting notation for this new setting, let y 1 , . . . , x n , y n ].

As before, we write e i = e(z i ), z i = (x i , y i ), and e(P i ) = φ(e i ) when a homomorphism φ is given. Define rotation by ρ(x, y) = (−y, x) and inversion τ by τ (x, y) = (1/(tx), 1/(ty)).

Let G be the abelian group of order eight generated by ρ and τ .

We extend the binary operation ⊕ 0 using the automorphism τ . We also write δ 0 for δ, ν 0 for ν and so forth. Set

in R 2 [ 1 δ1 ] 2 where δ 1 = δ 1x δ 1y . We have the following easy identities of rational functions that are proved by simplification of rational functions:

inverses for σ = τ, ρ: ισ(z 1 ) = σ −1 ι(z 1 ); ι(z 1 ⊕ i z 2 ) = (ιz 1 ) ⊕ i (ιz 2 ).

(10)

coherence:

The first identity of (11) inverts δ 0 δ 1 , and the second inverts δ 1 . Proofs of (11) use polynomial division.

Let k be a field of characteristic different from two. We let E aff be the set of zeros of Eq. (6) in k 2 . Let E • ⊂ E aff be the subset of E aff with nonzero coordinates x, y = 0. We construct the projective Edwards curve E by taking two copies of E aff , glued along E • by isomorphism τ . We write [P, i] ∈ E, with i ∈ Z/2Z = F 2 , for the image of P ∈ E aff in E using the ith copy of E aff . The gluing condition gives for P ∈ E • :

The group G acts on the set E, specified on generators ρ, τ by ρ[P, i] = [ρ(P ), i] and τ [P, i] = [P, i + 1].

We define addition on E by

We will show that the addition is well-defined, is defined for all pairs of points in E, and that it gives a group law with identity element [(1, 0) , 0]. The inverse is [P, i] → [ιP, i], which is well-defined by the inverse rules (10).

Proof. Write P = (x, y). If g = ρ k = 1 G , then gP = P implies that 2x = 2y = 0 and x = y = 0 (if the characteristic is not two), which is not a point on the curve. If g = τ ρ k , then the fixed-point condition gP = P leads to 2txy = 0 or tx 2 = ty 2 = ±1. Then e(x, y) = 2(±1 − t)/t = 0, and again P is not a point on the curve.

Whenever we write P ⊕ i Q, it is always accompanied by the implicit assertion of summability; that is, (P, Q) ∈ E aff,i . There is a group isomorphism ρ → E aff \ E • given by

Lemma 7 (dichotomy). Let P, Q ∈ E aff . Then either P ∈ E • and Q = gι P for some g ∈ τ ρ , or (P, Q) ∈ E aff,i for some i. Moreover, assume that P ⊕ i Q = (1, 0) for some i, then Q = ι P .

Proof. We start with the first claim. We analyze the denominators in the formulas for ⊕ i . We have (P, Q) ∈ E aff,0 for all P or Q ∈ E aff \ E • . That case completed, we may assume that P, Q ∈ E • . Assuming δ 0 (P, Q) = δ 0x (P, Q)δ 0y (P, Q) = 0, and δ 1 (P, Q) = δ 1x (P, Q)δ 1y (P, Q) = 0, we show that Q = gιP for some g ∈ τ ρ . Replacing Q by ρQ if needed, which exchanges δ 0x ↔ δ 0y , we may assume that δ 0x (P, Q) = 0. Set τ Q = Q 0 = (a 0 , b 0 ) and P = (a 1 , b 1 ). We claim that

We describe the main polynomial identity that must be verified. Write δ , δ + , δ − for x 0 y 0 δ 0x , tx 0 y 0 δ 1x , and tx 0 y 0 δ 1y respectively, each evaluated at (P, τ (Q 0 )) = (x 1 , y 1 , 1/(tx 0 ), 1/(ty 0 )). The nonzero factors x 0 y 0 and tx 0 y 0 have been included to clear denominators, leaving us with polynomials. We have two cases ±, according to δ ± = 0. In each case, let S ± = Gröbner basis of {e 1 , e 2 , δ , δ ± }.

We have

In fact, δ = x 0 y 0 − x 1 y 1 , so that the ideal membership for this polynomial is immediate. The factors 2, 1 − t 2 , and x 0 y 0 are nonzero and can be removed from the left-hand side. These equations then immediately yield (a 0 , b 0 ) = ±(b 1 , a 1 ). This gives the needed identity: τ Q = Q 0 = (a 0 , b 0 ) = gι P , for some g ∈ ρ .

Then Q = τ gι P . The second statement of the lemma has a similar proof. Polynomial division gives for i ∈ F 2 : (x1 − x2, y1 + y2) ≡ (0, 0) mod Gröbner{e1, e2, qxδix − 1, qyδiy − 1, νiy, νix − δix}.

In fact, both x 1 −x 2 and y 1 +y 2 (which specify the condition Q = ι P ) are already members of the Gröbner basis. The fresh variables q x , q y force the denominators δ ix and δ iy to be invertible. Here the equations ν iy = ν ix − δ ix = 0 specify the sum (1, 0) = (ν ix /δ ix , ν iy /δ iy ) of Q and P .

Proof. If Q = τ ρ k ι P , then τ Q does not have the form τ ρ k ιP because the action of G is fixed-point free. By dichotomy,

works for some . Otherwise, by dichotomy P ⊕ Q is defined for some .

Lemma 9 (well-defined). Addition ⊕ given by (13) on E is well-defined.

Proof. The right-hand side of (13) is well-defined by coherence (11), provided we show well-definedness across gluings (12). We use dichotomy. If Q = τ ρ k ι P , then by an easy simplification of polynomials,

so that only one rule (16) for ⊕ applies (up to coherence (11) and inversion (8)), making it necessarily well-defined. Otherwise, coherence (11), inversion (8), and (7)) give when [Q, j] = [τ Q, j + 1]:

Theorem 2. E is an abelian group.

Proof. We have already shown the existence of an identity and inverse. We prove associativity. Both sides of the associativity identity are clearly invariant under shifts [P, i] → [P, i + j] of the indices. Thus, it is enough to show

By polynomial division, we have the following associativity identities

in the appropriate localizations, for i, j, k, ∈ F 2 . Note that (g[P 1 , i]) ⊕ [P 2 , j] = g([P 1 , i] ⊕ [P 2 , j]) for g ∈ G, as can easily be checked on generators g = τ, ρ of G, using dichotomy, (13), and (9). We use this to cancel group elements g from both sides of equations without further comment.

We claim that

The special case Q = τ ρ k ι(P ) is easy. We reduce the claim to the case where P ⊕ Q = τ ρ k Q, by applying τ to both sides of (18) and replacing P with τ P if necessary. Then by dichotomy, the left-hand side simplifies by affine associativity 17 to give the claim. Finally, we have general associativity by repeated use of dichotomy, which reduces in each case to (17) or (18).

Following the change of variables performed in Sect. 5.1, it is assumed that c = 1 and d = t 2 where t = −1, 0, 1. The resulting formalization is more challenging. In the following, some key insights are emphasized.

Gröbner Basis. The proof of Lemma 7 (dichotomy) requires solving particular instances of the ideal membership problem. Formalization caught and corrected some ideal membership errors in [Hal16] , which resulted from an incorrect interpretation of computer algebra calculations. For instance, a goal ∃r 1 r 2 r 3 r 4 . y 2 0 − x 2 1 = r 1 e(x 0 , y 0 ) + r 2 e(x 1 , y 1 ) + r 3 δ + r 4 δ − (derived from [Hal16] ) had to be corrected to ∃r 1 r 2 r 3 r 4 . 2x 0 y 0 (y 2 0 − x 2 1 ) = r 1 e(x 0 , y 0 ) + r 2 e(x 1 , y 1 ) + r 3 δ + r 4 δ − to prove (15). In another subcase, it was necessary to strengthen the hypothesis δ + = 0 to δ − = 0. Eventually, after some reworking, algebra solved the required ideal membership problems.

We defined the addition in three stages. This is convenient for some lemmas like covering (Lemma 8). First, we define the addition on projective points (Fig. 3) . Then, we add two classes of points by applying the basic addition to any pair of points coming from each class. Finally, we apply the gluing relation and obtain as a result a set of classes with a unique element, which is then defined as the resulting class (Fig. 4) .

The definitions use Isabelle's ability to encode partial functions. However, it is possible to obtain an equivalent definition more suitable for execution. In (x 1, y1) , i), ((x 2, y2) , j)). (((x 1, y1) , i), ((x 2, y2) , j)) ∈ c 1 × c 2 ∧ ((x 1, y1) , (x 2, y2)) ∈ e'_aff_0 ∪ e'_aff_1}) // gluing if c 1 ∈ e_proj and c 2 ∈ e_proj proj_addition c 1 c 2 = the_elem (proj_add_class c 1 c 2) Fig. 4 . Definition of ⊕ on classes particular, it is easy to compute the gluing relation (see lemmas e proj elim 1, e proj elim 2 and e proj aff in the formalization scripts).

Finally, since projective addition works with classes, we had to show that its definition does not depend on the representative used. 

Proof of Associativity. During formalization, we found several relations between δ expressions (see Table 1 ). While they were proven in order to show associativity, the upper group can rather be used to establish the independence of class representative and the lower group is crucial to establish the associativity law.

In particular, the lower part of the table is fundamental to the formal proof of Eq. (18). In more detail, the formal proof development showed that it was necessary to perform a dichotomy (Lemma 7) three times. The first dichotomy is performed on P , Q. The non-summable case was easy. Therefore, we set R = P ⊕ Q. On each of the resulting branches, a dichotomy on R, ιQ is performed. This time the summable cases were easy, but the non-summable case required a third dichotomy on R, τ ιQ. The non-summable case was solved using the nofixed-point theorem but for the summable subcases the following expression is Here we cannot invoke associativity because Q, τ ιQ are non-summable (lemma not add self). Instead, we use the equations from the lower part of the table and the hypothesis of the second dichotomy to get a contradiction.

We have shown that Isabelle can encompass the process of defining, computing and certifying intensive algebraic calculations. The encoding in a proof-assistant allows a better comprehension of the methods used and helps to clarify its structure.

Faster computation of the Tate pairing

Twisted Edwards curves

Weierstraß elliptic curves and side-channel attacks

Faster addition and doubling on elliptic curves

The security impact of a new cryptographic library

A formal library for elliptic curves in the Coq proof assistant

Automated methods for formal proofs in simple arithmetics and algebra

Ideals, Varieties, and Algorithms

Context aware calculation and deduction

A normal form for elliptic curves

Systematic generation of fast elliptic curve cryptography implementations

Crafting certified elliptic curve cryptography implementations in Coq

An elementary proof of the group law for elliptic curves

An elementary proof of the group law for elliptic curves

The group law for Edwards curves

Automating elementary number-theoretic proofs using Gröbner bases

Pattern-based subterm selection in Isabelle

A computationally surveyable proof of the group properties of an elliptic curve

Primality proving with elliptic curves

The Isabelle/Isar reference manual