RSA cryptosystem

17 fully proved

RSA

TheoremFermat's little theorem with exponents congruent to one#✓fully proved

Let \(p\) be a prime and let \(k \ge 1\) be a natural number with \(k \equiv 1 \pmod{p - 1}\). Then \(x^k = x\) for every \(x \in \mathbb{Z}/p\mathbb{Z}\).

theorem pow_eq_self_of_modEq {p : ℕ} [Fact p.Prime] {k : ℕ} (hk : 1 ≤ k)
    (hmod : k ≡ 1 [MOD p - 1]) (x : ZMod p) : x ^ k = x

Used by 1

Used byRSA exponent identity

TheoremFermat's little theorem for congruent exponents#✓fully proved

Let \(p\) be a prime and let \(a\) and \(b\) be natural numbers with \(a, b \ge 1\) and \(a \equiv b \pmod{p - 1}\). Then \(x^a = x^b\) for every \(x \in \mathbb{Z}/p\mathbb{Z}\).

theorem pow_eq_pow_of_modEq {p : ℕ} [Fact p.Prime] {a b : ℕ} (ha : 1 ≤ a) (hb : 1 ≤ b)
    (hab : a ≡ b [MOD p - 1]) (x : ZMod p) : x ^ a = x ^ b

Used by 1

Used byRSA-CRT decryption is correct

TheoremPositivity of the reduced RSA exponent#✓fully proved

Let \(p\), \(e\) and \(d\) be natural numbers with \(p > 2\) and \(ed \equiv 1 \pmod{p - 1}\). Then \(d \bmod (p - 1) \ge 1\).

Otherwise \(p - 1\) divides \(ed\), contradicting \(ed \equiv 1 \pmod{p - 1}\).

theorem one_le_mod {p e d : ℕ} (hp : 2 < p) (hed : e * d ≡ 1 [MOD p - 1]) :
    1 ≤ d % (p - 1)

Used by 1

Used byRSA-CRT decryption with the standard exponents

StructureRSA key#✓fully proved

A textbook RSA key consists of distinct primes \(p\) and \(q\) and natural numbers \(e\) (the public exponent) and \(d\) (the private exponent) such that \(ed \equiv 1 \pmod{p - 1}\) and \(ed \equiv 1 \pmod{q - 1}\).

structure Key where
  /-- The first prime factor of the modulus. -/
  p : ℕ
  /-- The second prime factor of the modulus. -/
  q : ℕ
  hp : p.Prime
  hq : q.Prime
  hpq : p ≠ q
  /-- The public (encryption) exponent. -/
  e : ℕ
  /-- The private (decryption) exponent. -/
  d : ℕ
  hed_p : e * d ≡ 1 [MOD p - 1]
  hed_q : e * d ≡ 1 [MOD q - 1]

Used by 13

Used byChinese remainder isomorphism for an RSA modulus · RSA-CRT decryption · RSA-CRT decryption is correct · RSA-CRT decryption with the standard exponents · RSA decryption · Correctness of textbook RSA · Correctness of textbook RSA on natural numbers · RSA encryption · RSA encryption is a bijection · RSA modulus · RSA key from the totient condition · RSA exponent identity · Checking a power identity through the Chinese remainder theorem

Key

DefinitionRSA modulus#✓fully proved

The modulus of an RSA key with primes \(p\) and \(q\) is \(n = pq\).

def n : ℕ := key.p * key.q

Uses 1 · Used by 11

Statement usesRSA key

Used byChinese remainder isomorphism for an RSA modulus · RSA-CRT decryption · RSA-CRT decryption is correct · RSA-CRT decryption with the standard exponents · RSA decryption · Correctness of textbook RSA · Correctness of textbook RSA on natural numbers · RSA encryption · RSA encryption is a bijection · RSA exponent identity · Checking a power identity through the Chinese remainder theorem

DefinitionRSA encryption#✓fully proved

For an RSA key with modulus \(n = pq\) and public exponent \(e\), encryption is the map \(\mathbb{Z}/n\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}\) given by \(m \mapsto m^e\).

def encrypt (m : ZMod key.n) : ZMod key.n := m ^ key.e

Uses 2 · Used by 3

Statement usesRSA key · RSA modulus

Used byCorrectness of textbook RSA · Correctness of textbook RSA on natural numbers · RSA encryption is a bijection

DefinitionRSA decryption#✓fully proved

For an RSA key with modulus \(n = pq\) and private exponent \(d\), decryption is the map \(\mathbb{Z}/n\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}\) given by \(c \mapsto c^d\).

