Operations of Points on Elliptic Curve in Projective Coordinates
Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima, Yasunari Shidama · Formalized Mathematics · 2012
Operations of Points on Elliptic Curve in Projective Coordinates 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.