		Search-engine friendly clone of the ACL2 documentation.

Elliptic-curves

Twisted-edwards

Elliptic curves over prime fields in twisted Edwards form.

Twisted Edwards curves are introduced in Bernstein, Birkner, Joye, Lange, and Peters's ``Twisted Edwards Curves''.

Their definition is the following:

Definition 2.1. (Twisted Edwards curve). Fix a field k with \mathrm{char}(k) \neq 2. Fix distinct nonzero elements a, d \in k. The twisted Edwards curve with coefficients a and d is the curve
$\mathrm{E}_{\mathrm{E},a,d} : a x^2 + y^2 = 1 + d x^2 y^2$
An Edwards curve is a twisted Edwards curve with a = 1.

Since, as noted above, Edwards curves are a special case of twisted Edwards curves, our formalization of twisted Edwards curves also covers Edwards curves, at least for some purposes.

Subtopics

Twisted-edwards-mul: Scalar multiplication in the twisted Edwards group.
Twisted-edwards-mul-fast: Fast scalar multiplication in the twisted Edwards group.
Twisted-edwards-add: Group addition on a twisted Edwards curve.
Twisted-edwards-point-orderp: Check if a point on a twisted Edwards curve has a certain order.
Twisted-edwards-add-associativity: Assumption of associativity of twisted-Edwards addition.
Twisted-edwards-mul-distributivity-over-scalar-addition: Distributivity of scalar multiplication over scalar addition.
Twisted-edwards-neg-inverse: Property that negation is left and right inverse for addition.
Twisted-edwards-mul-fast-nonneg
Twisted-edwards-curve: Fixtype of elliptic curves over prime fields in twisted Edwards form.
Twisted-edwards-mul-nonneg
Birational-montgomery-twisted-edwards: Birational equivalence between Montgomery curves and twisted Edwards curves.
Twisted-edwards-compress: Turn a point on a twisted Edwards curve into compressed form.
Twisted-edwards-neg: Negation of a point of the twisted Edwards curve group.
Twisted-edwards-sub: Subtraction of two points of the twisted Edwards group.
Point-on-twisted-edwards-p: Check if a point is on a twisted Edwards curve.
Twisted-edwards-curve-completep: Check if a twisted Edwards curve is complete.
Twisted-edwards-point-order-leastp
Twisted-edwards-only-points-with-x-0-or-y-1: Theorem about the only points with zero abscissa or unit ordinate on twisted Edwards curves.
Twisted-edwards-add-inverse-uniqueness: Uniqueness of inverse (i.e. negation).
Twisted-edwards-distributivity-of-neg-over-add: Distributivity of negation over addition.
Twisted-edwards-mul-associativity: Associativity of scalar multiplication.
Twisted-edwards-zero: Neutral point of the twisted Edwards curve group.
Twisted-edwards-add-closure: Proof of closure of group addition on a twisted Edwards curve.
Twisted-edwards-point-orderp-of-neg: If a point has a certain order, its negation has the same order.
Twisted-edwards-mul-of-mod-order: Scalar multiplication modulo order.
Twisted-edwards-zero-identity: Left and right identity properties of the neutral point.
Twisted-edwards-add-cancel-left: If adding the same point on the left to two points P1 and P2 yields equal points, then P1 and P2 are equal.
Twisted-edwards-mul-of-neg: Multiplying a negated point is like negating the multiplied point.
Twisted-edwards-add-commutative: Commutativity of twisted Edwards addition.