Proof Checking The RSA Public Key Encryption Algorithm
Robert S. Boyer, J Strother Moore · American Mathematical Monthly · 1984
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 mod n) mod N=M, provided n is the product of two distinct primes p and q, M