Proof Checking the RSA (Rivest, Shamir and Adleman) Public Key Encryption Algorithm.
Abstract
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)
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1982
- Accession Number
- ADA130626
Entities
People
- J. Strother Moore
- Robert S. Boyer
Organizations
- University of Texas at Austin