def decrypt (c : ZMod key.n) : ZMod key.n := c ^ key.d

Uses 2 · Used by 5

Statement usesRSA key · RSA modulus

Used byRSA-CRT decryption is correct · RSA-CRT decryption with the standard exponents · Correctness of textbook RSA · Correctness of textbook RSA on natural numbers · RSA encryption is a bijection

DefinitionChinese remainder isomorphism for an RSA modulus#✓fully proved

For an RSA key with distinct primes \(p\), \(q\) and modulus \(n = pq\), this is the ring isomorphism \(\mathbb{Z}/n\mathbb{Z} \cong \mathbb{Z}/p\mathbb{Z} \times \mathbb{Z}/q\mathbb{Z}\) of the Chinese remainder theorem, sending \(x\) to \((x \bmod p, x \bmod q)\).

def crt : ZMod key.n ≃+* ZMod key.p × ZMod key.q := ZMod.chineseRemainder key.coprime

Uses 2 · Used by 4

Statement usesRSA key · RSA modulus

Used byRSA-CRT decryption · RSA-CRT decryption is correct · RSA exponent identity · Checking a power identity through the Chinese remainder theorem

TheoremChecking a power identity through the Chinese remainder theorem#✓fully proved

Let an RSA key have primes \(p\) and \(q\) and modulus \(n\), let \(k\) be a natural number and \(x \in \mathbb{Z}/n\mathbb{Z}\), and let \((x_p, x_q) \in \mathbb{Z}/p\mathbb{Z} \times \mathbb{Z}/q\mathbb{Z}\) be the image of \(x\) under the Chinese remainder isomorphism. If \(x_p^k = x_p\) and \(x_q^k = x_q\), then \(x^k = x\).

theorem pow_eq_self_of_crt {k : ℕ} (x : ZMod key.n)
    (h : (key.crt x).1 ^ k = (key.crt x).1 ∧ (key.crt x).2 ^ k = (key.crt x).2) :
    x ^ k = x

Uses 3 · Used by 1

Statement usesRSA key · Chinese remainder isomorphism for an RSA modulus · RSA modulus

Used byRSA exponent identity

TheoremRSA exponent identity#✓fully proved

For an RSA key with modulus \(n\) and exponents \(e\) and \(d\), every \(x \in \mathbb{Z}/n\mathbb{Z}\) satisfies \(x^{ed} = x\).

theorem pow_ed (x : ZMod key.n) : x ^ (key.e * key.d) = x

Uses 5 · Used by 2

Statement usesRSA key · RSA modulus

Proof usesChinese remainder isomorphism for an RSA modulus · Checking a power identity through the Chinese remainder theorem · Fermat's little theorem with exponents congruent to one

Used byCorrectness of textbook RSA · RSA encryption is a bijection

TheoremCorrectness of textbook RSA#✓fully proved

Decryption inverts encryption on every message, including messages that are not coprime to n.

theorem decrypt_encrypt (m : ZMod key.n) : key.decrypt (key.encrypt m) = m

Uses 5 · Used by 2

Statement usesRSA key · RSA decryption · RSA encryption · RSA modulus

Proof usesRSA exponent identity

Used byCorrectness of textbook RSA on natural numbers · RSA encryption is a bijection

TheoremRSA encryption is a bijection#✓fully proved

For an RSA key with modulus \(n = pq\) and public exponent \(e\), the encryption map \(m \mapsto m^e\) is a bijection from \(\mathbb{Z}/n\mathbb{Z}\) to itself.

theorem encrypt_bijective : Function.Bijective key.encrypt

Uses 6

Statement usesRSA key · RSA encryption · RSA modulus

Proof usesRSA decryption · Correctness of textbook RSA · RSA exponent identity

TheoremCorrectness of textbook RSA on natural numbers#✓fully proved

For an RSA key with modulus \(n = pq\) and exponents \(e\), \(d\), every natural number \(m < n\) satisfies \((m^e \bmod n)^d \bmod n = m\).

theorem decrypt_encrypt_nat {m : ℕ} (hm : m < key.n) :
    (m ^ key.e % key.n) ^ key.d % key.n = m

Uses 5

Statement usesRSA key · RSA modulus

Proof usesRSA decryption · Correctness of textbook RSA · RSA encryption

DefinitionRSA-CRT decryption#✓fully proved

