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