Proof Checking the RSA (Rivest, Shamir and Adleman) Public Key Encryption Algorithm.

The authors describe the use of a mechanical theorem-prover to check the published proof of the invertibility of the public key encryption algorithm of Rivest, Shamir and Adleman Me mod nd mod n M, provided n is the product of two distinct primes p and q, M n, and e and d are multiplicative inverses in the ring of integers modulo p-1q-1. Among the lemmas proved mechanically and used in the main proof are many familiar theorems of number theory, including Fermats theorem M p-1 mod p 1, when p is a prime and pM. The axioms underlying the proofs are those of Peano arithmetic and ordered pairs. Author