Operations of Points on Elliptic Curve in Projective Coordinates

Yuichi Futa; Hiroyuki Okazaki; Daichi Mizushima; Yasunari Shidama

doi:10.2478/v10037-012-0012-2

.blurhash-client-img { display: none !important; }

Operations of Points on Elliptic Curve in Projective Coordinates

Formalized Mathematics

Volume 20 (2012): Issue 1 (January 2012)

By: Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima and Yasunari Shidama

Open Access

|Sep 2012

Abstract

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: compell_ProjCo and addell_ProjCo are unary and binary operations of a point over the elliptic curve.

References

Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.
Search in Google Scholar
Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175-180, 1990.
Search in Google Scholar
Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990.
Search in Google Scholar
Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
Search in Google Scholar
Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
Search in Google Scholar
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.10.2478/v10037-011-0021-6
Search in Google Scholar
G. Seroussi I. Blake and N. Smart. Elliptic Curves in Cryptography. Number 265 in London Mathematical Society Lecture Note Series. Cambridge University Press, 1999.
Search in Google Scholar
Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990.
Search in Google Scholar
Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887-890, 1990.
Search in Google Scholar
Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relative primes. Formalized Mathematics, 1(5):829-832, 1990.
Search in Google Scholar
Christoph Schwarzweller. The binomial theorem for algebraic structures. Formalized Mathematics, 9(3):559-564, 2001.
Search in Google Scholar
Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115-122, 1990.
Search in Google Scholar
Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97-105, 1990.
Search in Google Scholar
Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.
Search in Google Scholar
Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821-827, 1990.
Search in Google Scholar
Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.
Search in Google Scholar
Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
Search in Google Scholar

Articles in this issue

DOI: https://doi.org/10.2478/v10037-012-0012-2 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630

Journal RSS Feed

Language: English

Page range: 87 - 95

Published on: Sep 12, 2012

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 issue per year

Related subjects:

Mathematics,

Logic and set theory,

Computer sciences,

Artificial intelligence

© 2012 Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima, Yasunari Shidama, published by University of Białystok
This work is licensed under the Creative Commons License.

Volume 20 (2012): Issue 1 (January 2012)