		Search-engine friendly clone of the ACL2 documentation.

Elliptic-curves

Montgomery

Elliptic curves over prime fields in Montgomery form.

Montgomery curves are introduced in (Section 10.3.1 of) Montgomery's ``Speeding the Pollard and Elliptic Curve Methods of Factorization'' and described in perhaps more detail in Bernstein and Lange's ``Montgomery curves and the Montgomery ladder'' and Bernstein, Birkner, Joye, Lange, and Peters's ``Twisted Edwards Curves''.

A Montgomery curve over a prime field of size p \neq 2 is described by the equation

B y^2 = x^3 + A x^2 + x

where B \neq 0 and A \not\in \{-2, 2\}. The curve consists of all the finite points (x,y) that satisfy the equation, plus the point at infinity.

Subtopics

Montgomery-mul: Scalar multiplication in the Montgomery group.
Montgomery-add: Group addition on a Montgomery curve.
Montgomery-point-orderp: Check if a point on a Montgomery curve has a certain order.
Montgomery-add-commutativity: Commutativity of Montgomery addition.
Montgomery-mul-distributivity-over-scalar-addition: Distributivity of scalar multiplication over scalar addition.
Montgomery-add-associativity: Assumption of associativity of Montgomery addition.
Birational-montgomery-twisted-edwards: Birational equivalence between Montgomery curves and twisted Edwards curves.
Montgomery-curve: Fixtype of elliptic curve over prime fields in Montgomery form.
Montgomery-mul-nonneg
Montgomery-not-point-with-x-minus1-when-a-minus-2-over-b-not-square: Theorem about no points with abscissa -1 on a Montgomery curve.
Point-on-montgomery-p: Check if a point is on a Montgomery curve.
Montgomery-neg: Negation of a point of the Montgomery curve group.
Montgomery-sub: Subtraction of two points of the Montgomery group.
Montgomery-add-closure: Assumption of closure of Montgomery addition.
Montgomery-only-point-with-y-0-when-aa-minus-4-non-square: Theorem about the only point with zero ordinate for certain Montgomery curves.
Montgomery-point-order-leastp
Montgomery-distinct-x-when-nonzero-mul-in-order-range: Multiplying a Montgomery point by two distinct and not opposite non-zero scalars in the range of the point order yields points with distinct abscissae.
Montgomery-add-inverse-uniqueness: Uniqueness of inverse (i.e. negation).
Montgomery-distributivity-of-neg-over-add: Distributivity of negation over addition.
Montgomery-mul-associativity: Associativity of scalar multiplication.
Montgomery-points-with-same-x-have-same-or-neg-y: Theorem about points on the curve with the same abscissa having the same or opposite ordinates.
Montgomery-zero: Neutral point of the Montgomery curve group.
Montgomery-points-with-same-x-are-same-or-neg-point: Theorem about points on the curve with the same abscissa being the same or opposite points.
Montgomery-mul-of-mod-order: Scalar multiplication modulo order.
Montgomery-neg-inverse: Property that negation is left and right inverse for addition.
Montgomery-zero-identity: Left and right identity properties of the neutral point.
Point-on-montgomery-finite-when-not-zero: A non-zero point on a Montgomery curve is finite.