Accession Number : ADA130626

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

Descriptive Note : Technical rept.,

Corporate Author : TEXAS UNIV AT AUSTIN INST FOR COMPUTING SCIENCE AND COMPUTER APPLICATIONS

Personal Author(s) : Boyer,Robert S ; Moore,J Strother

PDF Url : ADA130626

Report Date : Sep 1982

Pagination or Media Count : 26

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)

Descriptors :   *Algorithms, *Mathematics, Theorems, Solutions(General)

Subject Categories : Theoretical Mathematics

Distribution Statement : APPROVED FOR PUBLIC RELEASE