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.

### Like this:

Like Loading...

*Related*

Comments on:"Elliptic Curves" (2)Michael Norrishsaid:Did you see that Laurent Théry has a couple of technical reports on this topic?

Joseph Chansaid:Thanks, Michael. With your hint I can find the following from INRIA:

Laurent Théry used the prover Coq, and Romain Cosset developed a new algorithm. Is there any work on proving/verifying EC factoring algorithms?