Let \((p, q, e, d)\) be an RSA key with modulus \(n = pq\). For natural numbers \(d_p\), \(d_q\) and \(c \in \mathbb{Z}/n\mathbb{Z}\), let \(c_p\) and \(c_q\) be the images of \(c\) in \(\mathbb{Z}/p\mathbb{Z}\) and \(\mathbb{Z}/q\mathbb{Z}\). RSA-CRT decryption of \(c\) with the exponents \(d_p\) and \(d_q\) is the element of \(\mathbb{Z}/n\mathbb{Z}\) that corresponds to the pair \((c_p^{d_p}, c_q^{d_q})\) under the Chinese remainder isomorphism \(\mathbb{Z}/n\mathbb{Z} \cong \mathbb{Z}/p\mathbb{Z} \times \mathbb{Z}/q\mathbb{Z}\).

def crtDecrypt (dp dq : ℕ) (c : ZMod key.n) : ZMod key.n :=
  key.crt.symm ((key.crt c).1 ^ dp, (key.crt c).2 ^ dq)

Uses 3 · Used by 2

Statement usesRSA key · Chinese remainder isomorphism for an RSA modulus · RSA modulus

Used byRSA-CRT decryption is correct · RSA-CRT decryption with the standard exponents

TheoremRSA-CRT decryption is correct#✓fully proved

Let \((p, q, e, d)\) be an RSA key with modulus \(n = pq\), and let \(d_p, d_q \ge 1\) be natural numbers with \(d_p \equiv d \pmod{p - 1}\) and \(d_q \equiv d \pmod{q - 1}\). Then for every \(c \in \mathbb{Z}/n\mathbb{Z}\), RSA-CRT decryption of \(c\) with the exponents \(d_p\) and \(d_q\) equals the RSA decryption \(c^d\).

theorem crtDecrypt_eq {dp dq : ℕ} (hdp : 1 ≤ dp) (hdq : 1 ≤ dq) (hp : dp ≡ key.d [MOD key.p - 1])
    (hq : dq ≡ key.d [MOD key.q - 1]) (c : ZMod key.n) :
    key.crtDecrypt dp dq c = key.decrypt c

Uses 6 · Used by 1

Statement usesRSA key · RSA-CRT decryption · RSA decryption · RSA modulus

Proof usesChinese remainder isomorphism for an RSA modulus · Fermat's little theorem for congruent exponents

Used byRSA-CRT decryption with the standard exponents

TheoremRSA-CRT decryption with the standard exponents#✓fully proved

Let \((p, q, e, d)\) be an RSA key with modulus \(n = pq\) in which both primes are odd, that is \(p > 2\) and \(q > 2\). Then for every \(c \in \mathbb{Z}/n\mathbb{Z}\), RSA-CRT decryption of \(c\) with the exponents \(d_p = d \bmod (p - 1)\) and \(d_q = d \bmod (q - 1)\) equals the RSA decryption \(c^d\).

theorem crtDecrypt_mod_eq (hp : 2 < key.p) (hq : 2 < key.q) (c : ZMod key.n) :
    key.crtDecrypt (key.d % (key.p - 1)) (key.d % (key.q - 1)) c = key.decrypt c

Uses 6

Statement usesRSA key · RSA-CRT decryption · RSA decryption · RSA modulus

Proof usesRSA-CRT decryption is correct · Positivity of the reduced RSA exponent

DefinitionRSA key from the totient condition#✓fully proved

Given distinct primes \(p\) and \(q\) and natural numbers \(e\) and \(d\) with \(ed \equiv 1 \pmod{\varphi(pq)}\), where \(\varphi\) is Euler's totient function, this is the RSA key with primes \(p\) and \(q\), public exponent \(e\) and private exponent \(d\). Its conditions \(ed \equiv 1 \pmod{p - 1}\) and \(ed \equiv 1 \pmod{q - 1}\) hold because \(\varphi(pq) = (p - 1)(q - 1)\).

Cslib.Crypto.PublicKey.RSA.Key.ofTotient · 17 lines

def ofTotient (p q e d : ℕ) (hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q)
    (hed : e * d ≡ 1 [MOD Nat.totient (p * q)]) : Key where
  p := p
  q := q
  hp := hp
  hq := hq
  hpq := hpq
  e := e
  d := d
  hed_p := by
    rw [Nat.totient_mul ((Nat.coprime_primes hp hq).mpr hpq), Nat.totient_prime hp,
      Nat.totient_prime hq] at hed
    exact Nat.ModEq.of_mul_right _ hed
  hed_q := by
    rw [Nat.totient_mul ((Nat.coprime_primes hp hq).mpr hpq), Nat.totient_prime hp,
      Nat.totient_prime hq] at hed
    exact Nat.ModEq.of_mul_left _ hed

Uses 1

Statement usesRSA key

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.