Formal Proof of the Group Law for Edwards Elliptic Curves

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...

Descripción completa

Detalles Bibliográficos
Autores principales: Hales, Thomas, Raya, Rodrigo
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324045/
http://dx.doi.org/10.1007/978-3-030-51054-1_15
_version_ 1783551869816143872
author Hales, Thomas
Raya, Rodrigo
author_facet Hales, Thomas
Raya, Rodrigo
author_sort Hales, Thomas
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7324045
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73240452020-06-30 Formal Proof of the Group Law for Edwards Elliptic Curves Hales, Thomas Raya, Rodrigo Automated Reasoning Article 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. 2020-06-06 /pmc/articles/PMC7324045/ http://dx.doi.org/10.1007/978-3-030-51054-1_15 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Hales, Thomas
Raya, Rodrigo
Formal Proof of the Group Law for Edwards Elliptic Curves
title Formal Proof of the Group Law for Edwards Elliptic Curves
title_full Formal Proof of the Group Law for Edwards Elliptic Curves
title_fullStr Formal Proof of the Group Law for Edwards Elliptic Curves
title_full_unstemmed Formal Proof of the Group Law for Edwards Elliptic Curves
title_short Formal Proof of the Group Law for Edwards Elliptic Curves
title_sort formal proof of the group law for edwards elliptic curves
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324045/
http://dx.doi.org/10.1007/978-3-030-51054-1_15
work_keys_str_mv AT halesthomas formalproofofthegrouplawforedwardsellipticcurves
AT rayarodrigo formalproofofthegrouplawforedwardsellipticcurves

Ejemplares similares