This article gives an elementary computational proof of the group law for Edwards elliptic curves. The associative law is expressed as a polynomial identity over the integers that is directly checked by polynomial division. Unlike other proofs, no preliminaries such as intersection numbers, Bézout’s theorem, projective geometry, divisors, or Riemann Roch are required. The proof of the group law has been formalized in the Isabelle/HOL proof assistant.
CITATION STYLE
Hales, T., & Raya, R. (2020). Formal Proof of the Group Law for Edwards Elliptic Curves. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12167 LNAI, pp. 254–269). Springer. https://doi.org/10.1007/978-3-030-51054-1_15
Mendeley helps you to discover research relevant for your work.