<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this article, we formalize in Mizar [1], [2] a binary operation of points on an elliptic curve over <bold>GF</bold>(<bold>p</bold>) in affine coordinates. We show that the operation is unital, complementable and commutative. Elliptic curve cryptography [3], whose security is based on a difficulty of discrete logarithm problem of elliptic curves, is important for information security.</p></abstract>

In this article, we formalize in Mizar [1], [2] a binary operation of points on an elliptic curve over GF(p) in affine coordinates. We show that the operation is unital, complementable and commutative. Elliptic curve cryptography [3], whose security is based on a difficulty of discrete logarithm problem of elliptic curves, is important for information security.

Operations of Points on Elliptic Curve in Affine Coordinates

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 License.

{"article-title":"Operations of Points on Elliptic Curve in Affine Coordinates"}

In this article, we formalize in Mizar [1], [2] a binary operation of points on an elliptic curve over GF(p) in affine coordinates. We show that the operation...

Operations of Points on Elliptic Curve in Affine Coordinates

Data publikacji: 17 lut 2020

Zakres stron: 315 - 320

Przyjęty: 29 sie 2019

DOI: https://doi.org/10.2478/forma-2019-0026

Słowa kluczowe
elliptic curve, commutative operation

© 2019 Yuichi Futa et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 License.

Operations of Points on Elliptic Curve in Affine Coordinates

Data publikacji: 17 lut 2020

Zakres stron: 315 - 320

Przyjęty: 29 sie 2019

DOI: https://doi.org/10.2478/forma-2019-0026

Słowa kluczoweelliptic curve, commutative operation

© 2019 Yuichi Futa et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 License.

Słowa kluczowe
elliptic curve, commutative operation