8494 articles  [english version]

inria-00138382, version 2

Primality Proving with Elliptic Curves

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

TPHOL 2007 4732 (2007) 319-333

Résumé : 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)
  • Domaine : Informatique/Cryptographie et sécurité
    Informatique/Logique en informatique
  • Référence interne : RR-6155
  • Versions disponibles :  v1 (26-03-2007) v2 (09-04-2007)
 
  • inria-00138382, version 2
  • http://hal.inria.fr/inria-00138382
  • oai:hal.inria.fr:inria-00138382
  • Contributeur : Guillaume Hanrot <>
  • Soumis le : Lundi 9 Avril 2007, 07:50:19
  • Dernière modification le : Mercredi 10 Octobre 2007, 17:30:03