Elliptic curves in Edwards form (or Edwards curve) and addition formulas

Question

In recent studies on elliptic curve cryptography, Edwards curves are remarkable examples on this field. Studies show that this kind of elliptic curves provide faster computation compared to Weierstrass form.

The following equation is called an Edward Curve $$x^2 + y^2 = 1 + d\cdot x^2\cdot y^2$$ or $$x^2 + y^2 = c^2 \cdot (1+d\cdot x^2y^2)$$

If $(x_1, y_1)$ and $(x_2, y_2)$ are points on an Edwards curve, then new point calculated by addition formula would be still on the curve as illustrated below.

$$(x_1, y_1) + (x_2, y_2) = (x_3, y_3)$$ where:

$$\begin{align} x_3 &= \frac{(x_1\cdot y_2+x_2\cdot y_1)}{(1+d\cdot x_1\cdot x_2\cdot y_1\cdot y_2)}\\ y_3 &= \frac{(y_1\cdot y_2-x_1\cdot x_2)}{(1-d\cdot x_1\cdot x_2\cdot y_1\cdot y_2)}\\ \end{align}$$

Proofs of addition formulas for conventional Weierstrass form exist. However, I cannot find any proof for Edwards curve addition formulas. Where do they come from?

Answer 1

I think this is a good question, but not one with an easy answer. Let me give it a go anyway.

First of all, let's focus on the classic Weierstrass case. The points on an elliptic curve $E$ in this shape form a group. We can do this by the standard way (in most cases): draw a line between two points $P$ and $Q$, intersect at a unique third point, and invert across the $x$-axis. The resulting point $R$ is defined to be $P+Q$. Many standard texts indeed provide proofs that the points with this operation form a group.

Now, as you may have noticed, this way of defining the group depends very much on the way we represent the elliptic curve. That is, it assumes that we write $E$ as the set of solutions to $y^2=x^3+ax+b$. Can we also define the group law without making this assumption? The answer is yes.

How to do this, is quite complicated. Think of an elliptic curve $E$ as a very abstract object, not even assuming how to represent its points. It can be shown, that there exist some group attached to $E$, which is the degree-0 group of something called the Picard group. We denote it by $\operatorname{Pic}^0(E)$. Even more, it can be shown that there is a bijection between the points of $E$ and elements of $\operatorname{Pic}^0(E)$. Because $\operatorname{Pic}^0(E)$ is a group, so are the points on $E$.

So, we know that the points on $E$ form a group. How do we compute it? Well, it depends on how we represent points on $E$. If we choose to write points as $(x,y)$, where $y^2=x^3+ax+b$, then it is the classical way. If we choose to write points on $E$ as $(u,v)$ where $u^2+v^2=1+du^2v^2$, then it is done in the way you described.

TLDR How do we prove that your $x_3$ and $y_3$ are correct? As above, we need to prove that they correspond to a point on $E$ such that it corresponds exactly to the group law defined by $\operatorname{Pic}^0(E)$. For this specific case, your best bet is the original paper or the cryptographic application paper. In particular I would look at section 3 of the latter paper.

Answer 2

This is actually a reference request, anyway: according to Edwards "A Normal Form for Elliptic Curves", this addition law was introduced by Gauss with reference to Euler.

http://www.ams.org/journals/bull/2007-44-03/S0273-0979-07-01153-6/S0273-0979-07-01153-6.pdf

Answer 3

Another very good reference is here. In these slides, there is a very good (and intuitive) explanation for the addition formula you are looking for. The proof consist from three steps.

1. Prove that the initial curve is elliptic (has genus 1)

2. Find exactly the birational map from the initial Edward's curve to the Weierstrass model. and finally,

3. Use the well known addition formula over the Weierstrass model and transfer (via the birational map) to the Edward's curve.

Answer 4

I have been working on understanding Edwards addition formula and finally, I found an answer. In the paper A normal form for elliptic curves, Harold Edwards proves the correctness of the addition formula by mathematical induction. He showed that new point $P_3(x_3, y_3)$'s exact value derived from the known points $P_1(x_1, y_1)$ and $P_2(x_2, y_2)$ must satisfy the elliptic curve equation only if addition formula is valid.

I also study on Euler's and Gauss's work but they are really confusing.

Answer 5

Hales proposed and verified a proof for the group law of elliptic curves in Edwards form. It does not use sophisticated tools. His proof was fully formalised in a proof assistant.