Theory RSAPSS
section "RSS-PSS encoding and decoding operation"
theory RSAPSS
imports EMSAPSS Cryptinverts
begin
text ‹We define the RSA-PSS signature and verification operations. Moreover we
show, that messages signed with RSA-PSS can always be verified
›
definition rsapss_sign_help1:: "nat ⇒ nat ⇒ nat ⇒ bv"
where "rsapss_sign_help1 em_nat e n =
nat_to_bv_length (rsa_crypt em_nat e n) (length (nat_to_bv n))"
definition rsapss_sign:: "bv ⇒ nat ⇒ nat ⇒ bv"
where "rsapss_sign m e n =
(if (emsapss_encode m (length (nat_to_bv n) - 1)) = []
then []
else (rsapss_sign_help1 (bv_to_nat (emsapss_encode m (length (nat_to_bv n) - 1)) ) e n))"
definition rsapss_verify:: "bv ⇒ bv ⇒ nat ⇒ nat ⇒ bool"
where "rsapss_verify m s d n =
(if (length s) ≠ length(nat_to_bv n)
then False
else let em = nat_to_bv_length (rsa_crypt (bv_to_nat s) d n) ((roundup (length(nat_to_bv n) - 1) 8) * 8) in emsapss_decode m em (length(nat_to_bv n) - 1))"
lemma length_emsapss_encode:
"emsapss_encode m x ≠ [] ⟹ length (emsapss_encode m x) = roundup x 8 * 8"
apply (atomize (full))
apply (simp add: emsapss_encode_def)
apply (simp add: emsapss_encode_help1_def)
apply (simp add: emsapss_encode_help2_def)
apply (simp add: emsapss_encode_help3_def)
apply (simp add: emsapss_encode_help4_def)
apply (simp add: emsapss_encode_help5_def)
apply (simp add: emsapss_encode_help6_def)
apply (simp add: emsapss_encode_help7_def)
apply (simp add: emsapss_encode_help8_def)
apply (simp add: maskedDB_zero_def)
apply (simp add: length_generate_DB)
apply (simp add: sha1len)
apply (simp add: bvxor)
apply (simp add: length_generate_PS)
apply (simp add: length_bv_prepend)
apply (simp add: MGF_def)
apply (simp add: MGF1_def)
apply (simp add: length_MGF2)
apply (simp add: sha1len)
apply (simp add: length_generate_DB)
apply (simp add: length_generate_PS)
apply (simp add: BC_def)
apply (insert roundup_ge_emBits [of x 8])
apply safe
apply (simp add: max.absorb1)
done
lemma bv_to_nat_emsapss_encode_le: "emsapss_encode m x ≠ [] ⟹ bv_to_nat (emsapss_encode m x) < 2^(roundup x 8 * 8)"
apply (insert length_emsapss_encode [of m x])
apply (insert bv_to_nat_upper_range [of "emsapss_encode m x"])
by (simp)
lemma length_helper1: shows "length
(bvxor
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))))@
sha1 (generate_M' (sha1 m) salt) @ BC)
= length
(bvxor
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))))) + 168"
proof -
have a: "length BC = 8" by (simp add: BC_def)
have b: "length (sha1 (generate_M' (sha1 m) salt)) = 160" by (simp add: sha1len)
have c: "⋀ a b c. length (a@b@c) = length a + length b + length c" by simp
from a and b show ?thesis using c by simp
qed
lemma MGFLen_helper: "MGF z l ~= [] ⟹ l <= 2^32*(length (sha1 z))"
proof (cases "2^32*length (sha1 z) < l")
assume x: "MGF z l ~= []"
assume a: "2 ^ 32 * length (sha1 z) < l"
then have "MGF z l = []"
proof (cases "l=0")
assume "l=0"
then show "MGF z l = []" by (simp add: MGF_def)
next
assume "l~=0"
then have "(l = 0 ∨ 2^32*length(sha1 z) < l) = True" using a by fast
then show "MGF z l = []" apply (simp only: MGF_def) by simp
qed
then show ?thesis using x by simp
next
assume "¬ 2 ^ 32 * length (sha1 z) < l"
then show ?thesis by simp
qed
lemma length_helper2: assumes p: "prime p" and q: "prime q"
and mgf: "(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))))) ~= []"
and len: "length (sha1 M) + sLen + 16 ≤ (length (nat_to_bv (p * q))) - Suc 0"
shows "length
(
(bvxor
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))))))
) = (roundup (length (nat_to_bv (p * q)) - Suc 0) 8) * 8 - 168"
proof -
have a: "length (MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))))) = (length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))))"
proof -
have "0 < (length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))))" by (simp add: generate_DB_def)
moreover have "(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))) ≤ 2^32 * length (sha1 (sha1 (generate_M' (sha1 m) salt)))" using mgf and MGFLen_helper by simp
ultimately show ?thesis using length_MGF by simp
qed
have b: "length (generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))) = ((roundup ((length (nat_to_bv (p * q))) - Suc 0) 8) * 8 - 168)"
proof -
have "0 <= (length (nat_to_bv (p * q))) - Suc 0"
proof -
from p have p2: "1<p" by (simp add: prime_nat_iff)
moreover from q have "1<q" by (simp add: prime_nat_iff)
ultimately have "p<p*q" by simp
then have "1<p*q" using p2 by arith
then show ?thesis using len_nat_to_bv_pos by simp
qed
then show ?thesis using solve_length_generate_DB using len by simp
qed
have c: "length (bvxor
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))))) =
roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168" using a and b and length_bvxor by simp
then show ?thesis by simp
qed
lemma emBits_roundup_cancel: "emBits mod 8 ~= 0 ⟹ (roundup emBits 8)*8 - emBits = 8-(emBits mod 8)"
apply (auto simp add: roundup)
by (arith)
lemma emBits_roundup_cancel2: "emBits mod 8 ~=0 ⟹ (roundup emBits 8) * 8 - (8-(emBits mod 8)) = emBits"
by (auto simp add: roundup)
lemma length_bound: "⟦emBits mod 8 ~=0; 8 <= (length maskedDB)⟧ ⟹ length (remzero ((maskedDB_zero maskedDB emBits)@a@b)) <= length (maskedDB@a@b) - (8-(emBits mod 8))"
proof -
assume a: "emBits mod 8 ~=0"
assume len: "8 <= (length maskedDB)"
have b:" ⋀ a. length (remzero a) <= length a"
proof -
fix a
show "length (remzero a) <= length a"
proof (induct a)
show "(length (remzero [])) <= length []" by (simp)
next
case (Cons hd tl)
show "(length (remzero (hd#tl))) <= length (hd#tl)"
proof (cases hd)
assume "hd=𝟬"
then have "remzero (hd#tl) = remzero tl" by simp
then show ?thesis using Cons by simp
next
assume "hd=𝟭"
then have "remzero (hd#tl) = hd#tl" by simp
then show ?thesis by simp
qed
qed
qed
from len show "length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) ≤ length (maskedDB @ a @ b) - (8 - emBits mod 8)"
proof -
have "remzero(bv_prepend ((roundup emBits 8) * 8 - emBits)
𝟬 (drop ((roundup emBits 8)*8 - emBits) maskedDB)@a@b) = remzero ((drop ((roundup emBits 8)*8 -emBits) maskedDB)@a@b)" using remzero_replicate by (simp add: bv_prepend)
moreover from emBits_roundup_cancel have "roundup emBits 8 * 8 - emBits = 8 - emBits mod 8" using a by simp
moreover have "length ((drop (8-emBits mod 8) maskedDB)@a@b) = length (maskedDB@a@b) - (8-emBits mod 8)"
proof -
show ?thesis using length_drop[of "(8-emBits mod 8)" maskedDB]
proof (simp)
have "0 <= emBits mod 8" by simp
then have "8-(emBits mod 8) <= 8" by simp
then show "length maskedDB + emBits mod 8 - 8 + (length a + length b) =
length maskedDB + (length a + length b) + emBits mod 8 - 8" using len by arith
qed
qed
ultimately show ?thesis using b[of "(drop ((roundup emBits 8)*8 - emBits) maskedDB)@a@b"]
by (simp add: maskedDB_zero_def)
qed
qed
lemma length_bound2: "8<=length ( (bvxor
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))))))"
proof -
have "8 <= length (generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))" by (simp add: generate_DB_def)
then show ?thesis using length_bvxor_bound by simp
qed
lemma length_helper: assumes p: "prime p" and q: "prime q" and x: "(length (nat_to_bv (p * q)) - Suc 0) mod 8 ~= 0" and mgf: "(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))))) ~= []"
and len: "length (sha1 M) + sLen + 16 ≤ (length (nat_to_bv (p * q))) - Suc 0"
shows "length
(remzero
(maskedDB_zero
(bvxor
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))))))
(length (nat_to_bv (p * q)) - Suc 0) @
sha1 (generate_M' (sha1 m) salt) @ BC))
< length (nat_to_bv (p * q))"
proof -
from mgf have round: "168 <= roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8"
proof (simp only: sha1len sLen_def)
from len have "160 + sLen +16 ≤ length (nat_to_bv (p * q)) - Suc 0" by (simp add: sha1len)
then have len1: "176 <= length (nat_to_bv (p * q)) - Suc 0" by simp
have "length (nat_to_bv (p*q)) - Suc 0 <= (roundup (length (nat_to_bv (p * q)) - Suc 0) 8) * 8"
unfolding roundup
proof (cases "(length (nat_to_bv (p*q)) - Suc 0) mod 8 = 0")
assume len2: "(length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0"
then have "(if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = (length (nat_to_bv (p * q)) - Suc 0) div 8 * 8" by simp
moreover have "(length (nat_to_bv (p * q)) - Suc 0) div 8 * 8 = (length (nat_to_bv (p * q)) - Suc 0)" using len2
by auto
ultimately show "length (nat_to_bv (p * q)) - Suc 0
≤ (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8" by simp
next
assume len2: "(length (nat_to_bv (p*q)) - Suc 0) mod 8 ~= 0"
then have "(if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = ((length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8" by simp
moreover have "length (nat_to_bv (p*q)) - Suc 0 <= ((length (nat_to_bv (p*q)) - Suc 0) div 8 + 1)*8" by auto
ultimately show "length (nat_to_bv (p * q)) - Suc 0
≤ (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8" by simp
qed
then show "168 ≤ roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8" using len1 by simp
qed
from x have a: "length
(remzero
(maskedDB_zero
(bvxor
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))))))
(length (nat_to_bv (p * q)) - Suc 0) @
sha1 (generate_M' (sha1 m) salt) @ BC)) <= length ((bvxor
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))))) @
sha1 (generate_M' (sha1 m) salt) @ BC) - (8 - (length (nat_to_bv (p*q)) - Suc 0) mod 8)" using length_bound and length_bound2 by simp
have b: " length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @
sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) +168" using length_helper1 by simp
have c: "length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) =
(roundup (length (nat_to_bv (p * q)) - Suc 0) 8) * 8 - 168" using p and q and length_helper2 and mgf and len by simp
from a and b and c have " length (remzero (maskedDB_zero
(bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))))
(length (nat_to_bv (p * q)) - Suc 0) @
sha1 (generate_M' (sha1 m) salt) @ BC)) <= roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168 +168 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)" by simp
then have "length (remzero (maskedDB_zero
(bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))))
(length (nat_to_bv (p * q)) - Suc 0) @
sha1 (generate_M' (sha1 m) salt) @ BC)) <= roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)" using round by simp
moreover have " roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8) = (length (nat_to_bv (p*q))-Suc 0)" using x and emBits_roundup_cancel2 by simp
moreover have "0<length (nat_to_bv (p*q))"
proof -
from p have s: "1<p" by (simp add: prime_nat_iff)
moreover from q have "1<q" by (simp add: prime_nat_iff)
ultimately have "p<p*q" by simp
then have "1<p*q" using s by arith
then show ?thesis using len_nat_to_bv_pos by simp
qed
ultimately show ?thesis by arith
qed
lemma length_emsapss_smaller_pq: "⟦prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) ≠ []; (length (nat_to_bv (p * q)) - Suc 0) mod 8 ~= 0⟧ ⟹ length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p*q))"
proof -
assume a: "emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) ≠ []"
assume p: "prime p" and q: "prime q"
assume x: "(length (nat_to_bv (p * q)) - Suc 0) mod 8 ~= 0"
have b: " emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)= emsapss_encode_help1 (sha1 m)
(length (nat_to_bv (p * q)) - Suc 0)"
proof (simp only: emsapss_encode_def)
from a show "(if ((2^64 ≤ length m) ∨ (2^32 * 160 < (length (nat_to_bv (p*q)) - Suc 0)))
then []
else (emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p*q))- Suc 0))) = (emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p*q)) - Suc 0))"
by (auto simp add: emsapss_encode_def)
qed
have c: "length (remzero (emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p*q))"
proof (simp only: emsapss_encode_help1_def)
from a and b have d: "(if ((length (nat_to_bv (p * q)) - Suc 0) < (length (sha1 m) + sLen + 16))
then []
else (emsapss_encode_help2 (generate_M' (sha1 m) salt)
(length (nat_to_bv (p * q)) - Suc 0))) = (emsapss_encode_help2 ((generate_M' (sha1 m)) salt) (length (nat_to_bv (p*q)) - Suc 0))"
by (auto simp add: emsapss_encode_def emsapss_encode_help1_def)
from d have len: "length (sha1 m) + sLen + 16 <= (length (nat_to_bv (p*q))) - Suc 0"
proof (cases "length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16")
assume "length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16"
then have len1: "(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then []
else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = []" by simp
assume len2: "(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then []
else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) =
emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)"
from len1 and len2 and a and b show "length (sha1 m) + sLen + 16 ≤ length (nat_to_bv (p * q)) - Suc 0"
by (auto simp add: emsapss_encode_def emsapss_encode_help1_def)
next
assume "¬ length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16"
then show "length (sha1 m) + sLen + 16 ≤ length (nat_to_bv (p * q)) - Suc 0" by simp
qed
have e: "length (remzero (emsapss_encode_help2 (generate_M' (sha1 m) salt)
(length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))"
proof (simp only: emsapss_encode_help2_def)
show "length
(remzero
(emsapss_encode_help3 (sha1 (generate_M' (sha1 m) salt))
(length (nat_to_bv (p * q)) - Suc 0)))
< length (nat_to_bv (p * q))"
proof (simp add: emsapss_encode_help3_def emsapss_encode_help4_def emsapss_encode_help5_def)
show "length
(remzero
(emsapss_encode_help6
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))))
(sha1 (generate_M' (sha1 m) salt))
(length (nat_to_bv (p * q)) - Suc 0)))
< length (nat_to_bv (p * q))"
proof (simp only: emsapss_encode_help6_def)
from a and b and d have mgf: "MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))) ~=
[]" by (auto simp add: emsapss_encode_def emsapss_encode_help1_def emsapss_encode_help2_def emsapss_encode_help3_def emsapss_encode_help4_def emsapss_encode_help5_def emsapss_encode_help6_def)
from a and b and d have f: "(if MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))) =
[]
then []
else (emsapss_encode_help7
(bvxor
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))))))
(sha1 (generate_M' (sha1 m) salt))
(length (nat_to_bv (p * q)) - Suc 0))) = (emsapss_encode_help7
(bvxor
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))))))
(sha1 (generate_M' (sha1 m) salt))
(length (nat_to_bv (p * q)) - Suc 0))"
by (auto simp add: emsapss_encode_def emsapss_encode_help1_def emsapss_encode_help2_def
emsapss_encode_help3_def emsapss_encode_help4_def emsapss_encode_help5_def
emsapss_encode_help6_def)
have "length (remzero (emsapss_encode_help7
(bvxor
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))))))
(sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))"
proof (simp add: emsapss_encode_help7_def emsapss_encode_help8_def)
from p and q and x show " length
(remzero
(maskedDB_zero
(bvxor
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))))))
(length (nat_to_bv (p * q)) - Suc 0) @
sha1 (generate_M' (sha1 m) salt) @ BC))
< length (nat_to_bv (p * q))" using "length_helper" and len and mgf by simp
qed
then show "length
(remzero
(if MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))) =
[]
then []
else emsapss_encode_help7
(bvxor
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt)))))
(MGF (sha1 (generate_M' (sha1 m) salt))
(length
(generate_DB
(generate_PS (length (nat_to_bv (p * q)) - Suc 0)
(length (sha1 (generate_M' (sha1 m) salt))))))))
(sha1 (generate_M' (sha1 m) salt))
(length (nat_to_bv (p * q)) - Suc 0)))
< length (nat_to_bv (p * q))" using f by simp
qed
qed
qed
from d and e show "length
(remzero
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16
then []
else emsapss_encode_help2 (generate_M' (sha1 m) salt)
(length (nat_to_bv (p * q)) - Suc 0)))
< length (nat_to_bv (p * q))" by simp
qed
from b and c show ?thesis by simp
qed
lemma bv_to_nat_emsapss_smaller_pq: assumes a: "prime p" and b: "prime q" and pneq: "p ~= q" and c: "emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) ≠ []" shows "bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p*q"
proof -
from a and b and c show ?thesis
proof (cases "8 dvd ((length (nat_to_bv (p * q))) - Suc 0)")
assume d: "8 dvd ((length (nat_to_bv (p * q))) - Suc 0)"
then have "2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p*q"
proof -
from d have e: "roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 = length (nat_to_bv (p * q)) - Suc 0" using rnddvd by simp
have "p*q = bv_to_nat (nat_to_bv (p*q))" by simp
then have "2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p*q"
proof -
have "0<p*q"
proof -
have "0<p" using a by (simp add: prime_nat_iff)
moreover have "0<q" using b by (simp add: prime_nat_iff)
ultimately show ?thesis by simp
qed
moreover have "2^(length (nat_to_bv (p*q)) - Suc 0) ~= p*q"
proof (cases "2^(length (nat_to_bv (p*q)) - Suc 0) = p*q")
assume "2^(length (nat_to_bv (p*q)) - Suc 0) = p*q"
then have "p=q" using a and b and prime_equal by simp
then show ?thesis using pneq by simp
next
assume "2^(length (nat_to_bv (p*q)) - Suc 0) ~= p*q"
then show ?thesis by simp
qed
ultimately show ?thesis using len_lower_bound[of "p*q"] by (simp)
qed
then show ?thesis using e by simp
qed
moreover from c have "bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0)8 * 8 )"
using bv_to_nat_emsapss_encode_le [of m "(length (nat_to_bv (p * q)) - Suc 0)"] by auto
ultimately show ?thesis by simp
next
assume y: "~(8 dvd (length (nat_to_bv (p*q)) - Suc 0))"
then show ?thesis
proof -
from y have x: "~((length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0)" by (simp add: dvd_eq_mod_eq_0)
from remzeroeq have d: "bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) = bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)))" by simp
from a and b and c and x and length_emsapss_smaller_pq[of p q m] have "bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < bv_to_nat (nat_to_bv (p*q))" using length_lower[of "remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))" "nat_to_bv (p * q)"] and prime_hd_non_zero[of p q] by (auto)
then show "bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q" using d and bv_nat_bv by simp
qed
qed
qed
lemma rsa_pss_verify: "⟦ prime p; prime q; p ≠ q; n = p*q; e*d mod ((pred p)*(pred q)) = 1; rsapss_sign m e n ≠ []; s = rsapss_sign m e n ⟧ ⟹ rsapss_verify m s d n = True"
apply (simp only: rsapss_sign_def rsapss_verify_def)
apply (simp only: rsapss_sign_help1_def)
apply (auto)
apply (simp add: length_nat_to_bv_length)
apply (simp add: bv_to_nat_nat_to_bv_length)
apply (insert length_emsapss_encode [of m "(length (nat_to_bv (p * q)) - Suc 0)"])
apply (insert bv_to_nat_emsapss_smaller_pq [of p q m])
apply (simp add: cryptinverts)
apply (insert length_emsapss_encode [of m "(length (nat_to_bv (p * q)) - Suc 0)"])
apply (insert nat_to_bv_length_bv_to_nat [of "emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)" "roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8"])
apply (simp add: verify)
done
end