Cryptography

RSA: prove a tiny round trip

Use a finite type to prove a complete round trip for every message in a miniature RSA system.

-- RSA: prove a tiny round trip
-- History: 1978 · Rivest, Shamir, Adleman publication.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: With p=3 and q=11, φ(33)=20 and 3×7 is 1 modulo 20.
-- Scope: Proves decrypt(encrypt(m))=m for all 33 residues with e=3,d=7. This is tiny textbook RSA without padding and is not secure encryption.
-- Source: https://web.mit.edu/6.857/OldStuff/Fall03/ref/rivest78method.pdf

abbrev Message := Fin 33

def encrypt (m : Message) : Message := m^3
def decrypt (c : Message) : Message := c^7

-- This checks every possible message, not just the printed one.
theorem rsa_round_trip : ∀ m : Message, decrypt (encrypt m) = m := by
  decide

def main : IO Unit := do
  let message : Message := 4
  IO.println s!"Message: {message}"
  IO.println s!"Encrypted: {encrypt message}"
  IO.println s!"Decrypted: {decrypt (encrypt message)}"

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`decide`

Builds a proof using a decision procedure. Quantifying over Fin n checks every one of its finitely many values.

`Fin n`

Fin n contains the natural numbers less than n, each with a bound proof. Addition and multiplication wrap modulo n.

Background and proof scope

1978 · Rivest, Shamir, Adleman publication

With p=3 and q=11, φ(33)=20 and 3×7 is 1 modulo 20.

Proves decrypt(encrypt(m))=m for all 33 residues with e=3,d=7. This is tiny textbook RSA without padding and is not secure encryption.

The RSA paper (1978)

Expected output

Reference only. Run the file to check its actual result.

Message: 4
Encrypted: 31
Decrypted: 4

Exercise

Replace the decryption exponent 7 with 5. Can Lean still prove the round trip for all messages?