The Group Law for Edwards Curves

TL;DR

This paper provides an elementary, computational proof of the group law for Edwards elliptic curves, simplifying verification and facilitating formal proof of cryptographic protocols.

Contribution

It introduces a polynomial identity-based proof of the group law that avoids complex geometric concepts, aiding formal verification efforts.

Findings

Polynomial identity for group law verified by division

Proof avoids advanced geometric tools

Facilitates formal verification of cryptographic algorithms

Abstract

This article gives an elementary computational proof of the group law for Edwards elliptic curves following Bernstein, Lange, et al., Edwards, and Friedl. The associative law is expressed as a polynomial identity over the integers that is directly checked by polynomial division. No preliminaries such as intersection numbers, B\'ezout's theorem, projective geometry, divisors, or Riemann Roch are required. The proofs have been designed to facilitate the formal verification of elliptic curve cryptography.