Abstract
Elliptic curves are fascinating mathematical objects. In this paper, we present the way they have been represented inside the 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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Boutin, S.: Using Reflection to Build Efficient and Certified Decision Procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, pp. 515–529. Springer, Heidelberg (1997)
Boyer, R.S., Moore, J.S.: Single-threaded objects in ACL2. In: Ramakrishnan, I.V. (ed.) PADL 2001. LNCS, vol. 1990, pp. 9–27. Springer, Heidelberg (2001)
Buchberger, B.: Introduction to Gröbner Bases. In: Buchberger, B., Winkler, F. (eds.) Gröbner Bases and Applications, pp. 3–31. Cambridge University Press, Cambridge (1998)
Capani, A., Niesi, G., Robbiano, L.: Cocoa: Computations in commutative algebra, available at http://cocoa.dima.unige.it/
Cohen, H., Frey, G.: Handbook of Elliptic and Hyperelliptic Curve Cryptography. Discrete Mathematics and Its Applications. Chapman & Hall / CRC (2005)
Créci, J., Pottier, L.: Gb: une procédure de décision pour le système Coq. In: JFLA 2004, pp. 83–90 (2004)
Friedl, S.: An elementary proof of the group law for elliptic curves. Excerpt from undergraduate thesis, Regensburg (1998), available at http://www.labmath.uqam.ca/~friedl/papers/AAELLIPTIC.PDF
Goldwasser, S., Kilian, J.: Almost all primes can be quickly certified. In: Proceedings of the 18th STOC, pp. 316–329 (1986)
Grégoire, B., Théry, L.: A Purely Functional Library for Modular Arithmetic and its Application to Certifying Large Prime Numbers. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 423–437. Springer, Heidelberg (2006)
Grégoire, B., Théry, L., Werner, B.: A Computational Approach to Pocklington Certificates in Type Theory. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol. 3945, pp. 97–113. Springer, Heidelberg (2006)
Grégoire, B., Mahboubi, A.: Proving ring equalities done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, Heidelberg (2005)
Harrison, J.: HOL light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996)
Harrison, J.: Complex quantifier elimination in HOL. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 159–174. Springer, Heidelberg (2001)
Hurd, J.: Formalized elliptic curve cryptography, available at http://www.cl.cam.ac.uk/~jeh1004/research/talks/elliptic-talk.pdf
Lenstra Jr., H.W.: Factoring integers with elliptic curves. Ann. Math. 126, 649–673 (1987)
Leroy, X.: Objective Caml (1997), available at http://pauillac.inria.fr/ocaml/
Martin, M.: PRIMO - primality proving, available at http://www.ellipsa.net/
Morain, F.: Certificate for (((((((((23 + 3)3 + 30)3 + 6)3 + 80)3 + 12)3 + 450)3 + 894)3 + 3636)3 + 70756)3 + 97220, available at http://www.lix.polytechnique.fr/Labo/Francois.Morain
Morain, F.: La primalité en temps polynomial, d’après Adleman, Huang; Agrawal, Kayal, Saxena. Séminaire Bourbaki, 3(55) (2002)
Ménissier-Morain, V.: The CAML Numbers Reference Manual. Technical Report 141, INRIA (1992)
Silverman, J.H.: The Arithmetic of Elliptic Curves. Springer, Heidelberg (1986)
The COQ development team: The Coq Proof Assistant Reference Manual v7.2. Technical Report 255, INRIA (2002), available at http://coq.inria.fr/doc
Théry, L.: Proving the group law for elliptic curves formally. Technical Report 330, INRIA (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Théry, L., Hanrot, G. (2007). Primality Proving with Elliptic Curves. In: Schneider, K., Brandt, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2007. Lecture Notes in Computer Science, vol 4732. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74591-4_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-74591-4_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74590-7
Online ISBN: 978-3-540-74591-4
eBook Packages: Computer ScienceComputer Science (R0)