A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve

TL;DR

This paper provides an elementary, formal, and mechanically verified proof of the group properties of Curve25519, ensuring correctness of its hardware implementation for Diffie-Hellman key exchange.

Contribution

It introduces a computationally surveyable proof of elliptic curve group properties, formalized in ACL2, with steps reproducible in any programming language.

Findings

Proof is formalized and mechanically verified in ACL2.

Proof is computationally surveyable and reproducible.

Ensures correctness of hardware implementation for Diffie-Hellman.

Abstract

We present an elementary proof of the group properties of the elliptic curve known as "Curve25519", as a component of a comprehensive proof of correctness of a hardware implementation of the associated Diffie-Hellman key agreement algorithm. The entire proof has been formalized and mechanically verified with ACL2, and is computationally surveyable in the sense that all steps that require mechanical support are presented in such a way that they may readily reproduced in any suitable programming language.

Equations

$$\frac{y_{\_}{1}^2}{x_{\_}{1}^2}={\lambda }^2=x_{\_}1+A,$$

$$P_{\_}0\oplus P_{\_}0=P_{\_}0\oplus (\ominus P_{\_}1)=P_{\_}0\oplus P_{\_}1=\ominus P_{\_}1\oplus P_{\_}1=\infty ,$$

$$P_{\_}0\oplus P_{\_}0=P_{\_}0\oplus P_{\_}1=P_{\_}0\oplus (\ominus P_{\_}1)=P_{\_}0\oplus (\ominus P_{\_}0)=\infty .$$

$${\left(\frac{y_{\_}1-y_{\_}0}{x_{\_}1-x_{\_}0}\right)}^2-x_{\_}0-x_{\_}1={\left(\frac{y_{\_}1+y_{\_}0}{x_{\_}1-x_{\_}0}\right)}^2-x_{\_}0-x_{\_}1,$$

$$decode(\mathcal{P})=\left(\frac{\bar{m}}{{\bar{z}}^2},\frac{\bar{n}}{{\bar{z}}^3}\right)\in {\mathbb{F}}_{\_}{\wp }^2$$

$$z^{\prime }$$

$$w^{\prime }$$

$$m^{\prime }$$

$$n^{\prime }$$

$$z^{\prime }$$

$$m^{\prime }$$

$$n^{\prime }$$

$$\lambda =\frac{3{\left(\frac{m}{z^2}\right)}^2+2A\left(\frac{m}{z^2}\right)+1}{2\left(\frac{n}{z^3}\right)}=\frac{3m^2+2Am{z}^2+z^4}{2nz}=\frac{w^{\prime }}{z^{\prime }}.$$

$$x={\lambda }^2-A-2\left(\frac{m}{z^2}\right)=\frac{w^{\prime 2}}{z^{\prime 2}}-\frac{A{z}^2+2m}{z^2}=\frac{w^{\prime 2}}{z^{\prime 2}}-\frac{4n^2(A{z}^2+2m)}{z^{\prime 2}}=\frac{m^{\prime }}{z^{\prime 2}}$$

$$y=\lambda \left(\frac{m}{z^2}-x\right)-\frac{n}{z^3}=\frac{w^{\prime }}{z^{\prime }}\cdot \frac{4m{n}^2-m^{\prime }}{z^{\prime 2}}-\frac{8n^4}{z^{\prime 3}}=\frac{w^{\prime }(4m{n}^2-m^{\prime })-8n^4}{z^{\prime 3}}=\frac{n^{\prime }}{z^{\prime 3}}.$$

$$\lambda =\frac{y-\frac{n}{z^3}}{x-\frac{m}{z^2}}=\frac{z^{3}y-n}{z(z^{2}x-m)}=\frac{z^{3}y-n}{z^{\prime }},$$

$$x^{\prime }$$

$$y^{\prime }=\lambda (x-x^{\prime })-y=\frac{z^{3}y-n}{z^{\prime }}\cdot \frac{x{z}^{\prime 2}-m^{\prime }}{z^{\prime 2}}-\frac{z^{\prime 3}y}{z^{\prime 3}}=\frac{n^{\prime }}{z^{\prime 3}}.$$

$$evalh(norm(x,V),N)=evalp(x,A).$$

$$norm(f,V)=\text{mbox}(\mathtt{POW}ipq\text{mbox}).$$

$$norm(f,V)=\text{mbox}(\mathtt{POP}ip\text{mbox}).$$

$$x^3(4x{y}^2+3)+(2z^4+5),$$

