### 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

- Computer science/Security/Cryptography

### Session Elliptic_Curves_Group_Law

- Elliptic_Axclass
- Elliptic_Locale
- Elliptic_Test

### Used by

- Cryptographic Standards

## Cite

×

Elliptic_Curves_Group_Law-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Mar 1, 2017 : Isabelle2016-1