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: (M(e) mod n)d 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-1)*(q-1). Among the lemmas proved mechanically and used in the main proof are many familiar theorems of number theory, including Fermat's theorem: M (p-1) mod p = 1, when p is a prime and p/M. The axioms underlying the proofs are those of Peano arithmetic and ordered pairs. (Author)