$$x^{k}=\left\{\begin{array}[]{ll}1&\mbox{if $k=0$}\\ x\otimes x^{k-1}&\mbox{if $k>0$.}\end{array}\right.$$

$$A=\text{mbox}((v_{\_}0n_{\_}0\text{mbox})\dots \text{mbox}(v_{\_}k-1n_{\_}k-1\text{mbox})),$$

$$evalh(norm(f,V),N)=evalp(f,A).$$

$$split(h,j,k)=(pop(i,p_{\_}0),pop(i,p_{\_}1)).$$

$$split(h,j,k)=\left(pow(i,p_{\_}0,q_{\_}0),pow(i,p_{\_}1,q_{\_}1)\right);$$

$$split(h,j,k)=\left(({\Theta }^{\frac{i}{2}}\otimes p_{\_}0)\oplus pop(1,q_{\_}0),({\Theta }^{\frac{i}{2}}\otimes p_{\_}1)\oplus pop(1,q_{\_}1)\right);$$

$$split(h,j,k)=\left(({\Theta }^{\frac{i+1}{2}}\otimes p_{\_}1)\oplus pop(1,q_{\_}0),({\Theta }^{\frac{i-1}{2}}\otimes p_{\_}0)\oplus pop(1,q_{\_}1)\right).$$

$$evalh(h,{\mathcal{N}}^{(k)})$$

$$evalh(\text{mbox}(\mathtt{POW}i{p}_{\_}0q_{\_}0\text{mbox}),{\mathcal{N}}^{(k)})+y_{\_}j\cdot evalh(\text{mbox}(\mathtt{POW}i{p}_{\_}1q_{\_}1\text{mbox}),{\mathcal{N}}^{(k)})$$

$$y_{\_}{k}^{i}evalh(p_{\_}0,{\mathcal{N}}^{(k)})+evalh(q_{\_}0,{\mathcal{N}}^{(k+1)})$$

Full text

1 Introduction

An effort is under way at Intel to develop and verify a formal model and a hardware implementation of the elliptic curve key agreement algorithm known as Curve25519 [3], using ACL2. The most challenging aspect of this problem is the proof of the abelian group properties of the curve, especially associativity. This result may be viewed either as a deep theorem of algebraic or projective geometry [7, 4], accessible only to experts in that field, or as an elementary but computationally intensive arithmetic exercise, involving, as Bernstein [3] observes, “standard (but lengthy) calculations”. Silverman and Tate [11] attempt to quantify the effort with a “tongue-in-cheek estimate”:

Of course, there are a lot of cases to consider …. But in a few days you will be able to check associativity using these formulas. So we need say nothing more about the proof of the associative law!

What remains to be said is that there is compelling evidence (see below) that an elementary hand proof of this result is a practical impossibility. The first serious attack on the problem, by Friedl [5], was a combination of mathematical analysis and symbolic computation with the CoCoA (Computations in Commutative Algebra) package. Building on Friedl’s results, Théry [12] later developed a comprehensive formal proof with Coq. (Both papers address the somewhat more general class of Weierstrass curves rather than the one on which we focus here, but there is no difference in computational complexity.) These two efforts, which together represent a significant achievement, may be contrasted in the terminology of automated reasoning [2]: Friedl’s work is accepting insofar as it treats CoCoA as a trusted oracle, whereas Théry’s proof is autarkic by virtue of performing all logical deductions and supporting computations within the same formal system.

From a traditional mathematical perspective, however, both of these results are open to the same common criticism of computer-assisted proofs. There is general agreement in the mathematical community that it is desirable for a proof to be surveyable in the sense that each of its assertions could be derived manually by a competent reader as a logical consequence of preceding assertions and otherwise established results, and that the proof is short enough to be comprehended. One goal behind this principle is correctness, but equally important is the desire for mathematical growth—the propagation and advancement of techniques and ideas.

In the realm of computing, this is often an unattainable objective—reliance on a mechanical proof assistant may be unavoidable. It is common to find in a published proof in this field, in lieu of a cogent argument, an appeal to the authority of an established proof system. This device is a stark realization of Tymoczko’s allegory of the infallible Martian genius whose proclamations go unquestioned—proof by “Simon Says” [13]. It may provide evidence of correctness but does little to illuminate the underlying mathematics.

Dependence on mechanical assistance, however, need not preclude a full exposition of a proof. For example, the correctness of a hardware divider typically depends on a relation between the value and indices of each entry of an array that is too large to be either generated or checked by hand, but it should be possible to characterize the computation in such a way that it can be understood and machine-checked by the skeptical reader.

This suggests a judicious weakening of the conventional notion of surveyability. A proof may be said to be computationally surveyable if its only departure from that notion is its dependence on unproved assertions that satisfy the following criteria:

• (1)

The assertion pertains to a function for which a clear constructive definition has been provided, and merely specifies the value of that function corresponding to a concrete set of arguments.

• (2)

The computation of this value has been performed mechanically by the author of the proof in a reasonably short time.

• (3)

A competent reader could readily code the function in the programming language of his choice and verify the asserted result on his own computing platform.

Such a proof, though still objectionable to those who insist on strict surveyability, can convey a comprehensive understanding of a theorem and is susceptible to a process of social review, thus oppugning a commonly stated basis for the objection.

Neither of the treatments of the elliptic curve group properties cited above attempts such a proof, perhaps because the supporting tool or its application to the problem at hand is too complicated to admit a concise specification. Thus, Friedl simply attributes unproved results to CoCoA, while Théry’s claims depend on an undisclosed “tactic” that has reportedly been implemented in Coq.

An integrated computationally surveyable proof of a result of this sort, which combines subtle mathematical analysis with intensive computation, is best carried out with the support of an interactive prover based on an efficient executable logic. We shall present such a proof of this theorem that has been formalized and mechanically checked in its entirety with ACL2. The computational results for which we rely solely on ACL2 for verification, as opposed to proof checking, (all of which are in Section 7) are labeled as Computations, and are thus clearly distinguished from other steps in the proof, which are listed as Lemmas. All computations are performed on S-expressions and are most naturally performed in LISP, but can be readily implemented in any language that provides linked lists. Moreover, our exposition is confined to conventional mathematical terminology and notation, with no reference to the ACL2 logic.

Our proof benefits significantly from the two earlier efforts, both in its overall approach and through its appropriation of specific lemmas. In particular, we follow [12] in the representation of polynomials in sparse Horner normal form, using a normalization procedure adapted from [6]. Furthermore, our Lemmas 2.1, 2.2, and 7.7 are variants of results found in [12] (two of which are inherited from [5]).

The supporting materials for this paper include several subdirectories of books/projects in the ACL2 repository. The main script resides in curve25519. The basis of Curve25519 is the primality of $\wp=2^{255}-19$, which is proved in quadratic-reciprocity by Pratt’s method [8]and explained in [10]. Fermat’s Theorem ($a^{\wp-1}\bmod\wp=1$ when $a$ is not divisible by $\wp$), which allows the inversion operator in the field $\mathbb{F}_{\_}\wp$ to be defined as $a^{-1}=a^{\wp-2}\bmod\wp$, is also formalized in quadratic-reciprocity.

Our formalization of sparse Horner normal forms is in the subdirectory shnf. Following [6], we define an efficiently computable normalization of polynomial terms and an evaluation function on normal forms, and prove equality between the value of a polynomial and that of its representation, for all variable assignments. Thus, the equivalence of two polynomials we may be established by computing their normalizations and observing that they coincide.

Of course, the utility of this method rests on the property of completeness: equivalent polynomials always produce the same representation. According to the authors of the Coq proof, which does not address this property, it cannot even be stated within their formal framework. Our development includes a constructive proof of this result that we have formalized in ACL2, based on a function that computes, for a given pair of two polynomials, a list of variable assignments for which the values of the polynomials differ, whenever such a list exists. This result is not required for our present purpose, but is documented elsewhere [9].

The distinguishing features of our proof that enable the objective of computational surveyability are (1) a specialized rewriting procedure that reduces the normal form of a polynomial according to the curve equation (Definition 5.5), and (2) an encoding of group elements as integer triples, which facilitates symbolic computation of the group operation (Definition 6.3). Both of these functions require automated computation but admit concise specifications and correctness proofs. Furthermore, a modest improvement in efficiency over the more general Coq proof tactic is suggested by a comparison of execution times of the three computational results of [12] (9.2, 3.9, and 18.8 seconds for spec3_assoc, spec2_assoc, and spec3_assoc, respectively) and our versions of the same computations (3.78, 0.36, and 3.8 seconds for Computations 7, 8, and 9). We exploit this facility by performing several more intensive computations, thereby eliminating much of Théry’s analysis, which he characterizes as “really tedious”. In particular, Computation 10, which is proved in 26.2 seconds, disposes of a critical case of associativity. It is also worth noting that if the polynomial involved in this result were expanded into a sum of monomials, as might be done in a direct hand proof based on “standard computations”, the number of terms would exceed $10^{25}$. Clearly, the reader who completes such a proof “in a few days” is exceptionally good with figures.

2 Curve25519

Let $\wp=2^{255}-19$ and $A=486662$. The primality of $\wp$ is proved in [10]. The field of order $\wp$ is the set $\mathbb{F}_{\_}\wp=\{0,1,2,\ldots,\wp-1\}$ with the operations of addition and multiplication modulo $\wp$. Every $n\in\mathbb{Z}$ naturally corresponds to the field element $n\bmod\wp$, which we denote as $\bar{n}$. The field operations will be denoted by the usual symbols: if $x\in\mathbb{F}_{\_}\wp$, $y\in\mathbb{F}_{\_}\wp$, and $k\in\mathbb{N}$, then “$x+y$”, “$x-y$”, “$-x$”, “$xy$”, or “$x^{k}$” may refer to an operation in either $\mathbb{F}_{\_}\wp$ or $\mathbb{Z}$, depending on context, whereas “$x/y$” will only denote an operation in $\mathbb{F}_{\_}\wp$.

Definition 2.1

$EC=\{(x,y)\in\mathbb{F}_{\_}\wp\times\mathbb{F}_{\_}\wp\;|\;y^{2}=x^{3}+Ax^{2}+x\}\cup\{\infty\}$.

Our goal is to show that $EC$ is an abelian group under the following operation:

Definition 2.2

Let $P\in EC$ and $Q\in EC$.

• (1)

$P\oplus\infty=\infty\oplus P=P$.

• (2)

If $P=(x,y)$, then $P\oplus(x,-y)=\infty$.

• (3)

If $P=(x_{\_}1,y_{\_}1)$, $Q=(x_{\_}2,y_{\_}2)\neq(x_{\_}1,-y_{\_}1)$, and \lambda=\left\{\begin{array}[]{ll}\frac{y_{\_}2-y_{\_}1}{x_{\_}2-x_{\_}1}&\mbox{if x_{_}1\neq x_{_}2}\\ \frac{3x_{\_}1^{2}+2Ax_{\_}1+1}{2y_{\_}1}&\mbox{if x_{_}1=x_{_}2,}\end{array}\right. then $P\oplus Q=(x,y)$, where $x=\lambda^{2}-A-x_{\_}1-x_{\_}2$ and $y=\lambda(x_{\_}1-x)-y_{\_}1.$

Clearly, $\infty$ is the identity element, the inverse of $P=(x,y)$ is $\ominus P=(x,-y)$, and according to Corollary 1 of [10], the origin $O=(0,0)$ is the only element of order 2.

Remark. If we consider Definition 2.1 as an equation over $\mathbb{R}$ instead of $\mathbb{F}_{\_}\wp$, then Definition 2.2 admits a simple geometric interpretation. Except when $Q=\ominus P$, the line connecting points $P$ and $Q$ on the curve (or the tangent line at $P$, in case $P=Q$) intersects the curve at another point, $R$. If we were to define the operation as $P\oplus Q=\ominus R$, then analytic geometry would yield the formula in the definition. If $Q=\ominus P$, the third point of intersection is taken to be $\infty$.

In the sequel, we shall assume that $P_{\_}0=(x_{\_}0,y_{\_}0)$, $P_{\_}1=(x_{\_}1,y_{\_}1)$, and $P_{\_}2=(x_{\_}2,y_{\_}2)$ are fixed elements of $EC$ that are distinct from $\infty$ (but not necessarily from one another), in order to obviate repetition of such hypotheses. Any result pertaining to these points may be generalized by replacing them with arbitrary finite points of $EC$. We begin with two simple consequences of Definition 2.2.

Lemma 2.1

$P_{\_}0\oplus P_{\_}1\neq P_{\_}0$.

Proof: Suppose $P_{\_}0\oplus P_{\_}1=P_{\_}0$. Equating $y$-coordinates, we have $y_{\_}0=\lambda(x_{\_}0-x_{\_}0)-y_{\_}0=-y_{\_}0$, which implies $2y_{\_}0=0$ and hence (since $\mathbb{F}_{\_}\wp$ is of odd characteristic $\wp$) $y_{\_}0=0$, which implies $x_{\_}0=0$. But $x_{\_}1$ cannot be 0, as this would imply $P_{\_}0=O\oplus O=\infty$. Thus, the equation $x_{\_}0=\lambda^{2}-A-x_{\_}0-x_{\_}1$ reduces to

[TABLE]

which implies $x_{\_}1^{3}+Ax_{\_}1^{2}+x_{\_}1=y_{\_}1^{2}=x_{\_}1^{3}+Ax_{\_}1^{2}$, contradicting $x_{\_}1\neq 0$. $\Box$

Lemma 2.2

If $P_{\_}0\oplus P_{\_}1=P_{\_}0\oplus(\ominus P_{\_}1)$, then either $P_{\_}0=O$ or $P_{\_}1=O$.

Proof: If $P_{\_}0=\ominus P_{\_}1$, then

[TABLE]

which implies $P_{\_}0=O$. Similarly, if $P_{\_}0=P_{\_}1$, then

[TABLE]

Therefore, we may assume $x_{\_}0\neq x_{\_}1$. Equating the $x$-coordinates of $P_{\_}0\oplus P_{\_}1$ and $P_{\_}0\oplus(\ominus P_{\_}1)$, we have

[TABLE]

which implies $4y_{\_}0y_{\_}1=0$, and hence either $y_{\_}0=0$ or $y_{\_}1=0$. $\Box$

3 Encoding Points on the Curve as Integer Triples

Our scheme for symbolic computation of the group operation is based on a mapping from $\mathbb{Z}^{3}$ to $\mathbb{F}_{\_}\wp^{2}$:

Definition 3.1

If ${\cal P}=(m,n,z)\in\mathbb{Z}^{3}$, where $z$ is not divisible by $\wp$, then

[TABLE]

and ${\cal P}$ is said to be an encoding of $\mathit{decode}({\cal P})$.

Note that every $P=(x,y)\in\mathbb{F}_{\_}\wp^{2}$ admits the canonical encoding ${\cal P}=(x,y,1)$.

The motivation for this definition is that an encoding of $P\oplus Q$ can often be readily derived from encodings of $P$ and $Q$ in certain cases of interest. We define a partial addition operation on $\mathbb{Z}^{3}$ corresponding to Definition 2.2:

Definition 3.2

Given ${\cal P}\in\mathbb{Z}^{3}$ and ${\cal Q}\in\mathbb{Z}^{3}$, ${\cal P}\oplus{\cal Q}\in\mathbb{Z}^{3}$ is defined in two cases:

• (1)

If ${\cal P}={\cal Q}=(m,n,z)$, then ${\cal P}\oplus{\cal Q}=(m^{\prime},n^{\prime},z^{\prime})$, where

[TABLE]

• (2)

If ${\cal P}=(x,y,1)\in\mathbb{Z}^{3}$ and ${\cal Q}=(m,n,z)\neq{\cal P}$, then ${\cal P}\oplus{\cal Q}=(m^{\prime},n^{\prime},z^{\prime})$, where

[TABLE]

Lemma 3.1

Let $P=\mathit{decode}({\cal P})\in EC$ and $Q=\mathit{decode}({\cal Q})\in EC$, where ${\cal P}\oplus{\cal Q}$ is defined and if $P=Q$, then $P\neq O$ and ${\cal P}={\cal Q}$. Then $\mathit{decode}({\cal P}\oplus{\cal Q})=P\oplus Q$.

Proof: The arithmetic operations below are to be understood as operations in $\mathbb{F}_{\_}\wp$ on the field elements corresponding to the integers involved.

We first consider the case ${\cal P}={\cal Q}=(m,n,z)$. Let

[TABLE]

Then $P\oplus P=(x,y)$, where

[TABLE]

and

[TABLE]

Thus, $\mathit{decode}({\cal P}\oplus{\cal P})=\mathit{decode}(m^{\prime},n^{\prime},z^{\prime})=(x,y)=P\oplus P$.

In the remaining case, we have ${\cal P}=(m,n,z)$ and ${\cal Q}=(x,y,1)$. Let

[TABLE]

Then $P\oplus Q=(x^{\prime},y^{\prime})$, where

[TABLE]

and

[TABLE]

Thus, $\mathit{decode}({\cal P}\oplus{\cal Q})=\mathit{decode}(m^{\prime},n^{\prime},z^{\prime})=(x^{\prime},y^{\prime})=P\oplus Q$. $\Box$

4 Polynomial Terms and Sparse Horner Normal Form

In this section, we describe our formalization of sparse Horner forms as S-expressions. For this purpose, an S-expression is an integer, a symbol, or an ordered list $s=\mbox{\tt(}s_{\_}0\;s_{\_}1\;\ldots\;s_{\_}n\mbox{\tt)}$ of S-expressions. In the last case, $\mathit{head}(s)=s_{\_}0$, and for $k\in\mathbb{N}$, we define $s^{(k)}=\mbox{\tt(}s_{\_}k\;\ldots\;s_{\_}n\mbox{\tt)}$. The set of all lists whose members are confined to a set $S$ is ${\cal L}(S)$.

Under the usual ACL2 encoding of multi-variable polynomials, a polynomial term over a list $V$ of variable symbols is an S-expression constructed from integers and symbols in $V$ using the symbols +, -, *, and EXPT. The function evalp evaluates a term according to an alist that associates variables with integer values in the natural way. For example, if $V=\mbox{\tt(X Y Z)}$ and $A=\mbox{\tt((X}\;\;2\mbox{\tt) (Y}\;\;3\mbox{\tt) (Z}\;\;0\mbox{\tt))}$, then $\tau=\mbox{\tt(* X (EXPT (+ Y Z) 3))}$ is a term over $V$ and $\mathit{evalp}(\tau,A)=2\cdot(3+0)^{3}=54$. The set of all polynomial terms over $V$ is denoted ${\cal T}(V)$.

We shall represent polynomial terms as objects of the following type:

Definition 4.1

A sparse Horner form (SHF) is any of the following:

• (a)

An integer;

• (b)

A list (POP $i\;\;p$), where $i\in\mathbb{N}$ and $p$ is a SHF

• (c)

A list (POW $i\;\;p\;\;q$), where $i\in\mathbb{N}$ and $p$ and $q$ are SHFs.

A SHF is normal if its components are normal and it is not either of the following:

• (a)

(POP $i\;\;p$), where $i=0$ or $p\in\mathbb{Z}$ or $p=$(POP $j\;\;q$);

• (b)

(POW $i\;\;p\;\;q$), where $i=0$ or $p=$(POW $j\;\;r\;\;0$).

${\cal H}$* denotes the set of all normal SHFs, or SHNFs.*

The evaluation of a SHF with respect to a list of integers is defined as follows:

Definition 4.2

Let h be a SHF and let $N\in{\cal L}(\mathit{Z})$.

• (a)

If $h\in\mathbb{Z}$, then $\mathit{evalh}(h,N)=h$.

• (b)

If $h=\mbox{\tt(POP }i\;\;p\mbox{\tt)}$, then then $\mathit{evalh}(h,N)=\mathit{evalh}(p,N^{(i)})$.

• (c)

If $h=\mbox{\tt(POW }i\;\;p\;\;q\mbox{\tt)}$ and $\mathit{head}(N)=n$, then $\mathit{evalh}(h,N)=n^{i}\mathit{evalh}(p,N)+\mathit{evalh}(q,N^{(1)})$.

• (d)

If $h=\mbox{\tt(POW }i\;\;p\;\;q\mbox{\tt)}$ and $N=$(), then $\mathit{evalh}(h,N)=0$.

Our objective is to define, for a given variable list $V=$($v_{\_}0\ldots v_{\_}k$), a mapping $\mathit{norm}:{\cal T}(V)\rightarrow{\cal H}$ such that if $N=$ ($n_{\_}0\ldots n_{\_}k$) and $A=$(($v_{\_}0\;\;n_{\_}0$)$\ldots$($v_{\_}k\;\;n_{\_}k$)), then

[TABLE]

Thus, if two polynomials produce the same normal form, then they are equivalent.

A possible top-down approach to the definition of $\mathit{norm}(f,V)$ is as follows:

• (1)

If $f$ is an integer constant, then $\mathit{norm}(f,V)=f$.

• (2)

Suppose $v_{\_}0$ occurs in $f$. Find polynomials $g$ and $h$ such that $f=v_{\_}0^{i}\cdot g+h$, $g$ is not divisible by $v_{\_}0$, and $v_{\_}0$ does not occur in $h$. If $p=\mathit{norm}(g,V)$ and $q=\mathit{norm}(h,V^{(1)})$, then

[TABLE]

• (3)

Suppose $v_{\_}0$ does not occur in $f$. Let $v_{\_}i$ be the first variable in $V$ that does occur in $f$. If $p=\mathit{norm}(f,V^{(i)})$, then

[TABLE]

For example, consider the polynomial $4x^{4}y^{2}+3x^{3}+2z^{4}+5$ with variable ordering $\mbox{\tt(}x\;\;y\;\;z\mbox{\tt)}$. Rewriting the polynomial as

[TABLE]

we find that the normalization is $\mbox{\tt(POW }3\;\;p\;\;q\mbox{\tt)}$, where $p=\mathit{norm}(4xy^{2}+3,\mbox{\tt(}x\;\;y\;\;z\mbox{\tt)})$ and $q=\mathit{norm}(2z^{4}+5,\mbox{\tt(}y\;\;z\mbox{\tt)})$. Continuing recursively, we arrive at the final result:

              (POW 3 (POW 1 (POP 1 (POW 2 4 0)) 3)
                     (POP 1 (POW 4 2 5))).

It may be instructive to check that the value of this SHF for the list of values $(1\;\;2\;\;3)$, for example, and the value of the represented polynomial for the corresponding alist, are both 207.

It is not difficult to see that a SHF generated by this procedure is indeed normal. Unfortunately, this approach is impractical because of the general difficulty of constructing the polynomials $g$ and $h$ in Case (2). Our preferred definition will provide a more efficient bottom-up procedure. We begin with the two basic normalizing functions pop and pow:

Definition 4.3

Let $i\in\mathbb{N}$ and $p\in{\cal H}$.

• (a)

If $i=0$ or $p\in\mathbb{Z}$, then $\mathit{pop}(i,p)=p$.

• (b)

If $p=\mbox{\tt(POP }j\;\;q\mbox{\tt)}$, then $\mathit{pop}(i,p)=\mbox{\tt(POP }i+j\;\;q\mbox{\tt)}$.

• (c)

Otherwise, $\mathit{pop}(i,p)=\mbox{\tt(POP }i\;\;p\mbox{\tt)}$.

Definition 4.4

Let $i\in\mathbb{N}-\{0\}$, $p\in{\cal H}$, and $q\in{\cal H}$.

• (a)

If $p=0$, then $\mathit{pow}(i,p,q)=\mathit{pop}(1,q)$.

• (b)

If $p=\mbox{\tt(POW }j\;\;r\;\;0\mbox{\tt)}$, then $\mathit{pow}(i,p,q)=\mbox{\tt(POW }i+j\;\;r\;\;q\mbox{\tt)}$.

• (c)

Otherwise, $\mathit{pow}(i,p,q)=\mbox{\tt(POW }i\;\;p\;\;q\mbox{\tt)}$.

The following properties of these functions are immediate consequences of the definitions:

Lemma 4.1

Let $i\in\mathbb{N}$, $p\in{\cal H}$, $q\in{\cal H}$, and $N\in{\cal L}(\mathit{Z})$.

• (a)

$\mathit{pop}(i,p)\in{\cal H}$* and $\mathit{evalh}(\mathit{pop}(i,p),N)=\mathit{evalh}(\mbox{\tt(POP }i\;\;p\mbox{\tt)},N)$.*

• (b)

If $i\neq 0$, then $\mathit{pow}(i,p,q)\in{\cal H}$ and $\mathit{evalh}(\mathit{pow}(i,p,q),N)=\mathit{evalh}(\mbox{\tt(POW }i\;\;p\;\;q\mbox{\tt)},N)$.

We also define a ring structure on ${\cal H}$, Once we have computed the SHNFs for polynomials $x$ and $y$, the ring operations “$\oplus$” and “$\otimes$” compute those for $\mbox{\tt(+ }x\;\;y\mbox{\tt)}$ and $\mbox{\tt(* }x\;\;y\mbox{\tt)}$.

Definition 4.5

Let $x\in{\cal H}$ and $x\in{\cal H}$.

• (1)

If $x\in\mathbb{Z}$, then

• (a)

$y\in\mathbb{Z}\Rightarrow x\oplus y=x+y$* and $x\otimes y=xy$.*

• (b)

$y=\mbox{\tt(POP }i\;\;p\mbox{\tt)}\Rightarrow x\oplus y=\mbox{\tt(POP }i\;\;x\oplus p\mbox{\tt)}$* and $x\otimes y=\mathit{pop}(i,x\otimes p)$.*

• (c)

$y=\mbox{\tt(POW }i\;\;p\;\;q\mbox{\tt)}\Rightarrow x\oplus y=\mbox{\tt(POW }i\;\;p\;\;x\oplus q\mbox{\tt)}$* and $x\otimes y=\mathit{pow}(i,x\otimes p,x\otimes q)$.*

• (2)

If $y\in\mathbb{Z}$, then $x\oplus y=y\oplus x$ and $x\otimes y=y\otimes x$.

• (3)

If $x=\mbox{\tt(POP }i\;\;p\mbox{\tt)}$ and $y=\mbox{\tt(POP }j\;\;q\mbox{\tt)}$, then

• (a)

$i=j\Rightarrow x\oplus y=\mathit{pop}(i,p\oplus q)$* and $x\otimes y=\mathit{pop}(i,p\otimes q)$.*

• (b)

$i>j\Rightarrow x\oplus y=\mathit{pop}(j,\mbox{\tt(POP }i-j\;\;p\mbox{\tt)}\oplus q)$* and $x\otimes y=\mathit{pop}(j,\mbox{\tt(POP }i-j\;\;p\mbox{\tt)}\otimes q)$.*

• (c)

$i<j\Rightarrow x\oplus y=\mathit{pop}(i,\mbox{\tt(POP }j-i\;\;q\mbox{\tt)}\oplus p)$* and $x\otimes y=\mathit{pop}(i,\mbox{\tt(POP }j-i\;\;q\mbox{\tt)}\otimes p)$.*

• (4)

If $x=\mbox{\tt(POP }i\;\;p\mbox{\tt)}$ and $y=\mbox{\tt(POW }j\;\;q\;\;r\mbox{\tt)}$, then

• (a)

$i=1\Rightarrow x\oplus y=\mbox{\tt(POW }j\;\;q\;\;r\oplus p\mbox{\tt)}$* and $x\otimes y=\mbox{\tt(POW }j\;\;x\otimes q\;\;p\otimes r\mbox{\tt)}$.*

• (b)

$i>1\Rightarrow x\oplus y=\mbox{\tt(POW }j\;\;q\;\;r\oplus\mbox{\tt(POP }i-1\;\;p\mbox{\tt))}$* and $x\otimes y=\mbox{\tt(POW }j\;\;x\otimes q\;\;\mbox{\tt(POP }i-1\;\;p\mbox{\tt)}\otimes r{\tt)}$.*

• (5)

If $y=\mbox{\tt(POP }i\;\;p\mbox{\tt)}$ and $y=\mbox{\tt(POW }j\;\;q\;\;r\mbox{\tt)}$, then $x\oplus y=y\oplus x$ and $x\otimes y=y\otimes x$.

• (6)

If $x=\mbox{\tt(POW }i\;\;p\;\;q\mbox{\tt)}$ and $y=\mbox{\tt(POW }j\;\;r\;\;s\mbox{\tt)}$, then

• (a)

$i=j\Rightarrow x\oplus y=\mathit{pow}(i,p\oplus r,q\oplus s)$.

• (b)

$i>j\Rightarrow x\oplus y=\mathit{pow}(j,\mbox{\tt(POW }i-j\;\;p\;\;0\mbox{\tt)}\oplus r,q\oplus s)$**

• (c)

$i<j\Rightarrow x\oplus y=\mathit{pow}(i,\mbox{\tt(POW }j-i\;\;q\;\;0\mbox{\tt)}\oplus p,s\oplus q)$.

• (d)

$x\otimes y=\left(\mathit{pow}(i+j,p\otimes r,q\otimes s)\oplus\mathit{pow}(i,p\otimes\mathit{pop}(1,s),0)\right)\oplus\mathit{pow}(i,r\otimes\mathit{pop}(1,q),0)$.

The definitions of negation and exponentiation are straightforward:

Definition 4.6

Let $x\in{\cal H}$.

• (1)

If $x\in\mathbb{Z}$, then $\ominus x=-x$.

• (2)

If $x=\mbox{\tt(POP }i\;\;p\mbox{\tt)}$, then $\ominus x=\mbox{\tt(POP }i\;\;\ominus p\mbox{\tt)}$.

• (3)

If $x=\mbox{\tt(POW }i\;\;p\;\;q\mbox{\tt)}$, then $\ominus x=\mbox{\tt(POW }i\;\;\ominus p\;\;\ominus q\mbox{\tt)}$.

Definition 4.7

If $x\in{\cal H}$ and $k\in\mathbb{N}$, then

[TABLE]

The following properties are easily proved by induction:

Lemma 4.2

Let $x\in{\cal H}$, $y\in{\cal H}$, $N\in{\cal L}(\mathit{Z})$, and $k\in\mathbb{N}$.

• (a)

$x\oplus y\in{\cal H}$* and $\mathit{evalh}(x\oplus y,N)=\mathit{evalh}(x,N)+\mathit{evalh}(y,N)$.*

• (b)

$x\otimes y\in{\cal H}$* and $\mathit{evalh}(x\otimes y,N)=\mathit{evalh}(x,N)\cdot\mathit{evalh}(y,N)$.*

• (c)

$\ominus x\in{\cal H}$* and $\mathit{evalh}(\ominus x,N)=-\mathit{evalh}(x,N)$.*

• (d)

$x^{k}\in{\cal H}$* and $\mathit{evalh}(x^{k},N)=\mathit{evalh}(x,N)^{k}$.*

We can now define the normalization procedure:

Definition 4.8

If $x\in{\cal T}(V)$, where $V=\mbox{\tt(}v_{\_}0\ldots v_{\_}{k-1}\mbox{\tt)}$ is a list of distinct symbols, then

• (1)

$x\in\mathbb{Z}\Rightarrow\mathit{norm}(x,V)=x$.

• (2)

$x=v_{\_}i$, $0\leq i<k\Rightarrow\mathit{norm}(x,V)=\mathit{pop}(i,\mbox{\tt(POW }1\;\;1\;\;0\mbox{\tt)})$.

• (3)

$x=\mbox{\tt(- }y\mbox{\tt)}\Rightarrow\mathit{norm}(x,V)=\ominus\mathit{norm}(y,V)$.

• (4)

$x=\mbox{\tt(+ }y\;\;z\mbox{\tt)}\Rightarrow\mathit{norm}(x,V)=\mathit{norm}(y,V)\oplus\mathit{norm}(z,V)$.

• (5)

$x=\mbox{\tt(- }y\;\;z\mbox{\tt)}\Rightarrow\mathit{norm}(x,V)=\mathit{norm}(y,V)\oplus(\ominus\mathit{norm}(z,V))$.

• (6)

$x=\mbox{\tt(* }y\;\;z\mbox{\tt)}\Rightarrow\mathit{norm}(x,V)=\mathit{norm}(y,V)\otimes\mathit{norm}(z,V)$.

• (7)

$x=\mbox{\tt(EXPT }y\;\;k\mbox{\tt)}\Rightarrow\mathit{norm}(x,V)=\mathit{norm}(y,V)^{k}$.

The reader may wish to check that the SHNF for the polynomial $-z+x^{3}(z+x-3y)$ with respect to the variable list $\mbox{\tt(}x\;\;y\;\;z\mbox{\tt)}$ is once again

              (POW 3 (POW 1 (POP 1 (POW 2 4 0)) 3)
                     (POP 1 (POW 4 2 5))).

Lemma 4.3

Let $f\in{\cal T}(V)$, where $V=\mbox{\tt(}v_{\_}0\ldots v_{\_}{k-1}\mbox{\tt)}$ is a list of distinct symbols. Let $N=\mbox{\tt(}n_{\_}0\ldots n_{\_}{\ell-1}\mbox{\tt)}$ be a list of integers with $\ell\geq k$ and

[TABLE]

Then $\mathit{norm}(f,V)\in{\cal H}$ and

[TABLE]

Proof: The case $f=v_{\_}i$ follows from Definition 4.2 and Lemma 4.1; the other cases follow from Definition 4.2, induction, and Lemma 4.2. $\Box$

5 Polynomial Reduction

We shall focus on the case of a list of variables corresponding to the coordinates of the points $P_{\_}0$, $P_{\_}1$, and $P_{\_}2$, as characterized in Section 2. We define the following lists:

Definition 5.1

${\cal V}=$(Y0 Y1 Y2 X0 X1 X2), ${\cal N}=$($y_{\_}0\;\;y_{\_}1\;\;y_{\_}2\;\;x_{\_}0\;\;x_{\_}1\;\;x_{\_}2$), and

${\cal A}=$((Y0 $y_{\_}0$) (Y1* $y_{\_}1$) (Y2 $y_{\_}2$) (X0 $x_{\_}0$) (X1 $x_{\_}1$) (X2 $x_{\_}2$))*

We abbreviate ${\cal T}({\cal V})$ as ${\cal T}$, and for $\tau\in{\cal T}$ we abbreviate $\mathit{evalp}(\tau,{\cal A})$ as $\hat{\tau}$.

The ordering of the variable list ${\cal V}$ is designed to maximize the efficiency of the rewriting procedure defined below. This procedure operates on a SHF that represents a polynomial with respect to ${\cal V}$, which is effectively reduced, using the curve equation as a rewrite rule, to a polynomial that (a) has the same value (modulo $\wp$) as the given polynomial under the variable assignments of ${\cal A}$ and (b) is at most linear in each of the variables Y$i$.

The core of the rewriter is the function split, which reduces and splits a polynomial term $\tau$ into a sum of two polynomials, of which one is independent of a given Y$j$ and the other is linear in Y$j$. More precisely, if $h=\mathit{norm}(\tau,{\cal V}^{(k)})$ and $0\leq k\leq j\leq 3$, then $\mathit{split}(h,j,k)$ computes a pair of SHNFs that represent these polynomials.

The following SHNF is used in the reduction:

Definition 5.2

$\Theta=$(POP $3$ (POW $1$ (POW $1$ (POW $1\;\;1\;\;A$) $1$) [math])).

Lemma 5.1

If $j\in\{0,1,2\}$, then $\mathit{evalh}(\Theta,{\cal N}^{(j)})=x_{\_}j^{3}+Ax_{\_}j^{2}+x_{\_}j\equiv y_{\_}j^{2}\pmod{\wp}$.

Proof: This may be derived by expanding the definition of evalh. $\Box$

Definition 5.3

Let $h\in{\cal H}$, $j\in\{0,1,2\}$, and $k\in\mathbb{N}$.

• (1)

If $h\in\mathbb{Z}$ or $j<k$, then $\mathit{split}(h,j,k)=(h,0)$.

• (2)

If $j\geq k$, $h=$(POP $i\;\;p$), and $(p_{\_}0,p_{\_}1)=\mathit{split}(p,j,k+i)$, then

[TABLE]

• (3)

Let $h=$(POW$\;i\;p\;q$), $(p_{\_}0,p_{\_}1)=\mathit{split}(p,j,k)$, and $(q_{\_}0,q_{\_}1)=\mathit{split}(q,j,k+1)$.

• (a)

If $j>k$, then

[TABLE]

• (b)

If $j=k$ and $i$ is even, then

[TABLE]

• (c)

If $j=k$ and $i$ is odd, then

[TABLE]

Lemma 5.2

Let $(h_{\_}0,h_{\_}1)=\mathit{split}(h,j,k)$, where $h\in{\cal H}$, $j\in\{0,1,2\}$, and $k\in\mathbb{N}$. Then $\mathit{evalh}(h,{\cal N}^{(k)})\equiv\mathit{evalh}(h_{\_}0,{\cal N}^{(k)})+y_{\_}j\cdot\mathit{evalh}(h_{\_}1,{\cal N}^{(k)})\pmod{\wp}$.

Proof: We may assume that $j\geq k$; otherwise the claim is trivial. The proof is by induction on the structure of $h$. The case $h=$(POP $i\;\;p$) is straightforward:

[TABLE]

Suppose $h=$(POW $i\;\;p\;\;q$). By the definition of evalh,

[TABLE]

If $j>k$, then this may be written as

[TABLE]

We may assume, therefore, that $j=k$. If $i$ is even, then

[TABLE]

and similarly,

[TABLE]

if $i$ is odd, then we may rearrange the above expression for $\mathit{evalh}(h,{\cal N}^{(k)})$ as

[TABLE]

which similarly reduces to $\mathit{evalh}(h_{\_}0,{\cal N}^{(k)})+y_{\_}j\cdot\mathit{evalh}(h_{\_}1,{\cal N}^{(k)})$. $\Box$

Definition 5.4

If $h\in{\cal H}$, $j\in\{0,1,2\}$, and $(h_{\_}0,h_{\_}1)=\mathit{split}(h,j,0)$, then

[TABLE]

Lemma 5.3

If $h\in{\cal H}$, $j\in\{0,1,2\}$, and $r=\mathit{rewrite}(h,j)$, then $\hat{r}\equiv\hat{h}\pmod{\wp}$.

Proof: We instantiate Lemma 5.2 with $k=0$ and invoke Lemma 4.2. $\Box$

Definition 5.5

If $\sigma\in{\cal T}$, then

[TABLE]

Lemma 5.4

If $\mathit{reduce}(\sigma)=\mathit{reduce}(\tau)$, then $\hat{\sigma}\equiv\hat{\tau}\pmod{\wp}$.

Proof: This is a consequence of Lemmas 5.3 and 4.3). $\Box$

6 Encoding Points on the Curve as Term Triples

The evaluation of terms induces a mapping from ${\cal T}^{3}$ to $\mathbb{F}_{\_}\wp^{2}$:

Definition 6.1

For $\Pi=(\mu,\nu,\zeta)\in{\cal T}^{3}$, $\hat{\Pi}=(\hat{\mu},\hat{\nu},\hat{\zeta})$ and if $\hat{\zeta}$ is not divisible by $\wp$, then $\mathit{decode}(\Pi)=\mathit{decode}(\hat{\Pi})$.

Clearly, under the following definitions, $\mathit{decode}(\Omega)=O$ and $\mathit{decode}(\Pi_{\_}i)=P_{\_}i$.

Definition 6.2

$\Omega=(0,0,1)$* and for $i\in\{0,1,2\}$, $\Pi_{\_}i=(\mbox{\tt X}i,\mbox{\tt Y}i,1)$.

Definition 3.2 suggests a partial addition on ${\cal T}^{3}$ corresponding to the group operation on $EC$. This in combination with normalization (Definition 4.8) and reduction (Definition 5.5) will provide a practical means of establishing equivalence between expressions constructed from the above points by nested applications of $\oplus$, while avoiding the intractable task of explicitly computing those expressions.

Definition 6.3

For $\Pi\in{\cal T}^{3}$ and $\Lambda\in{\cal T}^{3}$, $\Pi\oplus\Lambda\in{\cal T}^{3}$ is defined in the following cases:

• (1)

If $\Pi=\Lambda=(\mu,\nu,\zeta)$, then $\Pi\oplus\Lambda=(\mu^{\prime},\nu^{\prime},\zeta^{\prime})$, where

[TABLE]

[TABLE]

[TABLE]

[TABLE]

• (2)

If $\Pi=(\theta,\phi,1)$ and $\Lambda=(\mu,\nu,\zeta)\neq\Pi$, then $\Pi\oplus\Lambda=(\mu^{\prime},\nu^{\prime},\zeta^{\prime})$, where

[TABLE]

[TABLE]

[TABLE]

Lemma 6.1

Let $\Pi\in{\cal T}^{3}$ and $\Lambda\in{\cal T}^{3}$ with $\mathit{decode}(\Pi)=P\in EC$, $\mathit{decode}(\Lambda)=Q\in EC$, and $\Pi\oplus\Lambda$ defined. Assume that if $\Pi=\Lambda$, then $P=Q\neq O$, and otherwise $P\neq Q$. Then $\mathit{decode}(\Pi\oplus\Lambda)=P\oplus Q$.

Proof: Let $\Gamma=\Pi\oplus\Lambda$. Clearly, the hypothesis implies that $\hat{\Pi}\oplus\hat{\Lambda}$ is defined. In light of Lemma 3.1, we need only show that $\hat{\Gamma}=\hat{\Pi}\oplus\hat{\Lambda}$.

We shall examine the case $\Pi=\Lambda$; the remaining case is similar. Let $\Pi=(\mu,\nu,\zeta)$, $\Lambda=(\mu^{\prime},\nu^{\prime},\zeta^{\prime})$, and

[TABLE]

According to Definition 6.3,

$\zeta^{\prime}=$ (* 2 (* $\nu\;\;\zeta$))

and it is clear from the definition of evalp that

[TABLE]

It may similarly be shown that $\hat{\mu}=m_{\_}{dbl}({\cal P})$ and $\hat{\nu}=n_{\_}{dbl}({\cal P})$. Thus,

[TABLE]

We also define a negation operator, with the obvious property:

Definition 6.4

For $\Pi=(\mu,\nu,\zeta)\in{\cal T}^{3}$, $\ominus\Pi=(\mu,\mbox{\tt(- }\nu\mbox{\tt)},\zeta)$.

Lemma 6.2

If $\Pi\in{\cal T}^{3}$ and $\mathit{decode}(\Pi)\in EC$, then $\mathit{decode}(\ominus\Pi)=\ominus P$.

The next two lemmas, which combine the results of this section with those of Section 5, will be critical in establishing the group axioms: Lemma 6.3 for closure and Lemma 6.4 for commutativity and associativity.

Definition 6.5

Given $\Pi=(\mu,\nu,\zeta)\in{\cal T}^{3}$, let

$\tau\ =$ (- (EXPT $\nu$ $2$)              (+ (EXPT $\mu$ $3$)                 (+ (* $A$ (EXPT (* $\mu$ $\zeta$) $2$))                    (* $\mu$ (EXPT $\zeta$ $4$))))).Then $\Pi$ is an EC-encoding if $\mathit{reduce}(\tau)=0$.

Lemma 6.3

If $\Pi$ is an EC-encoding and $P=\mathit{decode}(\Pi)$, then $P\in EC$.

Proof: Let $\Pi=(\mu,\nu,\zeta)$, $\hat{\Pi}=(m,n,z)$, and $P=(x,y)=\mathit{decode}(\Pi)$. Then

[TABLE]

and

[TABLE]

By Lemma 5.4, $\hat{\tau}\equiv 0\pmod{\wp}$, and therefore, in the field $\mathbb{F}_{\_}\wp$,

[TABLE]

Dividing this equation by $\bar{z}^{6}$ yields

[TABLE]

Definition 6.6

Given $\Pi=(\mu,\nu,\zeta)\in{\cal T}^{3}$ and $\Pi^{\prime}=(\mu^{\prime},\nu^{\prime},\zeta^{\prime})\in{\cal T}^{3}$, let

$\sigma=$(* $\mu$ (EXPT * $\zeta^{\prime}\;\;2$ )),**    ** $\sigma^{\prime}=$( $\mu^{\prime}$ (EXPT * $\zeta\;\;2$ )),*

$\tau=$(* $\nu$ (EXPT * $\zeta^{\prime}\;\;3$ )),**    ** $\tau^{\prime}=$( $\nu$ (EXPT * $\zeta\;\;3$ )).*

Then $\Pi\sim\Pi^{\prime}\Leftrightarrow\mathit{reduce}(\sigma)=\mathit{reduce}(\sigma^{\prime})\mbox{ and }\mathit{reduce}(\tau)=\mathit{reduce}(\tau^{\prime})$.

Lemma 6.4

Let $\Pi\in{\cal T}^{3}$ and $\Pi^{\prime}\in{\cal T}^{3}$. If $\mathit{decode}(\Pi)=P\in EC$, $\mathit{decode}(\Pi^{\prime})=P^{\prime}\in EC$, and $\Pi\sim\Pi^{\prime}$, then $P=P^{\prime}$.

Proof: Let $\Pi=(\mu,\nu,\zeta)$, $\Pi^{\prime}=(\mu^{\prime},\nu^{\prime},\zeta^{\prime})$, $\hat{\Pi}=(m,n,z)$, and $\hat{\Pi^{\prime}}=(m^{\prime},n^{\prime},z^{\prime})$. Then by Lemma 5.4,

[TABLE]

and

[TABLE]

Thus, in the field $\mathbb{F}_{\_}\wp$,

[TABLE]

7 Abelian Group Axioms

It must be shown that if $\{P,Q,R\}\subset EC$, then $P\oplus Q=Q\oplus P\in EC$ and $(P\oplus Q)\oplus R=P\oplus(Q\oplus R)$. We may assume that the points are finite, since each of these properties is trivial otherwise, and without loss of generality, we may confine our attention to the fixed points $P_{\_}0$, $P_{\_}1$, and $P_{\_}2$.

Computations 1–11 below are computational results of evaluating the functions that are specified by Definitions 5.5 (term reduction), 6.3 (addition of term triples), 6.4 (negation of a term triple), 6.5 (EC-encoding recognizer), and 6.6 (equivalence of term triples). The lemmas of this section are derived from these results using the corresponding Lemmas 5.4, 6.1, 6.2, 6.3, and 6.4.

Computation 1

$\Pi_{\_}0\oplus\Pi_{\_}0$* and $\Pi_{\_}0\oplus\Pi_{\_}1$ are EC-encodings.*

Lemma 7.1** (Closure)**

$P_{\_}0\oplus P_{\_}1\in EC$.

Proof: If $P_{\_}0\neq P_{\_}1$, then by Computation 1, Definition 6.2 and Lemmas 6.1,

[TABLE]

and by Lemma 6.3, $P_{\_}0\oplus P_{\_}1\in EC$. Similarly, $P_{\_}0\oplus P_{\_}0\in EC$. $\Box$

Computation 2

$\Pi_{\_}0\oplus\Pi_{\_}1\sim\Pi_{\_}1\oplus\Pi_{\_}0$.

Lemma 7.2** (Commutativity)**

$P_{\_}0\oplus P_{\_}1=P_{\_}1\oplus P_{\_}0$.

Proof: We may assume $P_{\_}0\neq P_{\_}1$. By Computation 2 and Lemmas 6.1 and 6.4,

[TABLE]

All remaining results pertain to associativity.

Computation 3

$\ominus(\Pi_{\_}0\oplus\Pi_{\_}0)\sim(\ominus\Pi_{\_}0)\oplus(\ominus\Pi_{\_}0)$.

Computation 4

$\ominus(\Pi_{\_}0\oplus\Pi_{\_}1)\sim(\ominus\Pi_{\_}0)\oplus(\ominus\Pi_{\_}1)$.

Lemma 7.3

$\ominus(P_{\_}0\oplus P_{\_}1)=(\ominus P_{\_}0)\oplus(\ominus P_{\_}1)$.

Proof: This follows from Computations 3 and 4 and Lemmas 5.4, 6.1, 6.2, and 6.4. $\Box$

Computation 5

$(\ominus\Pi_{\_}0)\oplus(\Pi_{\_}0\oplus\Pi_{\_}0)\sim\Pi_{\_}0$.

Computation 6

$(\ominus\Pi_{\_}0)\oplus(\Pi_{\_}0\oplus\Pi_{\_}1)\sim\Pi_{\_}1.$**

Lemma 7.4

If $P_{\_}0\oplus P_{\_}1\neq\ominus P_{\_}0$, then $(\ominus P_{\_}0)\oplus(P_{\_}0\oplus P_{\_}1)=P_{\_}1$.

Proof: This follows similarly from Computations 5 and 6. $\Box$

Computation 7

$\Pi_{\_}2\oplus(\Pi_{\_}0\oplus\Pi_{\_}1)\sim\Pi_{\_}1\oplus(\Pi_{\_}0\oplus\Pi_{\_}2)$.

Computation 8

$\Pi_{\_}1\oplus(\Pi_{\_}0\oplus\Pi_{\_}0)\sim\Pi_{\_}0\oplus(\Pi_{\_}0\oplus\Pi_{\_}1)$.

Lemma 7.5

If $P_{\_}0\oplus P_{\_}1\notin\{P_{\_}2,\ominus P_{\_}2\}$ and $P_{\_}0\oplus P_{\_}2\notin\{P_{\_}1,\ominus P_{\_}1\}$, then

[TABLE]

Proof: The claim follows immediately from Computations 7 and 8 and Lemmas 5.4,  6.1, and 6.4 except in the cases $P_{\_}0=\ominus P_{\_}1$, $P_{\_}0=P_{\_}1=O$, $P_{\_}0=\ominus P_{\_}2$, and $P_{\_}0=P_{\_}2=O$. We need only consider the first two of these cases; the other two are similar. Moreover, since $\ominus O=O$, the second case is subsumed by the first. Thus, we may assume $P_{\_}0=\ominus P_{\_}1$. Now $LHS$ (the left-hand side) is $P_{\_}2$ and by Lemma 7.4, $RHS=(\ominus P_{\_}0)\oplus(P_{\_}0\oplus P_{\_}2)=P_{\_}2=LHS$. $\Box$

Computation 9

$(\Pi_{\_}0\oplus\Pi_{\_}0)\oplus(\Pi_{\_}0\oplus\Pi_{\_}0)\sim\Pi_{\_}0\oplus(\Pi_{\_}0\oplus(\Pi_{\_}0\oplus\Pi_{\_}0))$.

Computation 10

$(\Pi_{\_}0\oplus\Pi_{\_}1)\oplus(\Pi_{\_}0\oplus\Pi_{\_}1)\sim\Pi_{\_}0\oplus(\Pi_{\_}1\oplus(\Pi_{\_}0\oplus\Pi_{\_}1))$.

Lemma 7.6

If $P_{\_}0\oplus P_{\_}1\neq-(P_{\_}0\oplus P_{\_}1)$, $P_{\_}0\oplus P_{\_}1\neq\ominus P_{\_}1$, and $P_{\_}1\oplus(P_{\_}0\oplus P_{\_}1)\notin\{P_{\_}0,\ominus P_{\_}0\}$, then $(P_{\_}0\oplus P_{\_}1)\oplus(P_{\_}0\oplus P_{\_}1)=P_{\_}0\oplus(P_{\_}1\oplus(P_{\_}0\oplus P_{\_}1))$.

Proof: The case $P_{\_}0=\ominus P_{\_}1$ is trivial and the case $P_{\_}1=P_{\_}0\oplus P_{\_}1$ is precluded by Lemma 2.1. All other cases are handled by Computations 9 and 10 and Lemmas 5.4, 6.1, and 6.4. $\Box$

Computation 11

Let $\Sigma=\Pi_{\_}0\oplus\Pi_{\_}1=(\mu,\nu,\zeta)$, $\Sigma^{\prime}=\Pi_{\_}0\oplus\Pi_{\_}0=(\mu^{\prime},\nu^{\prime},\zeta^{\prime})$,

[TABLE]

and

[TABLE]

Then $\mathit{reduce}(\phi)=\mathit{reduce}(\psi)$.

Lemma 7.7

If $P_{\_}0\oplus P_{\_}1=\ominus P_{\_}0$, then $P_{\_}1=\ominus(P_{\_}0\oplus P_{\_}0)$.

Proof: First note that we may assume that $P_{\_}0\notin\{P_{\_}1,\ominus P_{\_}1\}$, for if $P_{\_}0=P_{\_}1$, then

[TABLE]

and if $P_{\_}0=\ominus P_{\_}1$, then

[TABLE]

contradicting $P_{\_}0\neq\infty$. Furthermore, if $P_{\_}0=\ominus P_{\_}0$, then $P_{\_}0\oplus P_{\_}1=P_{\_}0$, contradicting Lemma 2.1. Thus, we have $x_{\_}0\neq x_{\_}1$ and $y_{\_}0\neq 0$.

Retaining the notation of Computation 11, let

[TABLE]

and

[TABLE]

It follows from the definition of evalp that

[TABLE]

and

[TABLE]

By Lemma 6.1,

[TABLE]

and hence $m\equiv x_{\_}0z^{2}\pmod{\wp}$, which implies $\hat{\phi}\equiv 0\pmod{\wp}$.

By Computation 11 and Lemma 5.4, $\hat{\psi}\equiv 0\pmod{\wp}$, which implies $m^{\prime}\equiv x_{\_}1z^{\prime 2}\pmod{\wp}$. Thus, by Lemma 6.1,

[TABLE]

which implies $P_{\_}0\oplus P_{\_}0\in\{P_{\_}1,\ominus P_{\_}1\}$. We need only consider the case $P_{\_}0\oplus P_{\_}0=P_{\_}1$.

Suppose that $P_{\_}0\oplus P_{\_}0=P_{\_}1$. Then $P_{\_}0\oplus P_{\_}0\neq\ominus P_{\_}0$, and by Lemma 7.10,

[TABLE]

Thus,

[TABLE]

By Lemma 2.2, $P_{\_}1=O$, and hence $P_{\_}1=\ominus P_{\_}1=\ominus(P_{\_}0\oplus P_{\_}0)$. $\Box$

Lemma 7.8

If $P_{\_}0\oplus P_{\_}1=\ominus P_{\_}2$, then $(P_{\_}0\oplus P_{\_}1)\oplus P_{\_}2=P_{\_}0\oplus(P_{\_}1\oplus P_{\_}2)$.

Proof: $LHS=\infty$ and by Lemma 7.3,

[TABLE]

Therefore, we must show that $P_{\_}1\oplus((\ominus P_{\_}0)\oplus(\ominus P_{\_}1))=\ominus P_{\_}0$.

If $(\ominus P_{\_}0)\oplus(\ominus P_{\_}1)\neq P_{\_}1$, then this follows from Lemma 7.4. On the other hand, if $(\ominus P_{\_}0)\oplus(\ominus P_{\_}1)=P_{\_}1$, then by Lemmas 7.7 and 7.3,

[TABLE]

Lemma 7.9

$(P_{\_}0\oplus P_{\_}0)\oplus P_{\_}1=P_{\_}0\oplus(P_{\_}0\oplus P_{\_}1)$.

Proof: By Lemma 7.8, we may assume $P_{\_}0\oplus P_{\_}1\neq\ominus P_{\_}0$ and $P_{\_}0\oplus P_{\_}0\neq\ominus P_{\_}1$. By Lemmas 2.1 and 7.5, we may assume that $P_{\_}1=P_{\_}0\oplus P_{\_}1$.

If $P_{\_}1=\ominus P_{\_}0$, then

[TABLE]

But if $P_{\_}1\neq\ominus P_{\_}0$, then the claim follows from Lemma 7.6. $\Box$

Two final computations are required for the case $P_{\_}1=O$ and $P_{\_}2=P_{\_}0\oplus P_{\_}1$:

Computation 12

$(\Pi_{\_}0\oplus\Omega)\oplus(\Pi_{\_}0\oplus\Omega)\sim\Pi_{\_}0\oplus\Pi_{\_}0$.

Computation 13

$\Omega\oplus(\Pi_{\_}0\oplus\Omega)\sim\Pi_{\_}0$.

Lemma 7.10

$(P_{\_}0\oplus O)\oplus(P_{\_}0\oplus O)=P_{\_}0\oplus(O\oplus(P_{\_}0\oplus O))$.

Proof: We may assume that $P_{\_}0\neq O$. Since Lemma 2.1 implies $P_{\_}0\oplus O\neq O$, it follows from Computation 13 that $O\oplus(P_{\_}0\oplus O)=P_{\_}0$. Thus, the claim reduces to $(P_{\_}0\oplus O)\oplus(P_{\_}0\oplus O)=P_{\_}0\oplus P_{\_}0$, which follows from Computation 12. $\Box$

Lemma 7.11** (Associativity)**

$(P_{\_}0\oplus P_{\_}1)\oplus P_{\_}2=P_{\_}0\oplus(P_{\_}1\oplus P_{\_}2)$.

Proof: By Lemmas 7.6 and 7.8, we may assume $P_{\_}1\oplus P_{\_}2\neq\ominus P_{\_}0$, and $P_{\_}2=P_{\_}0\oplus P_{\_}1$. By Lemma 7.6, we need only eliminate the cases $P_{\_}0\oplus P_{\_}1=\ominus P_{\_}1$ and $P_{\_}1\oplus(P_{\_}0\oplus P_{\_}1)=P_{\_}0$.

If $P_{\_}2=P_{\_}0\oplus P_{\_}1=\ominus P_{\_}1$, then $RHS=P_{\_}0$ and by Lemmas 7.3 and 7.7,

[TABLE]

Finally, if $P_{\_}1\oplus(P_{\_}0\oplus P_{\_}1)=P_{\_}0$, then Lemma 7.9 implies $P_{\_}0=P_{\_}0\oplus(P_{\_}1\oplus P_{\_}1)$, Lemma 2.1 then implies $P_{\_}1=O$, and the claim follows from Lemma 7.10. $\Box$