In this article, we formalize operations of points on an elliptic curve over GF(p). Elliptic curve cryptography [7], whose security is based on a difficulty of discrete logarithm problem of elliptic curves, is important for information security. We prove that the two operations of points: compellProjCo and addellProjCo are unary and binary operations of a point over the elliptic curve.
@article{bwmeta1.element.doi-10_2478_v10037-012-0012-2,
author = {Yuichi Futa and Hiroyuki Okazaki and Daichi Mizushima and Yasunari Shidama},
title = {Operations of Points on Elliptic Curve in Projective Coordinates},
journal = {Formalized Mathematics},
volume = {20},
year = {2012},
pages = {87-95},
zbl = {1276.11200},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_v10037-012-0012-2}
}
Yuichi Futa; Hiroyuki Okazaki; Daichi Mizushima; Yasunari Shidama. Operations of Points on Elliptic Curve in Projective Coordinates. Formalized Mathematics, Tome 20 (2012) pp. 87-95. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_v10037-012-0012-2/
Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.
Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175-180, 1990.
Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990.
Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Set of points on elliptic curve in projective coordinates. Formalized Mathematics, 19(3):131-138, 2011, doi: 10.2478/v10037-011-0021-6.[Crossref] | Zbl 1276.11090
G. Seroussi I. Blake and N. Smart. Elliptic Curves in Cryptography. Number 265 in London Mathematical Society Lecture Note Series. Cambridge University Press, 1999.
Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990.
Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887-890, 1990.
Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relative primes. Formalized Mathematics, 1(5):829-832, 1990.
Christoph Schwarzweller. The binomial theorem for algebraic structures. Formalized Mathematics, 9(3):559-564, 2001.
Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115-122, 1990.
Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97-105, 1990.
Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.
Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821-827, 1990.
Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.
Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.