Short-weierstrass-curves
Elliptic curves over prime fields in short Weierstrass form.
We provide executable formal specifications of operations on
elliptic curves in short Weierstrass form,
which are described by the equation
where a and b are integers in a prime field \{0,..,p-1\}
for an appropriate prime number p > 3,
satisfying the condition 4 a^3 + 27 b^2 \neq 0,
and where x and y range over the same prime field.
The arithmetic operations in the equation above,
namely addition and power (i.e. iterated multiplication),
are prime field operations (i.e. modulo p).
Besides the finite points (x,y) that satisfy the equation,
the curve also includes a point at infinity.
When p = 2 or p = 3,
the elliptic curve equation has different forms,
not the short Weierstrass form.
We may extend our formalization to cover those curves in the future.
We may also extend it to cover curves over non-prime finite fields.
The condition 4 a^3 + 27 b^2 \neq 0,
where the operations are again field operations,
means that the cubic equation on the right has no multiple roots.
See Neal Koblitz's book ``A Course in Number Theory and Cryptography''
(Second Edition) for background on elliptic curves.
Our formalization follows Standards for Efficient Cryptography 1 (SEC 1), as well as
``The Elliptic Curve Digital Signature Algorithm (ECDSA)'',
International Journal of Information Security,
August 2001, Volume 1, Issue 1, pages 33-63.
Subtopics
- Short-weierstrass
- Fixtype of elliptic curves over prime fields
in short Weierstrass form.
- Short-weierstrass-primep
- Check that the prime of a short Weierstrass curve is prime.
