<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

Published Online: Feb 17, 2020

Page range: 315 - 320

Accepted: Aug 29, 2019

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

Keywords
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

Published Online: Feb 17, 2020

Page range: 315 - 320

Accepted: Aug 29, 2019

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

Keywordselliptic 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.

Keywords
elliptic curve, commutative operation