# Theory Cryptinverts

```(*  Title:      RSAPSS/Cryptinverts.thy
Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)

section "Correctness proof for RSA"

theory Cryptinverts
imports  Crypt Productdivides  "HOL-Number_Theory.Residues"
begin

text ‹
In this theory we show, that a RSA encrypted message can be decrypted
›

primrec pred:: "nat ⇒ nat"
where
"pred 0 = 0"
| "pred (Suc a) = a"

lemma pred_unfold:
"pred n = n - 1"
by (induct n) simp_all

lemma fermat:
assumes "prime p" "m mod p ≠ 0"
shows "m^(p-(1::nat)) mod p = 1"
proof -
from assms have "[m ^ (p - 1) = 1] (mod p)"
using fermat_theorem [of p m] by (simp add: mod_eq_0_iff_dvd)
then show ?thesis
using ‹prime p› prime_gt_1_nat [of p] by (simp add: cong_def)
qed

lemma cryptinverts_hilf1: "prime p ⟹ (m * m ^(k * pred p)) mod p = m mod p"
apply (cases "m mod p = 0")
apply (simp only: mult.commute [of k "pred p"]
power_mult mod_mult_right_eq [of "m" "(m^pred p)^k" "p"]
remainderexp [of "m^pred p" "p" "k", symmetric])
apply (insert fermat [of p m], auto)
apply (simp add: mult.commute [of k] power_mult pred_unfold)
by (metis One_nat_def mod_mult_right_eq mult.right_neutral power_Suc_0 power_mod)

lemma cryptinverts_hilf2: "prime p ⟹ m*(m^(k * (pred p) * (pred q))) mod p = m mod p"
apply (simp add: mult.commute [of "k * pred p" "pred q"] mult.assoc [symmetric])
apply (rule cryptinverts_hilf1 [of "p" "m" "(pred q) * k"])
apply simp
done

lemma cryptinverts_hilf3: "prime q ⟹ m*(m^(k * (pred p) * (pred q))) mod q = m mod q"
by (fact cryptinverts_hilf1)

lemma cryptinverts_hilf4:
"m ^ x mod (p * q) = m" if "prime p" "prime q" "p ≠ q"
"m < p * q" "x mod (pred p * pred q) = 1"
proof (cases x)
case 0
with that show ?thesis
by simp
next
case (Suc x)
with that(5) have "Suc x mod (pred p * pred q) = Suc 0"
by simp
then have "pred p * pred q dvd x"
using dvd_minus_mod [of "(pred p * pred q)" "Suc x"]
by simp
then obtain y where "x = pred p * pred q * y" ..
then have "m ^ Suc x mod p = m mod p" and "m ^ Suc x mod q = m mod q"
using cryptinverts_hilf2 [of p m y q, OF ‹prime p›]
cryptinverts_hilf3 [of q m y p, OF ‹prime q›]
with that Suc show ?thesis
by (auto intro: specializedtoprimes1a)
qed

lemma primmultgreater: fixes p::nat shows "⟦ prime p; prime q; p ≠ 2; q ≠ 2⟧ ⟹ 2 < p*q"
apply (insert mult_le_mono [of 2 p 2 q])
apply auto
done

lemma primmultgreater2: fixes p::nat shows "⟦prime p; prime q; p ≠ q⟧ ⟹  2 < p*q"
apply (cases "p = 2")
apply simp+
apply (cases "q = 2")
apply (erule primmultgreater)
apply auto
done

lemma cryptinverts: "⟦ prime p; prime q; p ≠ q; n = p*q; m < n;
e*d mod ((pred p)*(pred q)) = 1⟧ ⟹ rsa_crypt (rsa_crypt m e n) d n = m"
apply (insert cryptinverts_hilf4 [of p q m "e*d"])
apply (insert cryptcorrect [of "p*q" "rsa_crypt m e (p * q)" d])
apply (insert cryptcorrect [of "p*q" m e])
apply (insert primmultgreater2 [of p q])