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:
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.
My proposed research topics are of the theme: formalize a theory X, apply to verification of algorithm Y. I still haven’t picked a topic to go ahead. Here are some of my thoughts:
- Turtle Geometry – Differential geometry and topology are the theories behind advanced turtle geometry. This is a wide range of topics – perhaps too many. The algorithms are just graphic procedures, although their validity are based on theorems. Such graphic algorithms probably have no practical applications, so are they worth verifying?
- Fractal Art – Like turtles, graphic algorithms to display fractals probably don’t have research value. Generating fractals is based on the theory of IFS. There is one practical application of IFS: (natural) image compression. I’m not sure if compression algorithms are worth verifying.
- Elliptic Curves – The theory of elliptic curves (EC) overlaps with number theory, group theory and modular forms. There are many elliptic curve algorithms in actual use, including factoring and cryptography. Certainly there are incentives to verify these algorithms, and Joe Hurd had been working on EC cryptography. Will doing only EC factoring be enough for research work?
I was thinking, formalizing EC is just putting textbook math into the theorem prover. That sounds easy. Joe’s paper showed that this is no easy task at all, and it’s only the beginning.
Among algebraic curves, elliptic curves enjoy a special status. This is because given two points A, B on the curve, there is a way to get a third point C, also on the curve. Math people denote this relationship as: A*B = C, meaning C is the product of (i.e. somehow produced by) A and B. It turns out that this “product” operation * behaves very much like the product of multiplication. In fact, math experts can show that all points on the elliptic curve under the “product” operation forms a group.
This particular feature of elliptic curve is well-known, and such curves had been well-studied by mathematicians. They found more interesting properties of elliptic curves, even a correspondence with other math objects called modular forms. This line of investigation reached a climax when the famous Fermat’s Last Theorem is linked to a special elliptic curve. This proves to be the key in the final settlement of Fermat’s claim by Andrew Wiles in 1994.
A search on the Net will show that nowadays there are many applications of elliptic curves: in integer factorization, proving primes, digit signatures and cryptography. There is a substantial body of algorithms based on the theory of elliptic curves.
Again searching on the Net, it seems that not much work has been done in verifying such elliptic curve algorithms (eventually I find this). Maybe the task isn’t straight-forward: proving an algorithm using a theorem-prover is like teaching someone who is faultless in logic deductions but with no other math background. Hence every concept of the math, e.g. elliptic curve theory, will need to be coded in the system. However, given their use in high-security areas such as cryptography, I think it is a worthwhile research project to verify elliptic curve algorithms.