Pratt's Primality Certificates

Simon Wimmer 📧 and Lars Noschinski 🌐

July 22, 2013

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

In 1975, Pratt introduced a proof system for certifying primes. He showed that a number p is prime iff a primality certificate for p exists. By showing a logarithmic upper bound on the length of the certificates in size of the prime number, he concluded that the decision problem for prime numbers is in NP. This work formalizes soundness and completeness of Pratt's proof system as well as an upper bound for the size of the certificate.

License

BSD License

History

November 19, 2024
Added a command for reading and verifying certificates in bulk. Introduced more compact syntax. Verified primes from FIPS 186-4 and PKCS #1 v2.2.

Topics

Session Pratt_Certificate

Depends on

Used by

Cite

× 
@article{Pratt_Certificate-AFP,
  author  = {Simon Wimmer and Lars Noschinski},
  title   = {Pratt's Primality Certificates},
  journal = {Archive of Formal Proofs},
  month   = {July},
  year    = {2013},
  note    = {\url{https://isa-afp.org/entries/Pratt_Certificate.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: