inria-00138382, version 2
Primality Proving with Elliptic Curves
Laurent Théry
a, 1Guillaume Hanrot a, 2
TPHOL 2007 4732 (2007) 319-333
Abstract: 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.
- a – INRIA
- 1: MARELLE (INRIA Sophia Antipolis)
- INRIA
- 2: CACAO (INRIA Lorraine - LORIA)
- CNRS : UMR7503 – INRIA – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- Domain : Computer Science/Cryptography and Security
Computer Science/Logic in Computer Science - Internal note : RR-6155
- Available versions : v1 (2007-03-26) v2 (2007-04-09)
- inria-00138382, version 2
- http://hal.inria.fr/inria-00138382
- oai:hal.inria.fr:inria-00138382
- From: Guillaume Hanrot
- Submitted on: Monday, 9 April 2007 07:50:19
- Updated on: Wednesday, 10 October 2007 17:30:03
Associated documents
Export