<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

Pubblicato online: 17 feb 2020

Pagine: 315 - 320

Accettato: 29 ago 2019

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

Parole chiave
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

Pubblicato online: 17 feb 2020

Pagine: 315 - 320

Accettato: 29 ago 2019

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

Parole chiaveelliptic 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.

Parole chiave
elliptic curve, commutative operation