Primality Proving with Elliptic Curves

Laurent Théry (1) , Guillaume Hanrot (2)

1 MARELLE - Mathematical, Reasoning and Software
2 CACAO - Curves, Algebra, Computer Arithmetic, and so On

Elliptic curves are fascinating mathematical objects. In this paper, we present the way they have been represented inside the {\sc Coq} system, and how we have proved that the classical composition law on the points is internal and gives them a group structure. We then describe how having elliptic curves inside a prover makes it possible to derive a checker for proving the primality of natural numbers.

Domaines: Cryptographie et sécurité [cs.CR]; Logique en informatique [cs.LO]

Laurent Théry, Guillaume Hanrot. Primality Proving with Elliptic Curves. TPHOL 2007, Sep 2007, Kaiserslautern, Germany. pp.319-333. ⟨inria-00138382v2⟩