A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve

David M. Russinoff
(ARM Ltd.)

We present an elementary proof of the group properties of the elliptic curve known as "Curve25519", as a component of a comprehensive proof of correctness of a hardware implementation of the associated Diffie-Hellman key agreement algorithm. The entire proof has been formalized and mechanically verified with ACL2, and is computationally surveyable in the sense that all steps that require mechanical support are presented in such a way that they may readily reproduced in any suitable programming language.

In Anna Slobodova and Warren Hunt Jr.: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2Workshop 2017), Austin, Texas, USA, May 22-23, 2017, Electronic Proceedings in Theoretical Computer Science 249, pp. 30–46.
Published: 2nd May 2017.

ArXived at: https://dx.doi.org/10.4204/EPTCS.249.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org