The Group Law for Elliptic Curves

Stefan Berghofer 🌐

February 28, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

We prove the group law for elliptic curves in Weierstrass form over fields of characteristic greater than 2. In addition to affine coordinates, we also formalize projective coordinates, which allow for more efficient computations. By specializing the abstract formalization to prime fields, we can apply the curve operations to parameters used in standard security protocols.

License

BSD License

Topics

Session Elliptic_Curves_Group_Law

Used by

Cite

× 
@article{Elliptic_Curves_Group_Law-AFP,
  author  = {Stefan Berghofer},
  title   = {The Group Law for Elliptic Curves},
  journal = {Archive of Formal Proofs},
  month   = {February},
  year    = {2017},
  note    = {\url{https://isa-afp.org/entries/Elliptic_Curves_Group_Law.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: