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

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 1982
Accession Number
ADA132482

Entities

People

  • J. Strother Moore
  • Robert S. Boyer

Organizations

  • University of Texas at Austin

Tags

Communities of Interest

  • Advanced Electronics

DTIC Thesaurus Topics

  • Algorithms
  • Arithmetic
  • Asymetric Encryption
  • Automatic
  • Computer Programs
  • Computer Science
  • Computers
  • Cryptography
  • Governments
  • Materials
  • Mathematics
  • Notation
  • Number Theory
  • Numbers
  • Permutations
  • Recursive Functions
  • Systems Science

Fields of Study

  • Mathematics

Readers

  • Computational Linguistics
  • Cybersecurity.
  • Educational Psychology