Proving order of Curve25519
andres-erbsen opened this issue · 1 comments
If we want to prove that Curve25519 has order 8*l and the base point has order l, I think we can actually do this.
|{ x^3 + 486662*x^2 + x | x \in F_p }| <= p
forall x, |{ y | y^2 = x }| <= 2
n = |{(x,y) | y^2 = x^3 + 486662*x^2 + x :> F_p}| = the order of the elliptive curve; n <= 2*p
B = (9, ?) and l from https://github.com/mit-plv/fiat-crypto/blob/master/src/Spec/Curve25519.v#L6
check that l * B = 0. this is a heavy computation, we probably want to use the montgomery ladder and a non-silly field inversion
use group theorems from coqprime or https://www.math.miami.edu/~cscaduto/teaching/461-spring-2021/Lecture%20notes/461-Lecture-10.pdf
m = order of B defined as smallest m s.t m*B=0; m <= n
0 = l * B = l%m*B, so l%m = 0
m divides l, and l is prime, so l=m
explicitly input a point of order 8 and naively check it has order 8
8 divides n, l divides n, 8*l <= n <= 2*p < 2*8*l -> n = 8*l
@talkon I mentioned using the order of Curve25519 today; this is the tracking issue for this. I just now added a computation to check that Curve25519 basepoint times its order gives 0 at https://github.com/mit-plv/fiat-crypto/pull/1514/files . I expect that to actually make use of this you'll need to deduplicate the definitions of ladderstep and montladder, currently there are slightly different copies under Spec and Curves. Further, the current computation includes an extraneous conversion out of projective montgomery x/z coordinates to normal montgomery x coordinate, which means it would also return 0 for the point with x coordinate equal to 0 instead of the identity point.