A polytime proof of correctness of the Rabin-Miller algorithm from Fermat's little theorem

Although a deterministic polytime algorithm for primality testing is now known ([4]), the Rabin-Miller randomized test of primality continues being the most efficient and widely used algorithm. We prove the correctness of the Rabin-Miller algorithm in the theory V1 for polynomial time reasoning, from Fermat's little theorem. This is interesting because the Rabin-Miller algorithm is a polytime randomized algorithm, which runs in the class RP (i.e., the class of polytime MonteCarlo algorithms), with a sampling space exponential in the length of the binary encoding of the input number. (The class RP contains polytime P.) However, we show how to express the correctness in the language of V1 , and we also show that we can prove the formula expressing correctness with polytime reasoning from Fermat's Little theorem, which is generally expected to be independent of V1 . Our proof is also conceptually very basic in the sense that we use the extended Euclid's algorithm, for comp...

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Grzegorz Herman, Michael Soltys
• Keywords: Algorithm, CORR 2008, Deterministic Polytime Algorithm, Education, Rabin-Miller Algorithm