Lumenary.Cryptography

Formal library

• powModdefDefinitionpropext, Quot.sound

  /-- **Modular exponentiation by repeated squaring.** To compute `bᵉ mod n`, compute
  `h = b^⌊e/2⌋ mod n` recursively, square it, and multiply by `b` once more if `e` is odd. Each
  call halves `e`, so about `log₂ e` calls suffice, and every intermediate number is below `n²`
  (or `n² · b`) — never the astronomically large `bᵉ`. -/
  def powMod (b e n : ℕ) : ℕ :=
    if e = 0 then 1 % n
    else
      let h := powMod b (e / 2) n
      if e % 2 = 0 then h * h % n else h * h % n * b % n
  termination_by e
  decreasing_by omega

  Axioms used: propext, Quot.soundformal/Lumenary/Cryptography.leanTry it in the Lean web editor

• powMod_eqtheoremProved here from basic factspropext, Quot.sound

  /-- **Repeated squaring computes the right number:** `powMod b e n = bᵉ mod n`. Strong induction
  on `e`, using `e = 2⌊e/2⌋` or `e = 2⌊e/2⌋ + 1` and the fact that reducing mod `n` before
  multiplying does not change the result mod `n` (`Nat.mul_mod`). -/
  theorem powMod_eq (b e n : ℕ) : powMod b e n = b ^ e % n := by
    induction e using Nat.strong_induction_on with
    | _ e ih =>
      rw [powMod]
      split_ifs with h0 h2
      · simp [h0]
      · have he : e = e / 2 + e / 2 := by omega
        have ih' := ih (e / 2) (by omega)
        simp only [ih']
        conv_rhs => rw [he, pow_add, Nat.mul_mod]
      · have he : e = (e / 2 + e / 2) + 1 := by omega
        have ih' := ih (e / 2) (by omega)
        simp only [ih']
        conv_rhs => rw [he, pow_succ, pow_add, Nat.mul_mod, Nat.mul_mod (b ^ (e / 2))]
        simp [Nat.mul_mod]

  Axioms used: propext, Quot.soundformal/Lumenary/Cryptography.leanTry it in the Lean web editor

• pow_mul_sub_one_succtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **The key lemma for RSA:** for a prime `p` and *every* natural number `m` (whether or not
  `p` divides it), `m^(k(p - 1) + 1) ≡ m (mod p)`. If `p ∣ m` both sides are `0 (mod p)`; otherwise
  Fermat gives `m^(p-1) ≡ 1`, so `m^(k(p-1)+1) = (m^(p-1))^k · m ≡ m`. -/
  theorem pow_mul_sub_one_succ (p : ℕ) [Fact p.Prime] (k m : ℕ) :
      m ^ (k * (p - 1) + 1) ≡ m [MOD p] := by
    rw [← ZMod.natCast_eq_natCast_iff]
    push_cast
    by_cases hm : (m : ZMod p) = 0
    · rw [hm, zero_pow (Nat.succ_ne_zero _)]
    · rw [pow_succ, mul_comm k, pow_mul, ZMod.pow_card_sub_one_eq_one hm, one_pow, one_mul]

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Cryptography.leanTry it in the Lean web editor

• rsa_correcttheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **RSA decryption works.** Let `p ≠ q` be primes, `n = pq`, and `ed ≡ 1 (mod (p-1)(q-1))`.
  Then `(mᵉ)ᵈ ≡ m (mod n)` for **every** natural number `m`. Write `ed = t(p-1)(q-1) + 1`; the key
  lemma gives `m^(ed) ≡ m` modulo `p` and modulo `q` separately, and because `p` and `q` are
  coprime the two congruences combine to one modulo `pq` (the Chinese remainder theorem, Mathlib's
  `Nat.modEq_and_modEq_iff_modEq_mul`). -/
  theorem rsa_correct {p q e d : ℕ} (hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q)
      (hed : e * d ≡ 1 [MOD (p - 1) * (q - 1)]) (m : ℕ) : (m ^ e) ^ d ≡ m [MOD p * q] := by
    have : Fact p.Prime := ⟨hp⟩
    have : Fact q.Prime := ⟨hq⟩
    have hp2 := hp.two_le
    have hq2 := hq.two_le
    -- `(p - 1)(q - 1) > 1`, so `ed` leaves remainder `1`.
    have hφ : 1 < (p - 1) * (q - 1) := by
      rcases Nat.lt_or_ge 2 p with h | h
      · calc 1 < 2 * 1 := by norm_num
          _ ≤ (p - 1) * (q - 1) := Nat.mul_le_mul (by omega) (by omega)
      · have hq3 : 3 ≤ q := by omega
        calc 1 < 1 * 2 := by norm_num
          _ ≤ (p - 1) * (q - 1) := Nat.mul_le_mul (by omega) (by omega)
    have hrem : e * d % ((p - 1) * (q - 1)) = 1 := by
      rw [hed, Nat.mod_eq_of_lt hφ]
    set t := e * d / ((p - 1) * (q - 1))
    have hsplit : e * d = t * (p - 1) * (q - 1) + 1 := by
      have := Nat.div_add_mod (e * d) ((p - 1) * (q - 1))
      rw [hrem] at this
      rw [← this]
      ring
    rw [← pow_mul, hsplit]
    have hmodp : m ^ (t * (p - 1) * (q - 1) + 1) ≡ m [MOD p] := by
      have h := pow_mul_sub_one_succ p (t * (q - 1)) m
      rwa [show t * (q - 1) * (p - 1) = t * (p - 1) * (q - 1) by ring] at h
    have hmodq : m ^ (t * (p - 1) * (q - 1) + 1) ≡ m [MOD q] :=
      pow_mul_sub_one_succ q (t * (p - 1)) m
    exact (Nat.modEq_and_modEq_iff_modEq_mul ((Nat.coprime_primes hp hq).mpr hpq)).mp
      ⟨hmodp, hmodq⟩

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Cryptography.leanTry it in the Lean web editor

• totient_pqtheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- For distinct primes, `φ(pq) = (p - 1)(q - 1)`: Mathlib's `Nat.totient_mul` (φ is
  multiplicative on coprime arguments) and `Nat.totient_prime`. So the condition in `rsa_correct`
  is the textbook `ed ≡ 1 (mod φ(n))`. -/
  theorem totient_pq {p q : ℕ} (hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q) :
      Nat.totient (p * q) = (p - 1) * (q - 1) := by
    rw [Nat.totient_mul ((Nat.coprime_primes hp hq).mpr hpq), Nat.totient_prime hp,
      Nat.totient_prime hq]

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Cryptography.leanTry it in the Lean web editor

• rsa_toytheoremProved here from basic factspropext

  /-- **A toy RSA key** (the small example in Rivest, Shamir and Adleman's 1978 paper):
  `n = 47 · 59 = 2773`, `φ = 46 · 58 = 2668`, `e = 17`, `d = 157`, since `17 · 157 = 2669`. The
  message `1234` encrypts to `1234¹⁷ mod 2773 = 1793`, which decrypts back to `1234`. The kernel
  checks the arithmetic (`decide +kernel`). -/
  theorem rsa_toy :
      17 * 157 % ((47 - 1) * (59 - 1)) = 1 ∧ 1234 ^ 17 % 2773 = 1793 ∧ 1793 ^ 157 % 2773 = 1234 := by
    decide +kernel

  Axioms used: propextformal/Lumenary/Cryptography.leanTry it in the Lean web editor

• rsa_malleabletheoremProved here from basic factspropext

  /-- **Textbook RSA is malleable:** the encryptions of `m₁` and `m₂` multiply to the encryption of
  `m₁ m₂`, because `m₁ᵉ m₂ᵉ = (m₁ m₂)ᵉ`. An attacker can transform a ciphertext into the
  ciphertext of a related message without knowing either — one reason real systems pad messages
  with randomness before encrypting. -/
  theorem rsa_malleable (m₁ m₂ e n : ℕ) :
      (m₁ ^ e % n) * (m₂ ^ e % n) % n = (m₁ * m₂) ^ e % n := by
    rw [← Nat.mul_mod, mul_pow]

  Axioms used: propextformal/Lumenary/Cryptography.leanTry it in the Lean web editor

• dh_agreetheoremProved here from basic factspropext

  /-- **Diffie–Hellman key agreement.** With public `g` and `p`, one party publishes `A = gᵃ mod p`,
  the other `B = gᵇ mod p`; then `Bᵃ ≡ Aᵇ (mod p)`, since both are `g^(ab) mod p`. Reducing mod `p`
  in between does not matter (`Nat.pow_mod`), and `(gᵇ)ᵃ = g^(ba) = g^(ab) = (gᵃ)ᵇ`. -/
  theorem dh_agree (g a b p : ℕ) : (g ^ b % p) ^ a % p = (g ^ a % p) ^ b % p := by
    rw [← Nat.pow_mod, ← Nat.pow_mod, ← pow_mul, ← pow_mul, mul_comm]

  Axioms used: propextformal/Lumenary/Cryptography.leanTry it in the Lean web editor

• dh_toytheoremProved here from basic factspropext

  /-- A toy exchange in the group of non-zero residues mod `101`, where `2` is a generator. Ama keeps
  `a = 37` and publishes `2³⁷ mod 101 = 55`; Bolat keeps `b = 58` and publishes `2⁵⁸ mod 101 = 47`.
  Both compute the shared secret `82`. -/
  theorem dh_toy :
      2 ^ 37 % 101 = 55 ∧ 2 ^ 58 % 101 = 47 ∧ 47 ^ 37 % 101 = 82 ∧ 55 ^ 58 % 101 = 82 := by
    decide +kernel

  Axioms used: propextformal/Lumenary/Cryptography.leanTry it in the Lean web editor

• otp_decrypttheoremApplies a library theorempropext, Quot.sound

  /-- **The one-time pad decrypts correctly:** encrypting with a key by bitwise XOR (`^^^`) and
  XOR-ing with the same key again returns the message. Core Lean's `Nat.xor_xor_cancel_right`. -/
  theorem otp_decrypt (m k : ℕ) : (m ^^^ k) ^^^ k = m := Nat.xor_xor_cancel_right m k

  Axioms used: propext, Quot.soundformal/Lumenary/Cryptography.leanTry it in the Lean web editor

• otp_unique_keytheoremProved here from basic factspropext, Quot.sound

  /-- **Why the one-time pad hides everything:** for any message `m` and any ciphertext `c` there
  is exactly one key `k` with `m ^^^ k = c`, namely `k = m ^^^ c`. So if the key is chosen
  uniformly at random, every message is equally consistent with the ciphertext — Shannon's perfect
  secrecy. -/
  theorem otp_unique_key (m k c : ℕ) : m ^^^ k = c ↔ k = m ^^^ c := by
    constructor
    · rintro rfl
      rw [← Nat.xor_assoc, Nat.xor_self, Nat.zero_xor]
    · rintro rfl
      rw [← Nat.xor_assoc, Nat.xor_self, Nat.zero_xor]

  Axioms used: propext, Quot.soundformal/Lumenary/Cryptography.leanTry it in the Lean web editor

Formal exercises

Each exercise contains a sorry for you to replace. Open it in the Lean web editor, or clone the repository and run lake build.

/-- Both Diffie–Hellman parties compute the same key.
Hint: `Nat.pow_mod` says `a ^ b % n = (a % n) ^ b % n`; then use `pow_mul` and `mul_comm`. -/
theorem dh_agree (g a b p : ℕ) : (g ^ b % p) ^ a % p = (g ^ a % p) ^ b % p := by
  sorry

/-- **Diffie–Hellman key agreement.** With public `g` and `p`, one party publishes `A = gᵃ mod p`,
the other `B = gᵇ mod p`; then `Bᵃ ≡ Aᵇ (mod p)`, since both are `g^(ab) mod p`. Reducing mod `p`
in between does not matter (`Nat.pow_mod`), and `(gᵇ)ᵃ = g^(ba) = g^(ab) = (gᵃ)ᵇ`. -/
theorem dh_agree (g a b p : ℕ) : (g ^ b % p) ^ a % p = (g ^ a % p) ^ b % p := by
  rw [← Nat.pow_mod, ← Nat.pow_mod, ← pow_mul, ← pow_mul, mul_comm]

/-- Textbook RSA is multiplicative.
Hint: `Nat.mul_mod` (read right to left) and `mul_pow`. -/
theorem rsa_malleable (m₁ m₂ e n : ℕ) :
    (m₁ ^ e % n) * (m₂ ^ e % n) % n = (m₁ * m₂) ^ e % n := by
  sorry

/-- **Textbook RSA is malleable:** the encryptions of `m₁` and `m₂` multiply to the encryption of
`m₁ m₂`, because `m₁ᵉ m₂ᵉ = (m₁ m₂)ᵉ`. An attacker can transform a ciphertext into the
ciphertext of a related message without knowing either — one reason real systems pad messages
with randomness before encrypting. -/
theorem rsa_malleable (m₁ m₂ e n : ℕ) :
    (m₁ ^ e % n) * (m₂ ^ e % n) % n = (m₁ * m₂) ^ e % n := by
  rw [← Nat.mul_mod, mul_pow]