Accession Number : ADA132482

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 : ADA132482

Report Date : Sep 1982

Pagination or Media Count : 26

Abstract : Typical proofs in journal articles, textbooks, and day-to-day mathematical communication use informal notation and leave many of the steps to the reader's imagination. Nevertheless, by transcribing the sentences of the proof into a formal notation, it is sometimes possible to use today's automatic theorem-provers to fill in the gaps between published steps and thus mechanically check some published, informal proofs. In this paper we illustrate this idea by mechanically checking the recently published proof of the invertibility of the public encryption algorithm. We will briefly explain the idea of public key encryption to motivate the theorem proved.

Descriptors :   *Algorithms, *Formulas(Mathematics), Recursive functions, Cryptography, Theorems

Subject Categories : Theoretical Mathematics

Distribution Statement : APPROVED FOR PUBLIC RELEASE