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 is unital, complementable and commutative. Elliptic curve cryptography [3], whose security is based on a difficulty of discrete logarithm pro...

Full description

Bibliographic Details
Main Authors: Futa Yuichi, Okazaki Hiroyuki, Shidama Yasunari
Format: Article
Language:English
Published: Sciendo 2019-10-01
Series:Formalized Mathematics
Subjects:
Online Access:https://doi.org/10.2478/forma-2019-0026
Description
Summary: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.
ISSN:1426-2630
1898-9934