Theorem: rsa_correct (BrownCs22/Demos/Lecture21.lean)

State before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
⊢ rsa_decrypt private_key (p * q) (rsa_encrypt public_key (p * q) message) = message
Tactic:
dsimp [rsa_decrypt, rsa_encrypt]
State after:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message

State before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message
Tactic:
have h_lin_combo : ∃ k, public_key * private_key = 1 + (p - 1)*(q - 1)*k := 
  sorry
State after:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
h_lin_combo : ∃ k, public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message

State before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
h_lin_combo : ∃ k, public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message
Tactic:
eliminate h_lin_combo with k hk
State after:
case intro
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message

State before:
case intro
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message
Tactic:
calc 
  (message ^ public_key % (p * q)) ^ private_key % (p * q) 
    = (message ^ public_key) ^ private_key % (p * q)      := by rw [← Nat.pow_mod]
  _ = message ^ (public_key * private_key) % (p * q)      := by rw [pow_mul] 
  _ = message ^ (1 + (p - 1)*(q - 1)*k) % (p * q)         := by rw [hk]
  _ = message ^ (1 + totient (p*q)*k) % (p * q)           := by sorry 
  _ = (message * (message ^ totient (p * q))^k) % (p * q) := by rw [pow_add, pow_one, pow_mul]
  _ = (message % (p * q)) * ((message ^ totient (p * q))^k % (p * q)) % (p * q) 
                                                          := by rw [Nat.mul_mod]
  _ = (message % (p * q)) * 1 % (p * q)                   := by sorry 
  _ = message % (p * q)                                   := by rw [mul_one, Nat.mod_mod]
  _ = message                                             := by rw [Nat.mod_eq_of_lt h_msg]
State after:
no goals

State before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = (message ^ public_key) ^ private_key % (p * q)
Tactic:
rw [← Nat.pow_mod]
State after:
no goals

State before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key) ^ private_key % (p * q) = message ^ (public_key * private_key) % (p * q)
Tactic:
rw [pow_mul]
State after:
no goals

State before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message ^ (public_key * private_key) % (p * q) = message ^ (1 + (p - 1) * (q - 1) * k) % (p * q)
Tactic:
rw [hk]
State after:
no goals

State before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message ^ (1 + (p - 1) * (q - 1) * k) % (p * q) = message ^ (1 + totient (p * q) * k) % (p * q)
Tactic:
sorry
State after:
no goals

State before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message ^ (1 + totient (p * q) * k) % (p * q) = message * (message ^ totient (p * q)) ^ k % (p * q)
Tactic:
rw [pow_add, pow_one, pow_mul]
State after:
no goals

State before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message * (message ^ totient (p * q)) ^ k % (p * q) =
    message % (p * q) * ((message ^ totient (p * q)) ^ k % (p * q)) % (p * q)
Tactic:
rw [Nat.mul_mod]
State after:
no goals

State before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message % (p * q) * ((message ^ totient (p * q)) ^ k % (p * q)) % (p * q) = message % (p * q) * 1 % (p * q)
Tactic:
sorry
State after:
no goals

State before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message % (p * q) * 1 % (p * q) = message % (p * q)
Tactic:
rw [mul_one, Nat.mod_mod]
State after:
no goals

State before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message % (p * q) = message
Tactic:
rw [Nat.mod_eq_of_lt h_msg]
State after:
no goals