The theory of elliptic curves (EC) can go very deep, but its applications (see here) need only an understanding of the group law which is unique to elliptic curves. Many algorithms of these applications work for any group, although the special structure of the elliptic curve group has implications in reliability (e.g. cryptography) or efficiency (e.g. factoring) of the algorithm.
Originally, my plan for the project work on this topic is to do the following:
- Formalize elementary group theory from its axioms
- Extend this formalization to include the group structure of elliptic curves
Then use this formalization to verify EC algorithms. However:
- Joe Hurd had done EC cryptography on HOL4
- Laurent Théry had done EC primality-proving on Coq
- Romain Cosset in INRIA worked on EC factorization
Since Romain Cosse haven’t published formal proofs of his new EC factorization algorithms, I may be able to fill in this gap by building upon the works of Joe and Laurent.