# Theory Cyclic_Group_Ext

theory Cyclic_Group_Ext imports
CryptHOL.CryptHOL
"HOL-Number_Theory.Cong"
begin

context cyclic_group begin

lemma generator_pow_order: "โg [^] order G = ๐ญ"
proof(cases "order G > 0")
case True
hence fin: "finite (carrier G)" by(simp add: order_gt_0_iff_finite)
then have [symmetric]: "(ฮปx. x โ โg)  carrier G = carrier G"
by(rule endo_inj_surj)(auto simp add: inj_on_multc)
then have "carrier G = (ฮป n. โg [^] Suc n)  {..<order G}"
using fin by(simp add: carrier_conv_generator image_image)
then obtain n where n: "๐ญ = โg [^] Suc n" "n < order G" by auto
have "n = order G - 1" using n inj_onD[OF inj_on_generator, of 0 "Suc n"] by fastforce
with True n show ?thesis by auto
qed simp

lemma pow_generator_mod: "โg [^] (k mod order G) = โg [^] k"
proof(cases "order G > 0")
case True
obtain n where n: "k = n * order G + k mod order G" by (metis div_mult_mod_eq)
have "โg [^] k = (โg [^] order G) [^] n โ โg [^] (k mod order G)"
by(subst n)(simp add: nat_pow_mult nat_pow_pow mult_ac)
then show ?thesis by(simp add: generator_pow_order)
qed simp

lemma int_nat_pow:
assumes "a โฅ 0"
shows "(โg [^] (int (a ::nat))) [^] (b::int)  = โg [^] (a*b)"
using assms
proof(cases "a > 0")
case True
show ?thesis
using int_pow_pow by blast
next case False
have "(โg [^] (int (a ::nat))) [^] (b::int) = ๐ญ" using False by simp
also have "โg [^] (a*b) = ๐ญ" using False by simp
ultimately show ?thesis by simp
qed

lemma pow_generator_mod_int: "โg [^] ((k :: int) mod order G) = โg [^] k"
proof(cases "order G > 0")
case True
obtain n :: int where n: "k = order G * n + k mod order G"
by (metis div_mult_mod_eq mult.commute)
then have "โg [^] k = โg [^] (order G * n) โ โg [^] (k mod order G)"
using int_pow_mult nat_pow_mult by (metis generator_closed)
then have "โg [^] k = (โg [^] order G) [^] n โ โg [^] (k mod order G)"
using int_nat_pow by (simp add: int_pow_int)
then show ?thesis by(simp add: generator_pow_order)
qed simp

lemma pow_gen_mod_mult:
shows"(โg [^] (a::nat) โ โg [^] (b::nat)) [^] ((c::int)* int (d::nat)) = (โg [^] a โ โg [^] b) [^] ((c*int d) mod (order G))"
proof-
have "(โg [^] (a::nat) โ โg [^] (b::nat)) โ carrier G" by simp
then obtain n :: nat where n: "โg [^] n = (โg [^] (a::nat) โ โg [^] (b::nat))"
by (simp add: monoid.nat_pow_mult)
also obtain r where r: "r = c*int d" by simp
have "(โg [^] (a::nat) โ โg [^] (b::nat)) [^] ((c::int)*int (d::nat)) = (โg [^] n) [^] r" using n r by simp
moreover have"... = (โg [^] n) [^] (r mod (order G))" using pow_generator_mod_int pow_generator_mod
by (metis int_nat_pow int_pow_int mod_mult_right_eq zero_le)
moreover have "... =  (โg [^] a โ โg [^] b) [^] ((c*int d) mod (order G))" using r n by simp
ultimately show ?thesis by simp
qed

lemma pow_generator_eq_iff_cong:
"finite (carrier G) โน โg [^] x = โg [^] y โท [x = y] (mod order G)"
by(subst (1 2) pow_generator_mod[symmetric])(auto simp add: cong_def order_gt_0_iff_finite intro: inj_onD[OF inj_on_generator])

lemma cyclic_group_commute:
assumes "a โ carrier G" "b โ carrier G"
shows "a โ b = b โ a"
(is "?lhs = ?rhs")
proof-
obtain n :: nat where n: "a = โg [^] n" using generatorE assms by auto
also  obtain k :: nat where k: "b = โg [^] k" using generatorE assms by auto
ultimately have "?lhs =  โg [^] n โ โg [^] k" by simp
then have "... = โg [^] (n + k)" by(simp add: nat_pow_mult)
then have "... = โg [^] (k + n)" by(simp add: add.commute)
then show ?thesis by(simp add: nat_pow_mult n k)
qed

lemma cyclic_group_assoc:
assumes "a โ carrier G" "b โ carrier G" "c โ carrier G"
shows "(a โ b) โ c = a โ (b โ c)"
(is "?lhs = ?rhs")
proof-
obtain n :: nat where n: "a = โg [^] n" using generatorE assms by auto
obtain k :: nat where k: "b = โg [^] k" using generatorE assms by auto
obtain j :: nat where j: "c = โg [^] j" using generatorE assms by auto
have "?lhs = (โg [^] n โ โg [^] k) โ โg [^] j" using n k j by simp
then have "... = โg [^] (n + (k + j))" by(simp add: nat_pow_mult add.assoc)
then show ?thesis by(simp add: nat_pow_mult n k j)
qed

lemma l_cancel_inv:
assumes "h โ carrier G"
shows "(โg [^] (a :: nat) โ inv (โg [^] a)) โ h = h"
(is "?lhs = ?rhs")
proof-
have "?lhs = (โg [^] int a โ inv (โg [^] int a)) โ h" by simp
then have "... = (โg [^] int a โ (โg [^] (- a))) โ h" using int_pow_neg[symmetric] by simp
then have "... = โg [^] (int a - a)  โ h" by(simp add: int_pow_mult)
then have "... = โg [^] ((0:: int)) โ h" by simp
then show ?thesis by (simp add: assms)
qed

lemma inverse_split:
assumes "a โ carrier G" and "b โ carrier G"
shows "inv (a โ b) = inv a โ inv b"
by (simp add:  assms comm_group.inv_mult cyclic_group_commute group_comm_groupI)

lemma inverse_pow_pow:
assumes "a โ carrier G"
shows "inv (a [^] (r::nat)) = (inv a) [^] r"
proof -
have "a [^] r โ carrier G"
using assms by blast
then show ?thesis
by (simp add: assms nat_pow_inv)
qed

lemma l_neq_1_exp_neq_0:
assumes "l โ carrier G"
and "l โ  ๐ญ"
and "l = โg [^] (t::nat)"
shows "t โ  0"
proof(rule ccontr)
assume "ยฌ (t โ  0)"
hence "t = 0" by simp
hence "โg [^] t = ๐ญ" by simp
then show "False" using assms by simp
qed

lemma order_gt_1_gen_not_1:
assumes "order G > 1"
shows "โg โ  ๐ญ"
proof(rule ccontr)
assume "ยฌ โg โ  ๐ญ"
hence "โg = ๐ญ" by simp
hence g_pow_eq_1: "โg [^] n = ๐ญ" for n :: nat by simp
hence "range (ฮปn :: nat. โg [^] n) = {๐ญ}" by auto
hence "carrier G โ {๐ญ}" using generator by auto
hence "order G < 1"
by (metis One_nat_def assms g_pow_eq_1 inj_onD inj_on_generator lessThan_iff not_gr_zero zero_less_Suc)
with assms show "False" by simp
qed

lemma power_swap: "((โg [^] (ฮฑ0::nat)) [^] (r::nat)) = ((โg [^] r) [^] ฮฑ0)"
(is "?lhs = ?rhs")
proof-
have "?lhs = โg [^] (ฮฑ0 * r)"
using nat_pow_pow mult.commute by auto
hence "... = โg [^] (r * ฮฑ0)"
by(metis mult.commute)
thus ?thesis using nat_pow_pow by auto
qed

end

end

# Theory Number_Theory_Aux

theory Number_Theory_Aux imports
"HOL-Number_Theory.Cong"
"HOL-Number_Theory.Residues"
begin

lemma bezw_inverse:
assumes "gcd (e :: nat) (N ::nat) = 1"
shows "[nat e * nat ((fst (bezw e N)) mod N) = 1] (mod nat N)"
proof-
have "(fst (bezw e N) * e + snd (bezw e N) * N) mod N = 1 mod N"
by (metis assms bezw_aux zmod_int)
hence "(fst (bezw e N) mod N * e mod N) = 1 mod N"
by (simp add: mod_mult_right_eq mult.commute)
hence cong_eq: "[(fst (bezw e N) mod N * e) = 1] (mod N)"
by (metis of_nat_1 zmod_int cong_def)
hence "[nat (fst (bezw e N) mod N) * e = 1] (mod N)"
proof -
{ assume "int (nat (fst (bezw e N) mod int N)) โ  fst (bezw e N) mod int N"
have "N = 0 โถ 0 โค fst (bezw e N) mod int N"
by fastforce
then have "int (nat (fst (bezw e N) mod int N)) = fst (bezw e N) mod int N"
by fastforce }
then have "[int (nat (fst (bezw e N) mod int N) * e) = int 1] (mod int N)"
by (metis cong_eq of_nat_1 of_nat_mult)
then show ?thesis
using cong_int_iff by blast
qed
then show ?thesis by(simp add: mult.commute)
qed

lemma inverse:
assumes "gcd x (q::nat) = 1"
and "q > 0"
shows "[x * (fst (bezw x q)) = 1] (mod q)"
proof-
have int_eq: "fst (bezw  x q) * x + snd (bezw x q) * int q = 1"
by (metis assms(1) bezw_aux of_nat_1)
hence int_eq': "(fst (bezw  x q) * x + snd (bezw x q) * int q) mod q = 1 mod q"
by (metis of_nat_1 zmod_int)
hence "(fst (bezw x q) * x) mod q = 1 mod q"
by simp
hence "[(fst (bezw x q)) * x  = 1] (mod q)"
using cong_def int_eq int_eq' by metis
then show ?thesis by(simp add: mult.commute)
qed

lemma prod_not_prime:
assumes "prime (x::nat)"
and "prime y"
and "x > 2"
and "y > 2"
shows "ยฌ prime ((x-1)*(y-1))"
by (metis assms One_nat_def Suc_diff_1 nat_neq_iff numeral_2_eq_2 prime_gt_0_nat prime_product)

lemma ex_inverse:
assumes coprime: "coprime (e :: nat) ((P-1)*(Q-1))"
and "prime P"
and "prime Q"
and "P โ  Q"
shows "โ d. [e*d = 1] (mod (P-1)) โง d โ  0"
proof-
have "coprime e (P-1)"
using assms(1) by simp
then obtain d where d: "[e*d = 1] (mod (P-1))"
using cong_solve_coprime_nat by auto
then show ?thesis by (metis cong_0_1_nat cong_1 mult_0_right zero_neq_one)
qed

lemma ex_k1_k2:
assumes coprime: "coprime (e :: nat) ((P-1)*(Q-1))"
and "[e*d = 1] (mod (P-1))"
shows "โ k1 k2. e*d + k1*(P-1) = 1 + k2*(P-1)"
by (metis assms(2) cong_iff_lin_nat)

lemma ex_k_mod:
assumes coprime: "coprime (e :: nat) ((P-1)*(Q-1))"
and "P โ  Q"
and "prime P"
and "prime Q"
and "d โ  0"
and " [e*d = 1] (mod (P-1))"
shows "โ k. e*d = 1 + k*(P-1)"
proof-
have "e > 0"
using assms(1) assms(2) prime_gt_0_nat by fastforce
then have "e*d โฅ 1" using assms by simp
then obtain k where k: "e*d = 1 + k*(P-1)"
using assms(6) cong_to_1'_nat by auto
then show ?thesis
by simp
qed

lemma fermat_little:
assumes "prime (P :: nat)"
shows "[x^P = x] (mod P)"
proof(cases "P dvd x")
case True
hence "x mod P = 0" by simp
moreover have "x ^ P mod P = 0"
by (simp add: True assms prime_dvd_power_nat_iff prime_gt_0_nat)
ultimately show ?thesis
by (simp add: cong_def)
next
case False
hence "[x ^ (P - 1) = 1] (mod P)"
using fermat_theorem assms by blast
then show ?thesis
by (metis assms cong_def diff_diff_cancel diff_is_0_eq' diff_zero mod_mult_right_eq power_eq_if power_one_right prime_ge_1_nat zero_le_one)
qed

end

# Theory Uniform_Sampling

section โนUniform Samplingโบ

textโนHere we prove different one time pad lemmas based on uniform sampling we require throughout our proofs.โบ

theory Uniform_Sampling
imports
CryptHOL.Cyclic_Group_SPMF
"HOL-Number_Theory.Cong"
CryptHOL.List_Bits
begin

text โนIf q is a prime we can sample from the units.โบ

definition sample_uniform_units :: "nat โ nat spmf"
where "sample_uniform_units q = spmf_of_set ({..< q} - {0})"

lemma set_spmf_sampl_uni_units [simp]: "set_spmf (sample_uniform_units q) = {..< q} - {0}"
by(simp add: sample_uniform_units_def)

lemma lossless_sample_uniform_units:
assumes "q > 1"
shows "lossless_spmf (sample_uniform_units q)"
apply(simp add: sample_uniform_units_def)
using assms by auto

text โนGeneral lemma for mapping using uniform sampling from units.โบ

lemma one_time_pad_units:
assumes inj_on: "inj_on f ({..<q} - {0})"
and sur: "f  ({..<q} - {0}) = ({..<q} - {0})"
shows "map_spmf f (sample_uniform_units q) = (sample_uniform_units q)"
(is "?lhs = ?rhs")
proof-
have rhs: "?rhs = spmf_of_set (({..<q} - {0}))"
by(auto simp add: sample_uniform_units_def)
also have "map_spmf(ฮปs. f s) (spmf_of_set ({..<q} - {0})) = spmf_of_set ((ฮปs. f s)  ({..<q} - {0}))"
by(simp add: inj_on)
also have "f  ({..<q} - {0}) = ({..<q} - {0})"
apply(rule endo_inj_surj) by(simp, simp add: sur, simp add: inj_on)
ultimately show ?thesis using rhs by simp
qed

text โนGeneral lemma for mapping using uniform sampling.โบ

lemma one_time_pad:
assumes inj_on: "inj_on f {..<q}"
and sur: "f  {..<q} = {..<q}"
shows "map_spmf f (sample_uniform q) = (sample_uniform q)"
(is "?lhs = ?rhs")
proof-
have rhs: "?rhs = spmf_of_set ({..< q})"
by(auto simp add: sample_uniform_def)
also have "map_spmf(ฮปs. f s) (spmf_of_set {..<q}) = spmf_of_set ((ฮปs. f s)  {..<q})"
by(simp add: inj_on)
also have "f  {..<q} = {..<q}"
apply(rule endo_inj_surj) by(simp, simp add: sur, simp add: inj_on)
ultimately show ?thesis using rhs by simp
qed

text โนThe addition map case.โบ

lemma inj_add:
assumes x:  "x < q"
and x': "x' < q"
and map: "((y :: nat) + x) mod q = (y + x') mod q"
shows "x = x'"
proof-
have aa: "((y :: nat) + x) mod q = (y + x') mod q โน x mod q = x' mod q"
proof-
have 4: "((y:: nat) + x) mod q = (y + x') mod q โน [((y:: nat) + x) = (y + x')] (mod q)"
by(simp add: cong_def)
have 5: "[((y:: nat) + x) = (y + x')] (mod q) โน [x = x'] (mod q)"
by (simp add: cong_add_lcancel_nat)
have 6: "[x = x'] (mod q) โน x mod q = x' mod q"
by(simp add: cong_def)
then show ?thesis by(simp add: map 4 5 6)
qed
also have bb: "x mod q = x' mod q โน x = x'"
by(simp add: x x')
ultimately show ?thesis by(simp add: map)
qed

lemma inj_uni_samp_add: "inj_on (ฮป(b :: nat). (y + b) mod q ) {..<q}"
by(simp add: inj_on_def)(auto simp only: inj_add)

lemma surj_uni_samp:
assumes inj: "inj_on  (ฮป(b :: nat). (y + b) mod q ) {..<q}"
shows "(ฮป(b :: nat). (y + b) mod q)  {..< q} =  {..< q}"
apply(rule endo_inj_surj) using inj by auto

lemma samp_uni_plus_one_time_pad:
shows "map_spmf (ฮปb. (y + b) mod q) (sample_uniform q) = (sample_uniform q)"
using inj_uni_samp_add surj_uni_samp one_time_pad by simp

text โนThe multiplicaton map case.โบ

lemma inj_mult:
assumes coprime: "coprime x (q::nat)"
and y: "y < q"
and y': "y' < q"
and map: "x * y mod q = x * y' mod q"
shows "y = y'"
proof-
have "x*y mod q = x*y' mod q โน y mod q = y' mod q"
proof-
have "x*y mod q = x*y' mod q โน [x*y = x*y'] (mod q)"
by(simp add: cong_def)
also have "[x*y = x*y'] (mod q) = [y = y'] (mod q)"
by(simp add: cong_mult_lcancel_nat coprime)
also have "[y = y'] (mod q) โน y mod q = y' mod q"
by(simp add: cong_def)
ultimately show ?thesis by(simp add: map)
qed
also have "y mod q = y' mod q โน y = y'"
by(simp add: y y')
ultimately show ?thesis by(simp add: map)
qed

lemma inj_on_mult:
assumes coprime: "coprime x (q::nat)"
shows "inj_on (ฮป b. x*b mod q) {..<q}"
apply(auto simp add: inj_on_def)
using coprime by(simp only: inj_mult)

lemma surj_on_mult:
assumes coprime: "coprime x (q::nat)"
and inj: "inj_on (ฮป b. x*b mod q) {..<q}"
shows "(ฮป b. x*b mod q)  {..< q} = {..< q}"
apply(rule endo_inj_surj) using coprime inj by auto

lemma mult_one_time_pad:
assumes coprime: "coprime x q"
shows "map_spmf (ฮป b. x*b mod q) (sample_uniform q) = (sample_uniform q)"
using inj_on_mult surj_on_mult one_time_pad coprime by simp

text โนThe multiplication map for sampling from units.โบ

lemma inj_on_mult_units:
assumes 1: "coprime x (q::nat)" shows "inj_on (ฮป b. x*b mod q) ({..<q} - {0})"
apply(auto simp add: inj_on_def)
using 1 by(simp only: inj_mult)

lemma surj_on_mult_units:
assumes coprime: "coprime x (q::nat)"
and inj: "inj_on (ฮป b. x*b mod q) ({..<q} - {0})"
shows "(ฮป b. x*b mod q)  ({..<q} - {0}) = ({..<q} - {0})"
proof(rule endo_inj_surj)
show "finite ({..<q} - {0})" using coprime inj by(simp)
show "(ฮปb. x * b mod q)  ({..<q} - {0}) โ {..<q} - {0}"
proof -
obtain n :: "nat set โ (nat โ nat) โ nat set โ nat" where
"โx0 x1 x2. (โv3. v3 โ x2 โง x1 v3 โ x0) = (n x0 x1 x2 โ x2 โง x1 (n x0 x1 x2) โ x0)"
by moura
then have subset: "โN f Na. n Na f N โ N โง f (n Na f N) โ Na โจ f  N โ Na"
by (meson image_subsetI)
have mem_insert: "x * n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) mod q โ {..<q} โจ x * n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) mod q โ insert 0 {..<q}"
by force
have map_eq: "(x * n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) mod q โ insert 0 {..<q} - {0}) = (x * n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) mod q โ {..<q} - {0})"
by simp
{ assume "x * n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) mod q = x * 0 mod q"
then have "(0 โค q) = (0 = q) โจ (n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) โ {..<q} โจ n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) โ {0}) โจ n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) โ {..<q} - {0} โจ x * n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) mod q โ {..<q} - {0}"
by (metis antisym_conv1 insertCI lessThan_iff local.coprime inj_mult) }
moreover
{ assume "0 โ  x * n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) mod q"
moreover
{ assume "x * n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) mod q โ insert 0 {..<q} โง x * n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) mod q โ {0}"
then have "(ฮปn. x * n mod q)  ({..<q} - {0}) โ {..<q} - {0}"
using map_eq subset by (meson Diff_iff) }
ultimately have "(ฮปn. x * n mod q)  ({..<q} - {0}) โ {..<q} - {0} โจ (0 โค q) = (0 = q)"
using mem_insert by (metis antisym_conv1 lessThan_iff mod_less_divisor singletonD) }
ultimately have "(ฮปn. x * n mod q)  ({..<q} - {0}) โ {..<q} - {0} โจ n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) โ {..<q} - {0} โจ x * n ({..<q} - {0}) (ฮปn. x * n mod q) ({..<q} - {0}) mod q โ {..<q} - {0}"
by force
then show "(ฮปn. x * n mod q)  ({..<q} - {0}) โ {..<q} - {0}"
using subset by meson
qed
show "inj_on (ฮปb. x * b mod q) ({..<q} - {0})" using assms by(simp)
qed

lemma mult_one_time_pad_units:
assumes coprime: "coprime x q"
shows "map_spmf (ฮป b. x*b mod q) (sample_uniform_units q) = sample_uniform_units q"
using inj_on_mult_units surj_on_mult_units one_time_pad_units coprime by simp

text โนAddition and multiplication map.โบ

lemma samp_uni_add_mult:
assumes coprime: "coprime x (q::nat)"
and xa: "xa < q"
and ya: "ya < q"
and map: "(y + x * xa) mod q = (y + x * ya) mod q"
shows "xa = ya"
proof-
have "(y + x * xa) mod q = (y + x * ya) mod q โน xa mod q = ya mod q"
proof-
have "(y + x * xa) mod q = (y + x * ya) mod q โน [y + x*xa = y + x *ya] (mod q)"
using cong_def by blast
also have "[y + x*xa = y + x *ya] (mod q) โน [xa = ya] (mod q)"
by(simp add: cong_add_lcancel_nat)(simp add: coprime cong_mult_lcancel_nat)
ultimately show ?thesis by(simp add: cong_def map)
qed
also have "xa mod q = ya mod q โน xa = ya"
by(simp add: xa ya)
ultimately show ?thesis by(simp add: map)
qed

lemma inj_on_add_mult:
assumes coprime: "coprime x (q::nat)"
shows "inj_on (ฮป b. (y + x*b) mod q) {..<q}"
apply(auto simp add: inj_on_def)
using coprime by(simp only: samp_uni_add_mult)

lemma surj_on_add_mult: assumes coprime: "coprime x (q::nat)" and inj: "inj_on (ฮป b. (y + x*b) mod q) {..<q}"
shows "(ฮป b. (y + x*b) mod q)  {..< q} = {..< q}"
apply(rule endo_inj_surj) using coprime inj by auto

lemma add_mult_one_time_pad: assumes coprime: "coprime x q"
shows "map_spmf (ฮป b. (y + x*b) mod q) (sample_uniform q) = (sample_uniform q)"
using inj_on_add_mult surj_on_add_mult one_time_pad coprime by simp

text โนSubtraction Map.โบ

lemma inj_minus:
assumes x: "(x :: nat) < q"
and ya: "ya < q"
and map: "(y + q - x) mod q = (y + q - ya) mod q"
shows  "x = ya"
proof-
have "(y + q - x) mod q = (y + q - ya) mod q โน x mod q = ya mod q"
proof-
have "(y + q - x) mod q = (y + q - ya) mod q โน [y + q - x = y + q - ya] (mod q)"
using cong_def by blast
moreover have "[y + q - x = y + q - ya] (mod q) โน [q - x = q - ya] (mod q)"
using x ya cong_add_lcancel_nat by fastforce
moreover have "[y + q - x = y + q - ya] (mod q) โน [q + x = q + ya] (mod q)"
by (metis add_diff_inverse_nat calculation(2) cong_add_lcancel_nat cong_add_rcancel_nat cong_sym less_imp_le_nat not_le x ya)
ultimately show ?thesis
by (simp add: cong_def map)
qed
moreover have "x mod q = ya mod q โน x = ya"
by(simp add: x ya)
ultimately show ?thesis by(simp add: map)
qed

lemma inj_on_minus: "inj_on  (ฮป(b :: nat). (y + (q - b)) mod q ) {..<q}"
by(auto simp add: inj_on_def inj_minus)

lemma surj_on_minus:
assumes inj: "inj_on  (ฮป(b :: nat). (y + (q - b)) mod q ) {..<q}"
shows "(ฮป(b :: nat). (y + (q - b)) mod q)  {..< q} = {..< q}"
apply(rule endo_inj_surj)
using inj by auto

lemma samp_uni_minus_one_time_pad:
shows "map_spmf(ฮป b. (y + (q - b)) mod q) (sample_uniform q) = (sample_uniform q)"
using inj_on_minus surj_on_minus one_time_pad by simp

lemma not_coin_flip: "map_spmf (ฮป a. ยฌ a) coin_spmf = coin_spmf"
proof-
have "inj_on Not {True, False}"
by simp
also have  "Not  {True, False} = {True, False}"
by auto
ultimately show ?thesis using one_time_pad
by (simp add: UNIV_bool)
qed

lemma xor_uni_samp: "map_spmf(ฮป b. y โ b) (coin_spmf) = map_spmf(ฮป b. b) (coin_spmf)"
(is "?lhs = ?rhs")
proof-
have rhs: "?rhs = spmf_of_set {True, False}"
by (simp add: UNIV_bool insert_commute)
also have "map_spmf(ฮป b. y โ b) (spmf_of_set {True, False}) = spmf_of_set((ฮป b. y โ b)  {True, False})"
by (simp add: xor_def)
also have "(ฮป b. xor y b)  {True, False} = {True, False}"
using xor_def by auto
finally show ?thesis using rhs by(simp)
qed

end

# Theory Semi_Honest_Def

section โนSemi-Honest Securityโบ

text โนWe follow the security definitions for the semi honest setting as described in \cite{DBLP:books/sp/17/Lindell17}.
In the semi honest model the parties are assumed not to deviate from the protocol transcript.
Semi honest security guarantees that no information is leaked during the running of the protocol.โบ

subsection โนSecurity definitionsโบ

theory Semi_Honest_Def imports
CryptHOL.CryptHOL
begin

subsubsection โนSecurity for deterministic functionalitiesโบ

locale sim_det_def =
fixes R1 :: "'msg1 โ 'msg2 โ 'view1 spmf"
and S1  :: "'msg1 โ 'out1 โ 'view1 spmf"
and R2 :: "'msg1 โ 'msg2 โ 'view2 spmf"
and S2  :: "'msg2 โ 'out2 โ 'view2 spmf"
and funct :: "'msg1 โ 'msg2 โ ('out1 ร 'out2) spmf"
and protocol :: "'msg1 โ 'msg2 โ ('out1 ร 'out2) spmf"
assumes lossless_R1: "lossless_spmf (R1 m1 m2)"
and lossless_S1: "lossless_spmf (S1 m1 out1)"
and lossless_R2: "lossless_spmf (R2 m1 m2)"
and lossless_S2: "lossless_spmf (S2 m2 out2)"
and lossless_funct: "lossless_spmf (funct m1 m2)"
begin

type_synonym 'view' adversary_det = "'view' โ bool spmf"

definition "correctness m1 m2 โก (protocol m1 m2 = funct m1 m2)"

definition adv_P1 :: "'msg1 โ 'msg2 โ 'view1 adversary_det โ real"
where "adv_P1 m1 m2 D โก ยฆ(spmf (R1 m1 m2 โค D) True)
- spmf (funct m1 m2 โค (ฮป (o1, o2). S1 m1 o1 โค D)) Trueยฆ"

definition "perfect_sec_P1 m1 m2 โก (R1 m1 m2 = funct m1 m2 โค (ฮป (s1, s2). S1 m1 s1))"

definition adv_P2 :: "'msg1 โ 'msg2 โ 'view2 adversary_det โ real"
where "adv_P2 m1 m2 D = ยฆspmf (R2 m1 m2 โค (ฮป view. D view)) True
- spmf (funct m1 m2 โค (ฮป (o1, o2). S2 m2 o2 โค (ฮป view. D view))) Trueยฆ"

definition "perfect_sec_P2 m1 m2 โก (R2 m1 m2 = funct m1 m2 โค (ฮป (s1, s2). S2 m2 s2))"

text โนWe also define the security games (for Party 1 and 2) used in EasyCrypt to define semi honest security for Party 1.
We then show the two definitions are equivalent.โบ

definition P1_game_alt :: "'msg1 โ 'msg2 โ 'view1 adversary_det โ bool spmf"
where "P1_game_alt m1 m2 D = do {
b โ coin_spmf;
(out1, out2) โ funct m1 m2;
rview :: 'view1 โ R1 m1 m2;
sview :: 'view1 โ S1 m1 out1;
b' โ D (if b then rview else sview);
return_spmf (b = b')}"

definition adv_P1_game :: "'msg1 โ 'msg2 โ 'view1 adversary_det โ real"
where "adv_P1_game m1 m2 D = ยฆ2*(spmf (P1_game_alt m1 m2 D ) True) - 1ยฆ"

text โนWe show the two definitions are equivalentโบ

lemma equiv_defs_P1:
assumes lossless_D: "โ view. lossless_spmf ((D:: 'view1 adversary_det) view)"
shows "adv_P1_game m1 m2 D = adv_P1 m1 m2 D"
including monad_normalisation
proof-
have return_True_not_False: "spmf (return_spmf (b)) True = spmf (return_spmf (ยฌ b)) False"
for b by(cases b; auto)
have lossless_ideal: "lossless_spmf ((funct m1 m2 โค (ฮป(out1, out2). S1 m1 out1 โค (ฮปsview. D sview โค (ฮปb'. return_spmf (False = b'))))))"
by(simp add: lossless_S1 lossless_funct lossless_weight_spmfD split_def lossless_D)
have return: "spmf (funct m1 m2 โค (ฮป(o1, o2). S1 m1 o1 โค D)) True
= spmf (funct m1 m2 โค (ฮป(o1, o2). S1 m1 o1 โค (ฮป view. D view โค (ฮป b. return_spmf b)))) True"
by simp
have "2*(spmf (P1_game_alt m1 m2 D ) True) - 1 = (spmf (R1 m1 m2 โค (ฮปrview. D rview โค (ฮป(b':: bool). return_spmf (True = b'))))) True
- (1 - (spmf (funct m1 m2 โค (ฮป(out1, out2). S1 m1 out1 โค (ฮปsview. D sview โค (ฮปb'. return_spmf (False = b')))))) True)"
by(simp add: spmf_bind integral_spmf_of_set adv_P1_game_def P1_game_alt_def spmf_of_set
UNIV_bool bind_spmf_const lossless_R1 lossless_S1 lossless_funct lossless_weight_spmfD)
hence "adv_P1_game m1 m2 D = ยฆ(spmf (R1 m1 m2 โค (ฮปrview. D rview โค (ฮป(b':: bool). return_spmf (True = b'))))) True
- (1 - (spmf (funct m1 m2 โค (ฮป(out1, out2). S1 m1 out1 โค (ฮปsview. D sview โค (ฮปb'. return_spmf (False = b')))))) True)ยฆ"
using adv_P1_game_def by simp
also have "ยฆ(spmf (R1 m1 m2 โค (ฮปrview. D rview โค (ฮป(b':: bool). return_spmf (True = b'))))) True
- (1 - (spmf (funct m1 m2 โค (ฮป(out1, out2). S1 m1 out1 โค (ฮปsview. D sview
โค (ฮปb'. return_spmf (False = b')))))) True)ยฆ = adv_P1 m1 m2 D"
apply(simp only: adv_P1_def spmf_False_conv_True[symmetric] lossless_ideal; simp)
by(simp only: return)(simp only: split_def spmf_bind return_True_not_False)
ultimately show ?thesis by simp
qed

definition P2_game_alt :: "'msg1 โ 'msg2 โ 'view2 adversary_det โ bool spmf"
where "P2_game_alt m1 m2 D = do {
b โ coin_spmf;
(out1, out2) โ funct m1 m2;
rview :: 'view2 โ R2 m1 m2;
sview :: 'view2 โ S2 m2 out2;
b' โ D (if b then rview else sview);
return_spmf (b = b')}"

definition adv_P2_game :: "'msg1 โ 'msg2 โ 'view2 adversary_det โ real"
where "adv_P2_game m1 m2 D = ยฆ2*(spmf (P2_game_alt m1 m2 D ) True) - 1ยฆ"

lemma equiv_defs_P2:
assumes lossless_D: "โ view. lossless_spmf ((D:: 'view2 adversary_det) view)"
shows "adv_P2_game m1 m2 D = adv_P2 m1 m2 D"
including monad_normalisation
proof-
have return_True_not_False: "spmf (return_spmf (b)) True = spmf (return_spmf (ยฌ b)) False"
for b by(cases b; auto)
have lossless_ideal: "lossless_spmf ((funct m1 m2 โค (ฮป(out1, out2). S2 m2 out2 โค (ฮปsview. D sview โค (ฮปb'. return_spmf (False = b'))))))"
by(simp add: lossless_S2 lossless_funct lossless_weight_spmfD split_def lossless_D)
have return: "spmf (funct m1 m2 โค (ฮป(o1, o2). S2 m2 o2 โค D)) True = spmf (funct m1 m2 โค (ฮป(o1, o2). S2 m2 o2 โค (ฮป view. D view โค (ฮป b. return_spmf b)))) True"
by simp
have
"2*(spmf (P2_game_alt m1 m2 D ) True) - 1 = (spmf (R2 m1 m2 โค (ฮปrview. D rview โค (ฮป(b':: bool). return_spmf (True = b'))))) True
- (1 - (spmf (funct m1 m2 โค (ฮป(out1, out2). S2 m2 out2 โค (ฮปsview. D sview โค (ฮปb'. return_spmf (False = b')))))) True)"
by(simp add: spmf_bind integral_spmf_of_set adv_P1_game_def P2_game_alt_def spmf_of_set
UNIV_bool bind_spmf_const lossless_R2 lossless_S2 lossless_funct lossless_weight_spmfD)
hence "adv_P2_game m1 m2 D = ยฆ(spmf (R2 m1 m2 โค (ฮปrview. D rview โค (ฮป(b':: bool). return_spmf (True = b'))))) True
- (1 - (spmf (funct m1 m2 โค (ฮป(out1, out2). S2 m2 out2 โค (ฮปsview. D sview โค (ฮปb'. return_spmf (False = b')))))) True)ยฆ"
using adv_P2_game_def by simp
also have "ยฆ(spmf (R2 m1 m2 โค (ฮปrview. D rview โค (ฮป(b':: bool). return_spmf (True = b'))))) True
- (1 - (spmf (funct m1 m2 โค (ฮป(out1, out2). S2 m2 out2 โค (ฮปsview. D sview โค (ฮปb'. return_spmf (False = b')))))) True)ยฆ = adv_P2 m1 m2 D"
apply(simp only: adv_P2_def spmf_False_conv_True[symmetric] lossless_ideal; simp)
by(simp only: return)(simp only: split_def spmf_bind return_True_not_False)
ultimately show ?thesis by simp
qed

end

subsubsection โน Security definitions for non deterministic functionalities โบ

locale sim_non_det_def =
fixes R1 :: "'msg1 โ 'msg2 โ ('view1 ร ('out1 ร 'out2)) spmf"
and S1  :: "'msg1 โ 'out1 โ 'view1 spmf"
and Out1 :: "'msg1 โ 'msg2 โ 'out1 โ ('out1 ร 'out2) spmf" โ โนtakes the input of the other party so can form the outputs of partiesโบ
and R2 :: "'msg1 โ 'msg2 โ ('view2 ร ('out1 ร 'out2)) spmf"
and S2  :: "'msg2 โ 'out2 โ 'view2 spmf"
and Out2 :: "'msg2 โ 'msg1 โ 'out2 โ ('out1 ร 'out2) spmf"
and funct :: "'msg1 โ 'msg2 โ ('out1 ร 'out2) spmf"
begin

type_synonym ('view', 'out1', 'out2') adversary_non_det = "('view' ร ('out1' ร 'out2')) โ bool spmf"

definition Ideal1 :: "'msg1 โ 'msg2 โ 'out1  โ ('view1 ร ('out1 ร 'out2)) spmf"
where "Ideal1 m1 m2 out1 = do {
view1 :: 'view1 โ S1 m1 out1;
out1 โ Out1 m1 m2 out1;
return_spmf (view1, out1)}"

definition Ideal2 :: "'msg2 โ 'msg1 โ 'out2 โ ('view2 ร ('out1 ร 'out2)) spmf"
where "Ideal2 m2 m1 out2 = do {
view2 :: 'view2 โ S2 m2 out2;
out2 โ Out2 m2 m1 out2;
return_spmf (view2, out2)}"

definition adv_P1 :: "'msg1 โ 'msg2 โ ('view1, 'out1, 'out2) adversary_non_det โ real"
where "adv_P1 m1 m2 D โก ยฆ(spmf (R1 m1 m2 โค (ฮป view. D view)) True) - spmf (funct m1 m2 โค (ฮป (o1, o2). Ideal1 m1 m2 o1 โค (ฮป view. D view))) Trueยฆ"

definition "perfect_sec_P1 m1 m2 โก (R1 m1 m2 = funct m1 m2 โค (ฮป (s1, s2). Ideal1 m1 m2 s1))"

definition adv_P2 :: "'msg1 โ 'msg2 โ ('view2, 'out1, 'out2) adversary_non_det โ real"
where "adv_P2 m1 m2 D = ยฆspmf (R2 m1 m2 โค (ฮป view. D view)) True - spmf (funct m1 m2 โค (ฮป (o1, o2). Ideal2 m2 m1 o2 โค (ฮป view. D view))) Trueยฆ"

definition "perfect_sec_P2 m1 m2 โก (R2 m1 m2 = funct m1 m2 โค (ฮป (s1, s2). Ideal2 m2 m1 s2))"

end

subsubsection โน Secret sharing schemes โบ

locale secret_sharing_scheme =
fixes share :: "'input_out โ ('share ร 'share) spmf"
and reconstruct :: "('share ร 'share) โ 'input_out spmf"
and F :: "('input_out โ 'input_out โ 'input_out spmf) set"
begin

definition "sharing_correct input โก (share input โค (ฮป (s1,s2). reconstruct (s1,s2)) = return_spmf input)"

definition "correct_share_eval input1 input2 โก (โ gate_eval โ F.
โ gate_protocol :: ('share ร 'share) โ ('share ร 'share) โ ('share ร 'share) spmf.
share input1 โค (ฮป (s1,s2). share input2
โค (ฮป (s3,s4). gate_protocol (s1,s3) (s2,s4)
โค (ฮป (S1,S2). reconstruct (S1,S2)))) = gate_eval input1 input2)"

end

end



# Theory OT_Functionalities

subsection โนOblivious Transfer functionalitiesโบ

textโนHere we define the functionalities for 1-out-of-2 and 1-out-of-4 OT.โบ

theory OT_Functionalities imports
CryptHOL.CryptHOL
begin

definition funct_OT_12 :: "('a ร  'a) โ bool โ (unit ร 'a) spmf"
where "funct_OT_12 inputโฉ1 ฯ = return_spmf (() , if ฯ then (snd inputโฉ1) else (fst inputโฉ1))"

lemma lossless_funct_OT_12: "lossless_spmf (funct_OT_12 msgs ฯ)"
by(simp add: funct_OT_12_def)

definition funct_OT_14 :: "('a ร 'a ร 'a ร 'a) โ (bool ร bool) โ (unit ร 'a) spmf"
where "funct_OT_14 M C = do {
let (c0,c1) = C;
let (m00, m01, m10, m11) = M;
return_spmf ((),if c0 then (if c1 then m11 else m10) else (if c1 then m01 else m00))}"

lemma lossless_funct_14_OT: "lossless_spmf (funct_OT_14 M C)"
by(simp add: funct_OT_14_def split_def)

end

# Theory ETP

subsection โน ETP definitions โบ

text โน We define Extended Trapdoor Permutations (ETPs) following \cite{DBLP:books/sp/17/Lindell17} and \cite{DBLP:books/cu/Goldreich2004}.
In particular we consider the property of Hard Core Predicates (HCPs). โบ

theory ETP imports
CryptHOL.CryptHOL
begin

type_synonym ('index,'range) dist2 = "(bool ร 'index ร bool ร bool) โ bool spmf"

type_synonym ('index,'range) advP2 = "'index โ bool โ bool โ ('index,'range) dist2 โ 'range โ bool spmf"

locale etp =
fixes I :: "('index ร 'trap) spmf" โ โนsamples index and trapdoorโบ
and domain :: "'index โ 'range set"
and range :: "'index โ 'range set"
and F :: "'index โ ('range โ 'range)" โ โนpermutationโบ
and Fโฉiโฉnโฉv :: "'index โ 'trap โ 'range โ 'range" โ โนmust be efficiently computableโบ
and B :: "'index โ 'range โ bool" โ โนhard core predicateโบ
assumes dom_eq_ran: "y โ set_spmf I โถ domain (fst y) = range (fst y)"
and finite_range: "y โ set_spmf I โถ finite (range (fst y))"
and non_empty_range: "y โ set_spmf I โถ range (fst y) โ  {}"
and bij_betw: "y โ set_spmf I โถ bij_betw (F (fst y)) (domain (fst y)) (range (fst y))"
and lossless_I: "lossless_spmf I"
and F_f_inv: "y โ set_spmf I โถ x โ range (fst y) โถ Fโฉiโฉnโฉv (fst y) (snd y) (F (fst y) x) = x"
begin

definition S :: "'index โ 'range spmf"
where "S ฮฑ = spmf_of_set (range ฮฑ)"

lemma lossless_S: "y โ set_spmf I โถ  lossless_spmf (S (fst y))"
by(simp add: lossless_spmf_def S_def finite_range non_empty_range)

lemma set_spmf_S [simp]: "y โ set_spmf I โถ set_spmf (S (fst y)) = range (fst y)"
by (simp add: S_def finite_range)

lemma f_inj_on: "y โ set_spmf I โถ inj_on (F (fst y)) (range (fst y))"
by(metis bij_betw_def bij_betw dom_eq_ran bij_betw_def bij_betw dom_eq_ran)

lemma range_f: "y โ set_spmf I โถ  x โ range (fst y) โถ F (fst y) x โ range (fst y)"
by (metis bij_betw bij_betw dom_eq_ran bij_betwE)

lemma f_inv_f [simp]: "y โ set_spmf I โถ x โ range (fst y) โถ Fโฉiโฉnโฉv (fst y) (snd y) (F (fst y) x) = x"
by (metis bij_betw bij_betw_inv_into_left dom_eq_ran F_f_inv)

lemma f_inv_f' [simp]: "y โ set_spmf I โถ x โ range (fst y) โถ Hilbert_Choice.inv_into (range (fst y)) (F (fst y)) (F (fst y) x) = x"
by (metis bij_betw bij_betw_inv_into_left bij_betw dom_eq_ran)

lemma B_F_inv_rewrite: "(B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ yโฉฯ') = (B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ yโฉฯ') = m1)) = m1"
by auto

lemma uni_set_samp:
assumes "y โ set_spmf I"
shows "map_spmf (ฮป x. F (fst y) x) (S (fst y)) = (S (fst y))"
(is "?lhs = ?rhs")
proof-
have rhs: "?rhs = spmf_of_set (range (fst y))"
unfolding S_def by(simp)
also have "map_spmf (ฮป x. F (fst y) x) (spmf_of_set (range (fst y))) = spmf_of_set ((ฮป x. F (fst y) x)  (range (fst y)))"
using f_inj_on assms
by (metis map_spmf_of_set_inj_on)
also have "(ฮป x. F (fst y) x)  (range (fst y)) = range (fst y)"
apply(rule endo_inj_surj)
using bij_betw
by (auto simp add: bij_betw_def dom_eq_ran f_inj_on bij_betw finite_range assms)
finally show ?thesis by(simp add: rhs)
qed

textโนWe define the security property of the hard core predicate (HCP) using a game.โบ

definition HCP_game :: "('index,'range) advP2 โ  bool โ bool โ ('index,'range) dist2 โ bool spmf"
where "HCP_game A = (ฮป ฯ bโฉฯ D. do {
(ฮฑ, ฯ) โ I;
x โ S ฮฑ;
b' โ A ฮฑ ฯ bโฉฯ D x;
let b = B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ x);
return_spmf (b = b')})"

definition "HCP_adv A ฯ bโฉฯ D = ยฆ((spmf (HCP_game A ฯ bโฉฯ D) True) - 1/2)ยฆ"

end

end



# Theory ETP_OT

subsection โน Oblivious transfer constructed from ETPs โบ

textโนHere we construct the OT protocol based on ETPs given in \cite{DBLP:books/sp/17/Lindell17} (Chapter 4) and prove
semi honest security for both parties. We show information theoretic security for Party 1 and reduce the security of
Party 2 to the HCP assumption.โบ

theory ETP_OT imports
"HOL-Number_Theory.Cong"
ETP
OT_Functionalities
Semi_Honest_Def
begin

type_synonym 'range viewP1 = "((bool ร bool) ร 'range ร 'range) spmf"
type_synonym 'range dist1 = "((bool ร bool) ร 'range ร 'range) โ bool spmf"
type_synonym 'index viewP2 = "(bool ร 'index ร (bool ร bool)) spmf"
type_synonym 'index dist2 = "(bool ร 'index ร bool ร bool) โ bool spmf"
type_synonym ('index, 'range) advP2 = "'index โ bool โ bool โ 'index dist2 โ 'range โ bool spmf"

lemma if_False_True: "(if x then False else ยฌ False) โท (if x then False else True)"
by simp

lemma if_then_True [simp]: "(if b then True else x) โท (ยฌ b โถ x)"
by simp

lemma if_else_True [simp]: "(if b then x else True) โท (b โถ x)"
by simp

lemma inj_on_Not [simp]: "inj_on Not A"
by(auto simp add: inj_on_def)

locale ETP_base = etp: etp I domain range F Fโฉiโฉnโฉv B
for I :: "('index ร 'trap) spmf" โ โนsamples index and trapdoorโบ
and domain :: "'index โ 'range set"
and range :: "'index โ 'range set"
and B :: "'index โ 'range โ bool" โ โนhard core predicateโบ
and F :: "'index โ 'range โ 'range"
and Fโฉiโฉnโฉv :: "'index โ 'trap โ 'range โ 'range"
begin

textโนThe probabilistic program that defines the protocol.โบ

definition protocol :: "(bool ร bool) โ bool โ (unit ร bool) spmf"
where "protocol inputโฉ1 ฯ = do {
let (bโฉฯ, bโฉฯ') = inputโฉ1;
(ฮฑ :: 'index, ฯ :: 'trap) โ I;
xโฉฯ :: 'range โ etp.S ฮฑ;
yโฉฯ' :: 'range โ etp.S ฮฑ;
let (yโฉฯ :: 'range) = F ฮฑ xโฉฯ;
let (xโฉฯ :: 'range) = Fโฉiโฉnโฉv ฮฑ ฯ yโฉฯ;
let (xโฉฯ' :: 'range) = Fโฉiโฉnโฉv ฮฑ ฯ yโฉฯ';
let (ฮฒโฉฯ :: bool) = xor (B ฮฑ xโฉฯ) bโฉฯ;
let (ฮฒโฉฯ' :: bool) = xor (B ฮฑ xโฉฯ') bโฉฯ';
return_spmf ((), if ฯ then xor (B ฮฑ xโฉฯ') ฮฒโฉฯ' else xor (B ฮฑ xโฉฯ) ฮฒโฉฯ)}"

lemma correctness: "protocol (m0,m1) c = funct_OT_12 (m0,m1) c"
proof-
have "(B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ yโฉฯ') = (B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ yโฉฯ') = m1)) = m1"
for ฮฑ ฯ yโฉฯ'  by auto
then show ?thesis
by(auto simp add: protocol_def funct_OT_12_def Let_def etp.B_F_inv_rewrite bind_spmf_const etp.lossless_S local.etp.lossless_I lossless_weight_spmfD split_def cong: bind_spmf_cong)
qed

text โน Party 1 views โบ

definition R1 :: "(bool ร bool) โ bool โ 'range viewP1"
where "R1 inputโฉ1 ฯ = do {
let (bโฉ0, bโฉ1) = inputโฉ1;
(ฮฑ, ฯ) โ I;
xโฉฯ โ etp.S ฮฑ;
yโฉฯ' โ etp.S ฮฑ;
let yโฉฯ = F ฮฑ xโฉฯ;
return_spmf ((bโฉ0, bโฉ1), if ฯ then yโฉฯ' else yโฉฯ, if ฯ then yโฉฯ else yโฉฯ')}"

lemma lossless_R1: "lossless_spmf (R1 msgs ฯ)"
by(simp add: R1_def local.etp.lossless_I split_def etp.lossless_S Let_def)

definition S1 :: "(bool ร bool) โ unit โ 'range viewP1"
where "S1 == (ฮป inputโฉ1 (). do {
let (bโฉ0, bโฉ1) = inputโฉ1;
(ฮฑ, ฯ) โ I;
yโฉ0 :: 'range โ etp.S ฮฑ;
yโฉ1 โ etp.S ฮฑ;
return_spmf ((bโฉ0, bโฉ1), yโฉ0, yโฉ1)})"

lemma lossless_S1: "lossless_spmf (S1 msgs ())"
by(simp add: S1_def local.etp.lossless_I split_def etp.lossless_S)

text โน Party 2 views โบ

definition R2 :: "(bool ร bool) โ bool โ 'index viewP2"
where "R2 msgs ฯ = do {
let (b0,b1) = msgs;
(ฮฑ, ฯ) โ I;
xโฉฯ โ etp.S ฮฑ;
yโฉฯ' โ etp.S ฮฑ;
let yโฉฯ = F ฮฑ xโฉฯ;
let xโฉฯ = Fโฉiโฉnโฉv ฮฑ ฯ yโฉฯ;
let xโฉฯ' = Fโฉiโฉnโฉv ฮฑ ฯ yโฉฯ';
let ฮฒโฉฯ = (B ฮฑ xโฉฯ) โ (if ฯ then b1 else b0) ;
let ฮฒโฉฯ' = (B ฮฑ xโฉฯ') โ (if ฯ then b0 else b1);
return_spmf (ฯ, ฮฑ,(ฮฒโฉฯ, ฮฒโฉฯ'))}"

lemma lossless_R2: "lossless_spmf (R2 msgs ฯ)"
by(simp add: R2_def split_def local.etp.lossless_I etp.lossless_S)

definition S2 :: "bool โ bool โ 'index viewP2"
where "S2 ฯ bโฉฯ = do {
(ฮฑ, ฯ) โ I;
xโฉฯ โ etp.S ฮฑ;
yโฉฯ' โ etp.S ฮฑ;
let xโฉฯ' = Fโฉiโฉnโฉv ฮฑ ฯ yโฉฯ';
let ฮฒโฉฯ = (B ฮฑ xโฉฯ) โ bโฉฯ;
let ฮฒโฉฯ' = B ฮฑ xโฉฯ';
return_spmf (ฯ, ฮฑ, (ฮฒโฉฯ, ฮฒโฉฯ'))}"

lemma lossless_S2: "lossless_spmf (S2 ฯ bโฉฯ)"
by(simp add: S2_def local.etp.lossless_I etp.lossless_S split_def)

text โน Security for Party 1 โบ

textโนWe have information theoretic security for Party 1.โบ

lemma P1_security: "R1 inputโฉ1 ฯ = funct_OT_12 x y โค (ฮป (s1, s2). S1 inputโฉ1 s1)"
including monad_normalisation
proof-
have "R1 inputโฉ1 ฯ =  do {
let (b0,b1) = inputโฉ1;
(ฮฑ, ฯ) โ I;
yโฉฯ' :: 'range โ etp.S ฮฑ;
yโฉฯ โ map_spmf (ฮป xโฉฯ. F ฮฑ xโฉฯ) (etp.S ฮฑ);
return_spmf ((b0,b1), if ฯ then yโฉฯ' else yโฉฯ, if ฯ then yโฉฯ else yโฉฯ')}"
by(simp add: bind_map_spmf o_def Let_def R1_def)
also have "... = do {
let (b0,b1) = inputโฉ1;
(ฮฑ, ฯ) โ I;
yโฉฯ' :: 'range โ etp.S ฮฑ;
yโฉฯ โ etp.S ฮฑ;
return_spmf ((b0,b1), if ฯ then yโฉฯ' else yโฉฯ, if ฯ then yโฉฯ else yโฉฯ')}"
by(simp add: etp.uni_set_samp Let_def split_def cong: bind_spmf_cong)
also have "... = funct_OT_12 x y โค (ฮป (s1, s2). S1 inputโฉ1 s1)"
by(cases ฯ; simp add: S1_def R1_def Let_def funct_OT_12_def)
ultimately show ?thesis by auto
qed

text โน The adversary used in proof of security for party 2 โบ

definition ๐ :: "('index, 'range) advP2"
where "๐ ฮฑ ฯ bโฉฯ D2 x = do {
ฮฒโฉฯ' โ coin_spmf;
xโฉฯ โ etp.S ฮฑ;
let ฮฒโฉฯ = (B ฮฑ xโฉฯ) โ bโฉฯ;
d โ D2(ฯ, ฮฑ, ฮฒโฉฯ, ฮฒโฉฯ');
return_spmf(if d then ฮฒโฉฯ' else ยฌ ฮฒโฉฯ')}"

lemma lossless_๐:
assumes "โ view. lossless_spmf (D2 view)"
shows "y โ set_spmf I โถ  lossless_spmf (๐ (fst y) ฯ bโฉฯ D2 x)"
by(simp add: ๐_def etp.lossless_S assms)

lemma assm_bound_funct_OT_12:
assumes "etp.HCP_adv ๐ ฯ (if ฯ then b1 else b0) D โค HCP_ad"
shows "ยฆspmf (funct_OT_12 (b0,b1) ฯ โค (ฮป (out1,out2).
etp.HCP_game ๐ ฯ out2 D)) True - 1/2ยฆ โค HCP_ad"
(is "?lhs โค HCP_ad")
proof-
have "?lhs = ยฆspmf (etp.HCP_game ๐ ฯ (if ฯ then b1 else b0) D) True - 1/2ยฆ"
by(simp add: funct_OT_12_def)
thus ?thesis using assms etp.HCP_adv_def by simp
qed

lemma assm_bound_funct_OT_12_collapse:
assumes "โ bโฉฯ. etp.HCP_adv ๐ ฯ bโฉฯ D โค HCP_ad"
shows "ยฆspmf (funct_OT_12 m1 ฯ โค (ฮป (out1,out2). etp.HCP_game ๐ ฯ out2 D)) True - 1/2ยฆ โค HCP_ad"
using assm_bound_funct_OT_12 surj_pair assms by metis

text โน To prove security for party 2 we split the proof on the cases on party 2's input โบ

lemma R2_S2_False:
assumes "((if ฯ then b0 else b1) = False)"
shows "spmf (R2 (b0,b1) ฯ โค (D2 :: (bool ร 'index ร bool ร bool) โ bool spmf)) True
= spmf (funct_OT_12 (b0,b1) ฯ โค (ฮป (out1,out2). S2 ฯ out2 โค D2)) True"
proof-
have "ฯ โน ยฌ b0" using assms by simp
moreover have "ยฌ ฯ โน ยฌ b1" using assms by simp
ultimately show ?thesis
by(auto simp add: R2_def S2_def split_def local.etp.F_f_inv assms funct_OT_12_def cong: bind_spmf_cong_simp)
qed

lemma R2_S2_True:
assumes "((if ฯ then b0 else b1) = True)"
and lossless_D: "โ a. lossless_spmf (D2 a)"
shows "ยฆ(spmf (bind_spmf (R2 (b0,b1) ฯ) D2) True) - spmf (funct_OT_12 (b0,b1) ฯ โค (ฮป (out1, out2). S2 ฯ out2 โค (ฮป view. D2 view))) Trueยฆ
= ยฆ2*((spmf (etp.HCP_game ๐ ฯ (if ฯ then b1 else b0) D2) True) - 1/2)ยฆ"
proof-
have  "(spmf (funct_OT_12 (b0,b1) ฯ โค (ฮป (out1, out2). S2 ฯ out2 โค D2)) True
- spmf (bind_spmf (R2 (b0,b1) ฯ) D2) True)
= 2 * ((spmf (etp.HCP_game ๐ ฯ (if ฯ then b1 else b0) D2) True) - 1/2)"
proof-
have  "((spmf (etp.HCP_game ๐ ฯ (if ฯ then b1 else b0) D2) True) - 1/2)  =
1/2*(spmf (bind_spmf (S2 ฯ (if ฯ then b1 else b0)) D2) True
- spmf (bind_spmf (R2 (b0,b1) ฯ) D2) True)"
including monad_normalisation
proof-
have ฯ_true_b0_true: "ฯ โน b0 = True" using assms(1) by simp
have ฯ_false_b1_true: "ยฌ ฯ โน b1" using assms(1) by simp
have return_True_False: "spmf (return_spmf (ยฌ d)) True = spmf (return_spmf d) False"
for d by(cases d; simp)
define HCP_game_true where "HCP_game_true == ฮป ฯ bโฉฯ. do {
(ฮฑ, ฯ) โ I;
xโฉฯ โ etp.S ฮฑ;
x โ (etp.S ฮฑ);
let ฮฒโฉฯ = (B ฮฑ xโฉฯ) โ bโฉฯ;
let ฮฒโฉฯ' = B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ x);
d โ D2(ฯ, ฮฑ, ฮฒโฉฯ, ฮฒโฉฯ');
let b' = (if d then ฮฒโฉฯ' else ยฌ ฮฒโฉฯ');
let b = B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ x);
return_spmf (b = b')}"
define HCP_game_false where "HCP_game_false == ฮป ฯ bโฉฯ. do {
(ฮฑ, ฯ) โ I;
xโฉฯ โ etp.S ฮฑ;
x โ (etp.S ฮฑ);
let ฮฒโฉฯ = (B ฮฑ xโฉฯ) โ bโฉฯ;
let ฮฒโฉฯ' = ยฌ B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ x);
d โ D2(ฯ, ฮฑ, ฮฒโฉฯ, ฮฒโฉฯ');
let b' = (if d then ฮฒโฉฯ' else ยฌ ฮฒโฉฯ');
let b = B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ x);
return_spmf (b = b')}"
define HCP_game_๐ where "HCP_game_๐ == ฮป ฯ bโฉฯ. do {
ฮฒโฉฯ' โ coin_spmf;
(ฮฑ, ฯ) โ I;
x โ etp.S ฮฑ;
x' โ etp.S ฮฑ;
d โ D2 (ฯ, ฮฑ, (B ฮฑ x) โ bโฉฯ, ฮฒโฉฯ');
let b' = (if d then  ฮฒโฉฯ' else ยฌ ฮฒโฉฯ');
return_spmf (B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ x') = b')}"
define S2D where "S2D == ฮป ฯ bโฉฯ . do {
(ฮฑ, ฯ) โ I;
xโฉฯ โ etp.S ฮฑ;
yโฉฯ' โ etp.S ฮฑ;
let xโฉฯ' = Fโฉiโฉnโฉv ฮฑ ฯ yโฉฯ';
let ฮฒโฉฯ = (B ฮฑ xโฉฯ) โ bโฉฯ;
let ฮฒโฉฯ' = B ฮฑ xโฉฯ';
d :: bool โ D2(ฯ, ฮฑ, ฮฒโฉฯ, ฮฒโฉฯ');
return_spmf d}"
define R2D where "R2D == ฮป msgs ฯ.  do {
let (b0,b1) = msgs;
(ฮฑ, ฯ) โ I;
xโฉฯ โ etp.S ฮฑ;
yโฉฯ' โ etp.S ฮฑ;
let yโฉฯ = F ฮฑ xโฉฯ;
let xโฉฯ = Fโฉiโฉnโฉv ฮฑ ฯ yโฉฯ;
let xโฉฯ' = Fโฉiโฉnโฉv ฮฑ ฯ yโฉฯ';
let ฮฒโฉฯ = (B ฮฑ xโฉฯ) โ (if ฯ then b1 else b0) ;
let ฮฒโฉฯ' = (B ฮฑ xโฉฯ') โ (if ฯ then b0 else b1);
b :: bool โ D2(ฯ, ฮฑ,(ฮฒโฉฯ, ฮฒโฉฯ'));
return_spmf b}"
define D_true where "D_true  == ฮปฯ bโฉฯ. do {
(ฮฑ, ฯ) โ I;
xโฉฯ โ etp.S ฮฑ;
x โ (etp.S ฮฑ);
let ฮฒโฉฯ = (B ฮฑ xโฉฯ) โ bโฉฯ;
let ฮฒโฉฯ' = B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ x);
d :: bool โ D2(ฯ, ฮฑ, ฮฒโฉฯ, ฮฒโฉฯ');
return_spmf d}"
define D_false where "D_false == ฮป ฯ bโฉฯ. do {
(ฮฑ, ฯ) โ I;
xโฉฯ โ etp.S ฮฑ;
x โ etp.S ฮฑ;
let ฮฒโฉฯ = (B ฮฑ xโฉฯ) โ bโฉฯ;
let ฮฒโฉฯ' = ยฌ B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ x);
d :: bool โ D2(ฯ, ฮฑ, ฮฒโฉฯ, ฮฒโฉฯ');
return_spmf d}"
have lossless_D_false: "lossless_spmf (D_false ฯ (if ฯ then b1 else b0))"
apply(auto simp add: D_false_def lossless_D local.etp.lossless_I)
using local.etp.lossless_S by auto
have "spmf (etp.HCP_game ๐ ฯ (if ฯ then b1 else b0) D2) True =  spmf (HCP_game_๐ ฯ (if ฯ then b1 else b0)) True"
apply(simp add: etp.HCP_game_def HCP_game_๐_def ๐_def split_def etp.F_f_inv)
by(rewrite bind_commute_spmf[where q = "coin_spmf"]; rewrite bind_commute_spmf[where q = "coin_spmf"]; rewrite bind_commute_spmf[where q = "coin_spmf"]; auto)+
also have "... = spmf (bind_spmf (map_spmf Not coin_spmf) (ฮปb. if b then HCP_game_true ฯ (if ฯ then b1 else b0) else HCP_game_false ฯ (if ฯ then b1 else b0))) True"
unfolding HCP_game_๐_def HCP_game_true_def HCP_game_false_def ๐_def Let_def
apply(simp add: split_def cong: if_cong)
supply [[simproc del: monad_normalisation]]
apply(subst if_distrib[where f = "bind_spmf _" for f, symmetric]; simp cong: bind_spmf_cong add: if_distribR )+
apply(rewrite in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ"  in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "โ = _" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "โ = _" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "โ = _" bind_commute_spmf)
apply(fold map_spmf_conv_bind_spmf)
apply(rule conjI; rule impI; simp)
apply(simp only: spmf_bind)
apply(rule Bochner_Integration.integral_cong[OF refl])+
apply clarify
subgoal for r rโฉฯ ฮฑ ฯ
apply(simp only: UNIV_bool spmf_of_set integral_spmf_of_set)
apply(simp cong: if_cong split del: if_split)
apply(cases "B r (Fโฉiโฉnโฉv r rโฉฯ ฯ)")
by auto
apply(rewrite in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ"  in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "โ = _" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "โ = _" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "โ = _" bind_commute_spmf)
apply(simp only: spmf_bind)
apply(rule Bochner_Integration.integral_cong[OF refl])+
apply clarify
subgoal for r rโฉฯ ฮฑ ฯ
apply(simp only: UNIV_bool spmf_of_set integral_spmf_of_set)
apply(simp cong: if_cong split del: if_split)
apply(cases " B r (Fโฉiโฉnโฉv r rโฉฯ ฯ)")
by auto
done
also have "... = 1/2*(spmf (HCP_game_true ฯ (if ฯ then b1 else b0)) True) + 1/2*(spmf (HCP_game_false ฯ (if ฯ then b1 else b0)) True)"
by(simp add: spmf_bind UNIV_bool spmf_of_set integral_spmf_of_set)
also have "... = 1/2*(spmf (D_true ฯ (if ฯ then b1 else b0)) True) + 1/2*(spmf (D_false ฯ (if ฯ then b1 else b0)) False)"
proof-
have "spmf (I โค (ฮป(ฮฑ, ฯ). etp.S ฮฑ โค (ฮปxโฉฯ. etp.S ฮฑ โค (ฮปx. D2 (ฯ, ฮฑ, B ฮฑ xโฉฯ = (ยฌ (if ฯ then b1 else b0)), ยฌ B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ x)) โค (ฮปd. return_spmf (ยฌ d)))))) True
= spmf (I โค (ฮป(ฮฑ, ฯ). etp.S ฮฑ โค (ฮปxโฉฯ. etp.S ฮฑ โค (ฮปx. D2 (ฯ, ฮฑ, B ฮฑ xโฉฯ = (ยฌ (if ฯ then b1 else b0)), ยฌ B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ x)))))) False"
(is "?lhs = ?rhs")
proof-
have "?lhs = spmf (I โค (ฮป(ฮฑ, ฯ). etp.S ฮฑ โค (ฮปxโฉฯ. etp.S ฮฑ โค (ฮปx. D2 (ฯ, ฮฑ, B ฮฑ xโฉฯ = (ยฌ (if ฯ then b1 else b0)), ยฌ B ฮฑ (Fโฉiโฉnโฉv ฮฑ ฯ x)) โค (ฮปd. return_spmf (d)))))) False"
by(simp only: split_def return_True_False spmf_bind)
then show ?thesis by simp
qed
then show ?thesis  by(simp add: HCP_game_true_def HCP_game_false_def Let_def D_true_def D_false_def if_distrib[where f="(=) _"] cong: if_cong)
qed
also have "... =  1/2*((spmf (D_true ฯ (if ฯ then b1 else b0) ) True) + (1 - spmf (D_false ฯ (if ฯ then b1 else b0) ) True))"
by(simp add: spmf_False_conv_True lossless_D_false)
also have "... = 1/2 + 1/2* (spmf (D_true ฯ (if ฯ then b1 else b0)) True) - 1/2*(spmf (D_false ฯ (if ฯ then b1 else b0)) True)"
by(simp)
also have "... =  1/2 + 1/2* (spmf (S2D ฯ (if ฯ then b1 else b0) ) True) - 1/2*(spmf (R2D (b0,b1) ฯ ) True)"
apply(auto  simp add: local.etp.F_f_inv S2D_def R2D_def D_true_def D_false_def  assms split_def cong: bind_spmf_cong_simp)
apply(simp add: ฯ_true_b0_true)
by(simp add: ฯ_false_b1_true)
ultimately show ?thesis by(simp add: S2D_def R2D_def R2_def S2_def split_def)
qed
then show ?thesis by(auto simp add: funct_OT_12_def)
qed
thus ?thesis by simp
qed

lemma P2_adv_bound:
assumes lossless_D: "โ a. lossless_spmf (D2 a)"
shows "ยฆ(spmf (bind_spmf (R2 (b0,b1) ฯ) D2) True) - spmf (funct_OT_12 (b0,b1) ฯ โค (ฮป (out1, out2). S2 ฯ out2 โค (ฮป view. D2 view))) Trueยฆ
โค ยฆ2*((spmf (etp.HCP_game ๐ ฯ (if ฯ then b1 else b0) D2) True) - 1/2)ยฆ"
by(cases "(if ฯ then b0 else b1)"; auto simp add: R2_S2_False R2_S2_True assms)

sublocale OT_12: sim_det_def R1 S1 R2 S2 funct_OT_12 protocol
unfolding sim_det_def_def
by(simp add: lossless_R1 lossless_S1 lossless_R2 lossless_S2 funct_OT_12_def)

lemma correct: "OT_12.correctness m1 m2"
unfolding OT_12.correctness_def
by (metis prod.collapse correctness)

lemma P1_security_inf_the: "OT_12.perfect_sec_P1 m1 m2"
unfolding OT_12.perfect_sec_P1_def using P1_security by simp

lemma P2_security:
assumes "โ a. lossless_spmf (D a)"
and "โ bโฉฯ. etp.HCP_adv ๐ m2 bโฉฯ D โค HCP_ad"
shows "OT_12.adv_P2 m1 m2 D โค 2 * HCP_ad"
proof-
have "spmf (etp.HCP_game ๐ ฯ (if ฯ then b1 else b0) D) True = spmf (funct_OT_12 (b0,b1) ฯ โค (ฮป (out1, out2). etp.HCP_game ๐ ฯ out2 D)) True"
for ฯ b0 b1
by(simp add: funct_OT_12_def)
hence "OT_12.adv_P2 m1 m2 D โค ยฆ2*((spmf (funct_OT_12 m1 m2 โค (ฮป (out1, out2). etp.HCP_game ๐ m2 out2 D)) True) - 1/2)ยฆ"
unfolding OT_12.adv_P2_def using P2_adv_bound assms surj_pair prod.collapse by metis
moreover have "ยฆ2*((spmf (funct_OT_12 m1 m2 โค (ฮป (out1, out2). etp.HCP_game ๐ m2 out2 D)) True) - 1/2)ยฆ โค ยฆ2*HCP_adยฆ"
proof -
have "(โr. ยฆ(1::real) / rยฆ โ  1 / ยฆrยฆ) โจ 2 / ยฆ1 / (spmf (funct_OT_12 m1 m2
โค (ฮป(x, y). ((ฮปu b. etp.HCP_game ๐ m2 b D)::unit โ bool โ bool spmf) x y)) True - 1 / 2)ยฆ
โค HCP_ad / (1 / 2)"
using assm_bound_funct_OT_12_collapse assms by auto
then show ?thesis
by fastforce
qed
moreover have "HCP_ad โฅ 0"
using assms(2)  local.etp.HCP_adv_def by auto
ultimately show ?thesis by argo
qed

end

text โน We also consider the asymptotic case for security proofs โบ

locale ETP_sec_para =
fixes I :: "nat โ ('index ร 'trap) spmf"
and domain ::  "'index โ 'range set"
and range ::  "'index โ 'range set"
and f :: "'index โ ('range โ 'range)"
and F :: "'index โ 'range โ 'range"
and Fโฉiโฉnโฉv :: "'index โ 'trap โ 'range โ 'range"
and B :: "'index โ 'range โ bool"
assumes ETP_base: "โ n. ETP_base (I n) domain range F Fโฉiโฉnโฉv"
begin

sublocale ETP_base "(I n)" domain range
using ETP_base  by simp

lemma correct_asym: "OT_12.correctness n m1 m2"
by(simp add: correct)

lemma P1_sec_asym: "OT_12.perfect_sec_P1 n m1 m2"
using P1_security_inf_the by simp

lemma P2_sec_asym:
assumes "โ a. lossless_spmf (D a)"
and HCP_adv_neg: "negligible (ฮป n. etp_advantage n)"
and etp_adv_bound: "โ bโฉฯ n. etp.HCP_adv n ๐ m2 bโฉฯ D โค etp_advantage n"
shows "negligible (ฮป n. OT_12.adv_P2 n m1 m2 D)"
proof-
have "negligible (ฮป n. 2 * etp_advantage n)" using HCP_adv_neg
by (simp add: negligible_cmultI)
moreover have "ยฆOT_12.adv_P2 n m1 m2 Dยฆ = OT_12.adv_P2 n m1 m2 D" for n unfolding OT_12.adv_P2_def by simp
moreover have  "OT_12.adv_P2 n m1 m2 D โค 2 * etp_advantage n" for n using assms P2_security by blast
ultimately show ?thesis
using assms negligible_le HCP_adv_neg P2_security by presburger
qed

end

end

# Theory ETP_RSA_OT

subsubsection โน RSA instantiation โบ

textโนIt is known that the RSA collection forms an ETP. Here we instantitate our proof of security for OT
that uses a general ETP for RSA. We use the proof of the general construction of OT. The main proof effort
here is in showing the RSA collection meets the requirements of an ETP, mainly this involves showing the
RSA mapping is a bijection.โบ

theory ETP_RSA_OT imports
ETP_OT
Number_Theory_Aux
Uniform_Sampling
begin

type_synonym index = "(nat ร nat)"
type_synonym trap = nat
type_synonym range = nat
type_synonym domain = nat
type_synonym viewP1 = "((bool ร bool) ร nat ร nat) spmf"
type_synonym viewP2 = "(bool ร index ร (bool ร bool)) spmf"
type_synonym dist2 = "(bool ร index ร bool ร bool) โ bool spmf"
type_synonym advP2 = "index โ bool โ bool โ dist2 โ bool spmf"

locale rsa_base =
fixes prime_set :: "nat set" โ โนthe set of primes usedโบ
and B :: "index โ nat โ bool"
assumes prime_set_ass: "prime_set โ {x. prime x โง x > 2}"
and finite_prime_set: "finite prime_set"
and prime_set_gt_2: "card prime_set > 2"
begin

lemma prime_set_non_empty: "prime_set โ  {}"
using prime_set_gt_2 by auto

definition coprime_set :: "nat โ nat set"
where "coprime_set N โก {x. coprime x N โง x > 1 โง x < N}"

lemma coprime_set_non_empty:
assumes "N > 2"
shows "coprime_set N โ  {}"
by(simp add: coprime_set_def; metis assms(1) Suc_lessE coprime_Suc_right_nat lessI numeral_2_eq_2)

definition sample_coprime :: "nat โ nat spmf"
where "sample_coprime N = spmf_of_set (coprime_set (N))"

lemma sample_coprime_e_gt_1:
assumes "e โ set_spmf (sample_coprime N)"
shows "e > 1"
using assms by(simp add: sample_coprime_def coprime_set_def)

lemma lossless_sample_coprime:
assumes "ยฌ prime N"
and "N > 2"
shows  "lossless_spmf (sample_coprime N)"
proof-
have "coprime_set N โ  {}"
by(simp add: coprime_set_non_empty assms)
also have "finite (coprime_set N)"
by(simp add: coprime_set_def)
ultimately show ?thesis by(simp add: sample_coprime_def)
qed

lemma set_spmf_sample_coprime:
shows "set_spmf (sample_coprime N) = {x. coprime x N โง x > 1 โง x < N}"
by(simp add: sample_coprime_def coprime_set_def)

definition sample_primes :: "nat spmf"
where "sample_primes = spmf_of_set prime_set"

lemma lossless_sample_primes:
shows "lossless_spmf sample_primes"
by(simp add: sample_primes_def prime_set_non_empty finite_prime_set)

lemma set_spmf_sample_primes:
shows "set_spmf sample_primes โ {x. prime x โง x > 2}"
by(auto simp add: sample_primes_def prime_set_ass finite_prime_set)

lemma mem_samp_primes_gt_2:
shows "x โ set_spmf sample_primes โน x > 2"
apply (simp add: finite_prime_set sample_primes_def)
using prime_set_ass by blast

lemma mem_samp_primes_prime:
shows "x โ set_spmf sample_primes โน prime x"
apply (simp add: finite_prime_set sample_primes_def prime_set_ass)
using prime_set_ass by blast

definition sample_primes_excl :: "nat set โ nat spmf"
where "sample_primes_excl P = spmf_of_set (prime_set - P)"

lemma lossless_sample_primes_excl:
shows "lossless_spmf (sample_primes_excl {P})"
apply(simp add: sample_primes_excl_def finite_prime_set)
using prime_set_gt_2 subset_singletonD by fastforce

definition sample_set_excl :: "nat set โ nat set โ nat spmf"
where "sample_set_excl Q P = spmf_of_set (Q - P)"

lemma set_spmf_sample_set_excl [simp]:
assumes "finite (Q - P)"
shows "set_spmf (sample_set_excl Q P) = (Q - P)"
unfolding  sample_set_excl_def
by (metis set_spmf_of_set assms)+

lemma lossless_sample_set_excl:
assumes "finite Q"
and "card Q > 2"
shows "lossless_spmf (sample_set_excl Q {P})"
unfolding sample_set_excl_def
using assms subset_singletonD by fastforce

lemma mem_samp_primes_excl_gt_2:
shows "x โ set_spmf (sample_set_excl prime_set {y}) โน x > 2"
apply(simp add: finite_prime_set sample_set_excl_def  prime_set_ass )
using prime_set_ass by blast

lemma mem_samp_primes_excl_prime :
shows "x โ set_spmf (sample_set_excl prime_set {y}) โน prime x"
apply (simp add: finite_prime_set sample_set_excl_def)
using prime_set_ass by blast

lemma sample_coprime_lem:
assumes "x โ set_spmf sample_primes"
and " y โ set_spmf (sample_set_excl prime_set {x}) "
shows "lossless_spmf (sample_coprime ((x - Suc 0) * (y - Suc 0)))"
proof-
have gt_2: "x > 2" "y > 2"
using mem_samp_primes_gt_2 assms mem_samp_primes_excl_gt_2 by auto
have "ยฌ prime ((x-1)*(y-1))"
proof-
have "prime x" "prime y"
using mem_samp_primes_prime mem_samp_primes_excl_prime assms by auto
then show ?thesis using prod_not_prime gt_2 by simp
qed
also have "((x-1)*(y-1)) > 2"
by (metis (no_types, lifting) gt_2 One_nat_def Suc_diff_1 assms(1) assms(2) calculation
divisors_zero less_2_cases nat_1_eq_mult_iff nat_neq_iff not_numeral_less_one numeral_2_eq_2
prime_gt_0_nat rsa_base.mem_samp_primes_excl_prime rsa_base.mem_samp_primes_prime rsa_base_axioms two_is_prime_nat)
ultimately show ?thesis using lossless_sample_coprime by simp
qed

definition I :: "(index ร trap) spmf"
where "I = do {
P โ sample_primes;
Q โ sample_set_excl prime_set {P};
let N = P*Q;
let N' = (P-1)*(Q-1);
e โ sample_coprime N';
let d = nat ((fst (bezw e N')) mod N');
return_spmf ((N, e), d)}"

lemma lossless_I: "lossless_spmf I"
by(auto simp add: I_def lossless_sample_primes lossless_sample_set_excl finite_prime_set prime_set_gt_2 Let_def sample_coprime_lem)

lemma set_spmf_I_N:
assumes "((N,e),d) โ set_spmf I"
obtains P Q where "N = P * Q"
and "P โ  Q"
and "prime P"
and "prime Q"
and "coprime e ((P - 1)*(Q - 1))"
and "d = nat (fst (bezw e ((P-1)*(Q-1))) mod int ((P-1)*(Q-1)))"
using assms apply(auto simp add: I_def Let_def)
using finite_prime_set mem_samp_primes_prime sample_set_excl_def rsa_base_axioms sample_primes_def
by (simp add: set_spmf_sample_coprime)

lemma set_spmf_I_e_d:
assumes "((N,e),d) โ set_spmf I"
shows "e > 1" and "d > 1"
using assms sample_coprime_e_gt_1
apply(auto simp add: I_def Let_def)
by (smt Euclidean_Division.pos_mod_sign Num.of_nat_simps(5) Suc_diff_1 bezw_inverse cong_def coprime_imp_gcd_eq_1 gr0I less_1_mult less_numeral_extra(2) mem_Collect_eq mod_by_0 mod_less more_arith_simps(6) nat_0 nat_0_less_mult_iff nat_int nat_neq_iff numerals(2) of_nat_0_le_iff of_nat_1 rsa_base.mem_samp_primes_gt_2 rsa_base_axioms set_spmf_sample_coprime zero_less_diff)

definition domain :: "index โ nat set"
where "domain index โก {..< fst index}"

definition range :: "index โ nat set"
where "range index โก {..< fst index}"

lemma finite_range: "finite (range index)"
by(simp add: range_def)

lemma dom_eq_ran: "domain index = range index"
by(simp add: range_def domain_def)

definition F :: "index โ (nat โ nat)"
where "F index x = x ^ (snd index) mod (fst index)"

definition Fโฉiโฉnโฉv :: "index โ trap โ nat โ nat"
where "Fโฉiโฉnโฉv ฮฑ ฯ y = y ^ ฯ mod (fst ฮฑ)"

text โน We must prove the RSA function is a bijection โบ

lemma rsa_bijection:
assumes coprime: "coprime e ((P-1)*(Q-1))"
and prime_P: "prime (P::nat)"
and prime_Q: "prime Q"
and P_neq_Q: "P โ  Q"
and x_lt_pq: "x < P * Q"
and y_lt_pd: "y < P * Q"
and rsa_map_eq: "x ^ e mod (P * Q) = y ^ e mod (P * Q)"
shows "x = y"
proof-
have flt_xP: "[x ^ P = x] (mod P)"
using fermat_little prime_P by blast
have flt_yP: "[y ^ P = y] (mod P)"
using fermat_little prime_P by blast
have flt_xQ: "[x ^ Q = x] (mod Q)"
using fermat_little prime_Q by blast
have flt_yQ: "[y ^ Q = y] (mod Q)"
using fermat_little prime_Q by blast
show ?thesis
proof(cases "y โฅ x")
case True
hence ye_gt_xe: "y^e โฅ x^e"
by (simp add: power_mono)
have x_y_exp_e: "[x^e = y^e] (mod P)"
using cong_modulus_mult_nat  cong_altdef_nat True ye_gt_xe cong_sym cong_def assms by blast
obtain d where d:  "[e*d = 1] (mod (P-1)) โง d โ  0"
using ex_inverse assms by blast
then obtain k where k: "e*d = 1 + k*(P-1)"
using ex_k_mod assms by blast
hence xk_yk: "[x^(1 + k*(P-1)) = y^(1 + k*(P-1))] (mod P)"
by(metis k power_mult x_y_exp_e cong_pow)
have xk_x: "[x^(1 + k*(P-1)) = x] (mod P)"
proof(induct k)
case 0
then show ?case by simp
next
case (Suc k)
assume  asm: "[x ^ (1 + k * (P - 1)) = x] (mod P)"
then show ?case
proof-
have exp_rewrite: "(k * (P - 1) + P) = (1 + (k + 1) * (P - 1))"
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_P prime_gt_1_nat semiring_normalization_rules(3))
have "[x * x ^ (k * (P - 1)) = x] (mod P)" using asm by simp
hence "[x ^ (k * (P - 1)) * x ^ P = x] (mod P)" using flt_xP
by (metis cong_scalar_right cong_trans mult.commute)
hence "[x ^ (k * (P - 1) + P) = x] (mod P)"
by (simp add: power_add)
hence "[x ^ (1 + (k + 1) * (P - 1)) = x] (mod P)"
using exp_rewrite by argo
thus ?thesis by simp
qed
qed
have yk_y: "[y^(1 + k*(P-1)) = y] (mod P)"
proof(induct k)
case 0
then show ?case by simp
next
case (Suc k)
assume  asm: "[y ^ (1 + k * (P - 1)) = y] (mod P)"
then show ?case
proof-
have exp_rewrite: "(k * (P - 1) + P) = (1 + (k + 1) * (P - 1))"
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_P prime_gt_1_nat semiring_normalization_rules(3))
have "[y * y ^ (k * (P - 1)) = y] (mod P)" using asm by simp
hence "[y ^ (k * (P - 1)) * y ^ P = y] (mod P)" using flt_yP
by (metis cong_scalar_right cong_trans mult.commute)
hence "[y ^ (k * (P - 1) + P) = y] (mod P)"
by (simp add: power_add)
hence "[y ^ (1 + (k + 1) * (P - 1)) = y] (mod P)"
using exp_rewrite by argo
thus ?thesis by simp
qed
qed
have "[x^e = y^e] (mod Q)"
by (metis rsa_map_eq cong_modulus_mult_nat cong_def mult.commute)
obtain d' where d':  "[e*d' = 1] (mod (Q-1)) โง d' โ  0"
by (metis mult.commute ex_inverse prime_P prime_Q P_neq_Q coprime)
then obtain k' where k': "e*d' = 1 + k'*(Q-1)"
by(metis ex_k_mod mult.commute prime_P prime_Q P_neq_Q coprime)
hence xk_yk': "[x^(1 + k'*(Q-1)) = y^(1 + k'*(Q-1))] (mod Q)"
by(metis k' power_mult โน[x ^ e = y ^ e] (mod Q)โบ cong_pow)
have xk_x': "[x^(1 + k'*(Q-1)) = x] (mod Q)"
proof(induct k')
case 0
then show ?case by simp
next
case (Suc k')
assume  asm: "[x ^ (1 + k' * (Q - 1)) = x] (mod Q)"
then show ?case
proof-
have exp_rewrite: "(k' * (Q - 1) + Q) = (1 + (k' + 1) * (Q - 1))"
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_Q prime_gt_1_nat semiring_normalization_rules(3))
have "[x * x ^ (k' * (Q - 1)) = x] (mod Q)" using asm by simp
hence "[x ^ (k' * (Q - 1)) * x ^ Q = x] (mod Q)" using flt_xQ
by (metis cong_scalar_right cong_trans mult.commute)
hence "[x ^ (k' * (Q - 1) + Q) = x] (mod Q)"
by (simp add: power_add)
hence "[x ^ (1 + (k' + 1) * (Q - 1)) = x] (mod Q)"
using exp_rewrite by argo
thus ?thesis by simp
qed
qed
have yk_y': "[y^(1 + k'*(Q-1)) = y] (mod Q)"
proof(induct k')
case 0
then show ?case by simp
next
case (Suc k')
assume  asm: "[y ^ (1 + k' * (Q - 1)) = y] (mod Q)"
then show ?case
proof-
have exp_rewrite: "(k' * (Q - 1) + Q) = (1 + (k' + 1) * (Q - 1))"
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_Q prime_gt_1_nat semiring_normalization_rules(3))
have "[y * y ^ (k' * (Q - 1)) = y] (mod Q)" using asm by simp
hence "[y ^ (k' * (Q - 1)) * y ^ Q = y] (mod Q)" using flt_yQ
by (metis cong_scalar_right cong_trans mult.commute)
hence "[y ^ (k' * (Q - 1) + Q) = y] (mod Q)"
by (simp add: power_add)
hence "[y ^ (1 + (k' + 1) * (Q - 1)) = y] (mod Q)"
using exp_rewrite by argo
thus ?thesis by simp
qed
qed
have P_dvd_xy: "P dvd (y - x)"
proof-
have "[x = y] (mod P)"
using xk_x yk_y xk_yk
by (simp add: cong_def)
thus ?thesis
using cong_altdef_nat cong_sym True by blast
qed
have Q_dvd_xy: "Q dvd (y - x)"
proof-
have "[x = y] (mod Q)"
using xk_x' yk_y' xk_yk'
by (simp add: cong_def)
thus ?thesis
using cong_altdef_nat cong_sym True by blast
qed
show ?thesis
proof-
have "P*Q dvd (y - x)" using P_dvd_xy  Q_dvd_xy
by (simp add: assms divides_mult primes_coprime)
then have "[x = y] (mod P*Q)"
by (simp add: cong_altdef_nat cong_sym True)
hence "x mod P*Q = y mod P*Q"
using  cong_def xk_x xk_yk yk_y by metis
then show ?thesis
using โน[x = y] (mod P * Q)โบ cong_less_modulus_unique_nat x_lt_pq y_lt_pd by blast
qed
next
case False
hence ye_gt_xe: "x^e โฅ y^e"
by (simp add: power_mono)
have pow_eq: "[x^e = y^e] (mod P*Q)"
by (simp add: cong_def assms)
then have PQ_dvd_ye_xe: "(P*Q) dvd (x^e - y^e)"
using cong_altdef_nat False ye_gt_xe cong_sym by blast
then have "[x^e = y^e] (mod P)"
using cong_modulus_mult_nat pow_eq by blast
obtain d where d:  "[e*d = 1] (mod (P-1)) โง d โ  0" using ex_inverse assms
by blast
then obtain k where k: "e*d = 1 + k*(P-1)" using ex_k_mod assms by blast
have xk_yk: "[x^(1 + k*(P-1)) = y^(1 + k*(P-1))] (mod P)"
proof-
have "[(x^e)^d = (y^e)^d] (mod P)"
using โน[x ^ e = y ^ e] (mod P)โบ cong_pow by blast
then have "[x^(e*d) = y^(e*d)] (mod P)"
by (simp add: power_mult)
thus ?thesis using k by simp
qed
have xk_x: "[x^(1 + k*(P-1)) = x] (mod P)"
proof(induct k)
case 0
then show ?case by simp
next
case (Suc k)
assume  asm: "[x ^ (1 + k * (P - 1)) = x] (mod P)"
then show ?case
proof-
have exp_rewrite: "(k * (P - 1) + P) = (1 + (k + 1) * (P - 1))"
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_P prime_gt_1_nat semiring_normalization_rules(3))
have "[x * x ^ (k * (P - 1)) = x] (mod P)" using asm by simp
hence "[x ^ (k * (P - 1)) * x ^ P = x] (mod P)" using flt_xP
by (metis cong_scalar_right cong_trans mult.commute)
hence "[x ^ (k * (P - 1) + P) = x] (mod P)"
by (simp add: power_add)
hence "[x ^ (1 + (k + 1) * (P - 1)) = x] (mod P)"
using exp_rewrite by argo
thus ?thesis by simp
qed
qed
have yk_y: "[y^(1 + k*(P-1)) = y] (mod P)"
proof(induct k)
case 0
then show ?case by simp
next
case (Suc k)
assume  asm: "[y ^ (1 + k * (P - 1)) = y] (mod P)"
then show ?case
proof-
have exp_rewrite: "(k * (P - 1) + P) = (1 + (k + 1) * (P - 1))"
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_P prime_gt_1_nat semiring_normalization_rules(3))
have "[y * y ^ (k * (P - 1)) = y] (mod P)" using asm by simp
hence "[y ^ (k * (P - 1)) * y ^ P = y] (mod P)" using flt_yP
by (metis cong_scalar_right cong_trans mult.commute)
hence "[y ^ (k * (P - 1) + P) = y] (mod P)"
by (simp add: power_add)
hence "[y ^ (1 + (k + 1) * (P - 1)) = y] (mod P)"
using exp_rewrite by argo
thus ?thesis by simp
qed
qed
have P_dvd_xy: "P dvd (x - y)"
proof-
have "[x = y] (mod P)" using xk_x yk_y xk_yk
by (simp add: cong_def)
thus ?thesis
using cong_altdef_nat cong_sym False by simp
qed
have "[x^e = y^e] (mod Q)"
using cong_modulus_mult_nat pow_eq PQ_dvd_ye_xe cong_dvd_modulus_nat dvd_triv_right by blast
obtain d' where d':  "[e*d' = 1] (mod (Q-1)) โง d' โ  0"
by (metis mult.commute ex_inverse prime_P prime_Q coprime P_neq_Q)
then obtain k' where k': "e*d' = 1 + k'*(Q-1)"
by(metis ex_k_mod mult.commute prime_P prime_Q coprime P_neq_Q)
have xk_yk': "[x^(1 + k'*(Q-1)) = y^(1 + k'*(Q-1))] (mod Q)"
proof-
have "[(x^e)^d' = (y^e)^d'] (mod Q)"
using โน[x ^ e = y ^ e] (mod Q)โบ cong_pow by blast
then have "[x^(e*d') = y^(e*d')] (mod Q)"
by (simp add: power_mult)
thus ?thesis using k'
by simp
qed
have xk_x': "[x^(1 + k'*(Q-1)) = x] (mod Q)"
proof(induct k')
case 0
then show ?case by simp
next
case (Suc k')
assume  asm: "[x ^ (1 + k' * (Q - 1)) = x] (mod Q)"
then show ?case
proof-
have exp_rewrite: "(k' * (Q - 1) + Q) = (1 + (k' + 1) * (Q - 1))"
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_Q prime_gt_1_nat semiring_normalization_rules(3))
have "[x * x ^ (k' * (Q - 1)) = x] (mod Q)" using asm by simp
hence "[x ^ (k' * (Q - 1)) * x ^ Q = x] (mod Q)" using flt_xQ
by (metis cong_scalar_right cong_trans mult.commute)
hence "[x ^ (k' * (Q - 1) + Q) = x] (mod Q)"
by (simp add: power_add)
hence "[x ^ (1 + (k' + 1) * (Q - 1)) = x] (mod Q)"
using exp_rewrite by argo
thus ?thesis by simp
qed
qed
have yk_y': "[y^(1 + k'*(Q-1)) = y] (mod Q)"
proof(induct k')
case 0
then show ?case by simp
next
case (Suc k')
assume  asm: "[y ^ (1 + k' * (Q - 1)) = y] (mod Q)"
then show ?case
proof-
have exp_rewrite: "(k' * (Q - 1) + Q) = (1 + (k' + 1) * (Q - 1))"
by (smt add.assoc add.commute le_add_diff_inverse nat_le_linear not_add_less1 prime_Q prime_gt_1_nat semiring_normalization_rules(3))
have "[y * y ^ (k' * (Q - 1)) = y] (mod Q)" using asm by simp
hence "[y ^ (k' * (Q - 1)) * y ^ Q = y] (mod Q)" using flt_yQ
by (metis cong_scalar_right cong_trans mult.commute)
hence "[y ^ (k' * (Q - 1) + Q) = y] (mod Q)"
by (simp add: power_add)
hence "[y ^ (1 + (k' + 1) * (Q - 1)) = y] (mod Q)"
using exp_rewrite by argo
thus ?thesis by simp
qed
qed
have Q_dvd_xy: "Q dvd (x - y)"
proof-
have "[x = y] (mod Q)"
using xk_x' yk_y' xk_yk' by (simp add: cong_def)
thus ?thesis
using cong_altdef_nat cong_sym False by simp
qed
show ?thesis
proof-
have "P*Q dvd (x - y)"
using P_dvd_xy Q_dvd_xy by (simp add: assms divides_mult primes_coprime)
hence 1: "[x = y] (mod P*Q)"
using False cong_altdef_nat linear by blast
hence "x mod P*Q = y mod P*Q"
using cong_less_modulus_unique_nat x_lt_pq y_lt_pd by blast
thus ?thesis
using 1 cong_less_modulus_unique_nat x_lt_pq y_lt_pd by blast
qed
qed
qed

lemma rsa_bij_betw:
assumes "coprime e ((P - 1)*(Q - 1))"
and "prime P"
and "prime Q"
and "P โ  Q"
shows "bij_betw (F ((P * Q), e)) (range ((P * Q), e)) (range ((P * Q), e))"
proof-
have PQ_not_0: "prime P โถ prime Q โถ P * Q โ  0"
using assms by auto
have "inj_on (ฮปx. x ^ snd (P * Q, e) mod fst (P * Q, e)) {..<fst (P * Q, e)}"
apply(simp add: inj_on_def)
using rsa_bijection assms by blast
moreover have "(ฮปx. x ^ snd (P * Q, e) mod fst (P * Q, e))  {..<fst (P * Q, e)} = {..<fst (P * Q, e)}"
apply(simp add: assms(2) assms(3) prime_gt_0_nat PQ_not_0)
apply(rule endo_inj_surj; auto simp add: assms(2) assms(3) image_subsetI prime_gt_0_nat PQ_not_0 inj_on_def)
using rsa_bijection assms by blast
ultimately show ?thesis
unfolding bij_betw_def F_def range_def by blast
qed

lemma bij_betw1:
assumes "((N,e),d) โ set_spmf I"
shows "bij_betw (F ((N), e)) (range ((N), e)) (range ((N), e))"
proof-
obtain P Q where "N = P * Q" and "bij_betw (F ((P*Q), e)) (range ((P*Q), e)) (range ((P*Q), e))"
proof-
obtain P Q where "prime P" and "prime Q" and "N = P * Q" and "P โ  Q" and "coprime e ((P - 1)*(Q - 1))"
using set_spmf_I_N assms by blast
then show ?thesis
using rsa_bij_betw that by blast
qed
thus ?thesis by blast
qed

lemma
assumes "P dvd x"
shows "[x = 0] (mod P)"
using assms cong_def by force

lemma rsa_inv:
assumes d: "d = nat (fst (bezw e ((P-1)*(Q-1))) mod int ((P-1)*(Q-1)))"
and coprime: "coprime e ((P-1)*(Q-1))"
and prime_P: "prime (P::nat)"
and prime_Q: "prime Q"
and P_neq_Q: "P โ  Q"
and e_gt_1: "e > 1"
and d_gt_1: "d > 1"
shows "((((x) ^ e) mod (P*Q)) ^ d) mod (P*Q) = x mod (P*Q)"
proof(cases "x = 0 โจ x = 1")
case True
then show ?thesis
by (metis assms(6) assms(7) le_simps(1) nat_power_eq_Suc_0_iff neq0_conv not_one_le_zero numeral_nat(7) power_eq_0_iff power_mod)
next
case False
hence x_gt_1: "x > 1" by simp
define z where "z = (x ^ e) ^ d - x"
hence z_gt_0: "z > 0"
proof-
have "(x ^ e) ^ d - x = x ^ (e * d) - x"
by (simp add: power_mult)
also have "... > 0"
by (metis x_gt_1 e_gt_1 d_gt_1 le_neq_implies_less less_one linorder_not_less n_less_m_mult_n not_less_zero numeral_nat(7) power_increasing_iff power_one_right zero_less_diff)
ultimately  show ?thesis using z_def by argo
qed
hence "[z = 0] (mod P)"
proof(cases "[x = 0] (mod P)")
case True
then show ?thesis
proof -
have "0 โ  d * e"
by (metis (no_types) assms assms mult_is_0 not_one_less_zero)
then show ?thesis
by (metis (no_types) Groups.add_ac(2) True add_diff_inverse_nat cong_def cong_dvd_iff cong_mult_self_right dvd_0_right dvd_def dvd_trans mod_add_self2 more_arith_simps(5) nat_diff_split power_eq_if power_mult semiring_normalization_rules(7) z_def)
qed
next
case False
have "[e * d = 1] (mod ((P - 1) * (Q - 1)))"
by (metis d bezw_inverse coprime coprime_imp_gcd_eq_1 nat_int)
hence "[e * d = 1] (mod (P - 1))"
using assms cong_modulus_mult_nat by blast
then obtain k where k: "e*d = 1 + k*(P-1)"
using ex_k_mod assms by force
hence "x ^ (e * d) = x * ((x ^ (P - 1)) ^ k)"
by (metis power_add power_one_right mult.commute power_mult)
hence "[x ^ (e * d) = x * ((x ^ (P - 1)) ^ k)] (mod P)"
using cong_def by simp
moreover have "[x ^ (P - 1) = 1] (mod P)"
using prime_P fermat_theorem False
by (simp add: cong_0_iff)
moreover have "[x ^ (e * d) = x * ((1) ^ k)] (mod P)"
by (metis โนx ^ (e * d) = x * (x ^ (P - 1)) ^ kโบ calculation(2) cong_pow cong_scalar_left)
hence "[x ^ (e * d) = x] (mod P)" by simp
thus ?thesis using z_def z_gt_0
by (simp add: cong_diff_iff_cong_0_nat power_mult)
qed
moreover have "[z = 0] (mod Q)"
proof(cases "[x = 0] (mod Q)")
case True
then show ?thesis
proof -
have "0 โ  d * e"
by (metis (no_types) assms mult_is_0 not_one_less_zero)
then show ?thesis
by (metis (no_types) Groups.add_ac(2) True add_diff_inverse_nat cong_def cong_dvd_iff cong_mult_self_right dvd_0_right dvd_def dvd_trans mod_add_self2 more_arith_simps(5) nat_diff_split power_eq_if power_mult semiring_normalization_rules(7) z_def)
qed
next
case False
have "[e * d = 1] (mod ((P - 1) * (Q - 1)))"
by (metis d bezw_inverse coprime coprime_imp_gcd_eq_1 nat_int)
hence "[e * d = 1] (mod (Q - 1))"
using assms cong_modulus_mult_nat mult.commute by metis
then obtain k where k: "e*d = 1 + k*(Q-1)"
using ex_k_mod assms by force
hence "x ^ (e * d) = x * ((x ^ (Q - 1)) ^ k)"
by (metis power_add power_one_right mult.commute power_mult)
hence "[x ^ (e * d) = x * ((x ^ (Q - 1)) ^ k)] (mod P)"
using cong_def by simp
moreover have "[x ^ (Q - 1) = 1] (mod Q)"
using prime_Q fermat_theorem False
by (simp add: cong_0_iff)
moreover have "[x ^ (e * d) = x * ((1) ^ k)] (mod Q)"
by (metis โนx ^ (e * d) = x * (x ^ (Q - 1)) ^ kโบ calculation(2) cong_pow cong_scalar_left)
hence "[x ^ (e * d) = x] (mod Q)" by simp
thus ?thesis using z_def z_gt_0
by (simp add: cong_diff_iff_cong_0_nat power_mult)
qed
ultimately have "Q dvd (x ^ e) ^ d - x"
"P dvd (x ^ e) ^ d - x"
using z_def assms cong_0_iff by blast +
hence "P * Q dvd ((x ^ e) ^ d - x)"
using assms divides_mult primes_coprime_nat by blast
hence "[(x ^ e) ^ d = x] (mod (P * Q))"
using z_gt_0 cong_altdef_nat z_def by auto
thus ?thesis
by (simp add: cong_def power_mod)
qed

lemma rsa_inv_set_spmf_I:
assumes "((N, e), d) โ set_spmf I"
shows "((((x::nat) ^ e) mod N) ^ d) mod N = x mod N"
proof-
obtain P Q where "N = P * Q" and "d = nat (fst (bezw e ((P-1)*(Q-1))) mod int ((P-1)*(Q-1)))"
and "prime P"
and "prime Q"
and "coprime e ((P - 1)*(Q - 1))"
and "P โ  Q"
using assms set_spmf_I_N
by blast
moreover have "e > 1" and "d > 1" using set_spmf_I_e_d assms by auto
ultimately show ?thesis using rsa_inv by blast
qed

sublocale etp_rsa: etp I domain range F Fโฉiโฉnโฉv
unfolding etp_def apply(auto simp add: etp_def dom_eq_ran finite_range bij_betw1 lossless_I)
apply (metis fst_conv lessThan_iff mem_simps(2) nat_0_less_mult_iff prime_gt_0_nat range_def set_spmf_I_N)
apply(auto simp add: F_def Fโฉiโฉnโฉv_def) using rsa_inv_set_spmf_I
by (simp add: range_def)

sublocale etp: ETP_base I domain range B F Fโฉiโฉnโฉv
unfolding ETP_base_def
by (simp add: etp_rsa.etp_axioms)

textโนAfter proving the RSA collection is an ETP the proofs of security come easily from the general proofs.โบ

lemma correctness_rsa: "etp.OT_12.correctness m1 m2"
by (rule local.etp.correct)

lemma P1_security_rsa: "etp.OT_12.perfect_sec_P1 m1 m2"
by(rule local.etp.P1_security_inf_the)

lemma P2_security_rsa:
assumes "โ a. lossless_spmf (D a)"
and "โbโฉฯ. local.etp_rsa.HCP_adv etp.๐ m2 bโฉฯ D โค HCP_ad"
shows "etp.OT_12.adv_P2 m1 m2 D โค 2 * HCP_ad"
by(simp add: local.etp.P2_security assms)

end

locale rsa_asym =
fixes prime_set :: "nat โ nat set"
and B :: "index โ nat โ bool"
assumes rsa_proof_assm: "โ n. rsa_base (prime_set n)"
begin

sublocale rsa_base "(prime_set n)" B
using local.rsa_proof_assm  by simp

lemma correctness_rsa_asymp:
shows "etp.OT_12.correctness n m1 m2"
by(rule correctness_rsa)

lemma P1_sec_asymp: "etp.OT_12.perfect_sec_P1 n m1 m2"
by(rule local.P1_security_rsa)

lemma P2_sec_asym:
assumes "โ a. lossless_spmf (D a)"
and HCP_adv_neg: "negligible (ฮป n. hcp_advantage n)"
and hcp_adv_bound:  "โbโฉฯ n. local.etp_rsa.HCP_adv n etp.๐ m2 bโฉฯ D โค hcp_advantage n"
shows "negligible (ฮป n. etp.OT_12.adv_P2 n m1 m2 D)"
proof-
have "negligible (ฮป n. 2 * hcp_advantage n)" using HCP_adv_neg
by (simp add: negligible_cmultI)
moreover have "ยฆetp.OT_12.adv_P2 n m1 m2 Dยฆ = etp.OT_12.adv_P2 n m1 m2 D"
for n unfolding sim_det_def.adv_P2_def local.etp.OT_12.adv_P2_def by linarith
moreover have "etp.OT_12.adv_P2 n m1 m2 D โค 2 * hcp_advantage n" for n
using P2_security_rsa assms by blast
ultimately show ?thesis
using assms negligible_le by presburger
qed

end

end

# Theory Noar_Pinkas_OT

subsection โนNoar Pinkas OTโบ

textโนHere we prove security for the Noar Pinkas OT from \cite{DBLP:conf/soda/NaorP01}.โบ

theory Noar_Pinkas_OT imports
Cyclic_Group_Ext
Game_Based_Crypto.Diffie_Hellman
OT_Functionalities
Semi_Honest_Def
Uniform_Sampling
begin

locale np_base =
fixes ๐ข :: "'grp cyclic_group" (structure)
assumes finite_group: "finite (carrier ๐ข)"
and or_gt_0: "0 < order ๐ข"
and prime_order: "prime (order ๐ข)"
begin

lemma prime_field: "a < (order ๐ข) โน a โ  0 โน coprime a (order ๐ข)"
by(metis dvd_imp_le neq0_conv not_le prime_imp_coprime prime_order coprime_commute)

lemma weight_sample_uniform_units: "weight_spmf (sample_uniform_units (order ๐ข)) = 1"
using  lossless_spmf_def lossless_sample_uniform_units prime_order  prime_gt_1_nat by auto

definition protocol :: "('grp ร 'grp) โ bool โ (unit ร 'grp) spmf"
where "protocol M v = do {
let (m0,m1) = M;
a :: nat โ sample_uniform (order ๐ข);
b :: nat โ sample_uniform (order ๐ข);
let cโฉv = (a*b) mod (order ๐ข);
cโฉv' :: nat โ sample_uniform (order ๐ข);
r0 :: nat โ sample_uniform_units (order ๐ข);
s0 :: nat โ sample_uniform_units (order ๐ข);
let w0 = (โg [^] a) [^] s0 โ โg [^] r0;
let z0' = ((โg [^] (if v then cโฉv' else cโฉv)) [^] s0) โ ((โg [^] b) [^] r0);
r1 :: nat โ sample_uniform_units (order ๐ข);
s1 :: nat โ sample_uniform_units (order ๐ข);
let w1 = (โg [^] a) [^] s1 โ โg [^] r1;
let z1' = ((โg [^] ((if v then cโฉv else cโฉv'))) [^] s1) โ ((โg [^] b) [^] r1);
let enc_m0 = z0' โ m0;
let enc_m1 = z1' โ m1;
let out_2 = (if v then enc_m1 โ inv (w1 [^] b) else enc_m0 โ inv (w0 [^] b));
return_spmf ((), out_2)}"

lemma lossless_protocol: "lossless_spmf (protocol M ฯ)"
apply(auto simp add: protocol_def Let_def split_def lossless_sample_uniform_units or_gt_0)
using prime_order prime_gt_1_nat lossless_sample_uniform_units by simp

type_synonym 'grp' view1 = "(('grp' ร 'grp') ร ('grp' ร 'grp' ร 'grp' ร 'grp')) spmf"

type_synonym 'grp' dist_adversary = "(('grp' ร 'grp') ร 'grp' ร 'grp' ร 'grp' ร 'grp') โ bool spmf"

definition R1 :: "('grp ร 'grp) โ bool โ 'grp view1"
where "R1 msgs ฯ = do {
let (m0, m1) = msgs;
a โ sample_uniform (order ๐ข);
b โ sample_uniform (order ๐ข);
let cโฉฯ = a*b;
cโฉฯ' โ sample_uniform (order ๐ข);
return_spmf (msgs, (โg [^] a, โg [^] b, (if ฯ then โg [^] cโฉฯ' else โg [^] cโฉฯ), (if ฯ then โg [^] cโฉฯ else โg [^] cโฉฯ')))}"

lemma lossless_R1: "lossless_spmf (R1 M ฯ)"
by(simp add: R1_def Let_def lossless_sample_uniform_units or_gt_0)

definition inter :: "('grp ร 'grp) โ 'grp view1"
where "inter msgs = do {
a โ sample_uniform (order ๐ข);
b โ sample_uniform (order ๐ข);
c โ sample_uniform (order ๐ข);
d โ sample_uniform (order ๐ข);
return_spmf (msgs, โg [^] a, โg [^] b, โg [^] c, โg [^] d)}"

definition S1 :: "('grp ร 'grp) โ unit โ 'grp view1"
where "S1 msgs out1 = do {
let (m0, m1) = msgs;
a โ sample_uniform (order ๐ข);
b โ sample_uniform (order ๐ข);
c โ sample_uniform (order ๐ข);
return_spmf (msgs, (โg [^] a, โg [^] b, โg [^] c, โg [^] (a*b)))}"

lemma lossless_S1: "lossless_spmf (S1 M out1)"
by(simp add: S1_def Let_def lossless_sample_uniform_units or_gt_0)

fun R1_inter_adversary :: "'grp dist_adversary โ ('grp ร 'grp) โ 'grp โ 'grp โ 'grp โ bool spmf"
where "R1_inter_adversary ๐ msgs ฮฑ ฮฒ ฮณ = do {
c โ sample_uniform (order ๐ข);
๐ (msgs, ฮฑ, ฮฒ, ฮณ, โg [^] c)}"

fun inter_S1_adversary :: "'grp dist_adversary โ ('grp ร 'grp) โ 'grp โ 'grp โ 'grp โ bool spmf"
where "inter_S1_adversary ๐ msgs ฮฑ ฮฒ ฮณ = do {
c โ sample_uniform (order ๐ข);
๐ (msgs, ฮฑ, ฮฒ, โg [^] c, ฮณ)}"

sublocale ddh: ddh ๐ข .

definition R2 :: "('grp ร 'grp) โ bool โ (bool ร 'grp ร 'grp ร  'grp ร 'grp ร 'grp ร 'grp ร 'grp) spmf"
where "R2 M v  = do {
let (m0,m1) = M;
a :: nat โ sample_uniform (order ๐ข);
b :: nat โ sample_uniform (order ๐ข);
let cโฉv = (a*b) mod (order ๐ข);
cโฉv' :: nat โ sample_uniform (order ๐ข);
r0 :: nat โ sample_uniform_units (order ๐ข);
s0 :: nat โ sample_uniform_units (order ๐ข);
let w0 = (โg [^] a) [^] s0 โ โg [^] r0;
let z = ((โg [^] cโฉv') [^] s0) โ ((โg [^] b) [^] r0);
r1 :: nat โ sample_uniform_units (order ๐ข);
s1 :: nat โ sample_uniform_units (order ๐ข);
let w1 = (โg [^] a) [^] s1 โ โg [^] r1;
let z' = ((โg [^] (cโฉv)) [^] s1) โ ((โg [^] b) [^] r1);
let enc_m = z โ (if v then m0 else m1);
let enc_m' = z' โ (if v then m1 else m0) ;
return_spmf(v, โg [^] a, โg [^] b, โg [^] cโฉv, w0, enc_m, w1, enc_m')}"

lemma lossless_R2: "lossless_spmf (R2 M ฯ)"
apply(simp add: R2_def Let_def split_def lossless_sample_uniform_units or_gt_0)
using prime_order prime_gt_1_nat lossless_sample_uniform_units by simp

definition S2 :: "bool โ 'grp โ (bool ร 'grp ร 'grp ร 'grp ร 'grp ร 'grp ร 'grp ร 'grp) spmf"
where "S2 v m =  do {
a :: nat โ sample_uniform (order ๐ข);
b :: nat โ sample_uniform (order ๐ข);
let cโฉv = (a*b) mod (order ๐ข);
r0 :: nat โ sample_uniform_units (order ๐ข);
s0 :: nat โ sample_uniform_units (order ๐ข);
let w0 = (โg [^] a) [^] s0 โ โg [^] r0;
r1 :: nat โ sample_uniform_units (order ๐ข);
s1 :: nat โ sample_uniform_units (order ๐ข);
let w1 = (โg [^] a) [^] s1 โ โg [^] r1;
let z' = ((โg [^] (cโฉv)) [^] s1) โ ((โg [^] b) [^] r1);
s' โ sample_uniform (order ๐ข);
let enc_m =  โg [^] s';
let enc_m' = z' โ m ;
return_spmf(v, โg [^] a, โg [^] b, โg [^] cโฉv, w0, enc_m, w1, enc_m')}"

lemma lossless_S2: "lossless_spmf (S2 ฯ out2)"
apply(simp add: S2_def Let_def lossless_sample_uniform_units or_gt_0)
using prime_order prime_gt_1_nat lossless_sample_uniform_units by simp

sublocale sim_def: sim_det_def R1 S1 R2 S2 funct_OT_12 protocol
unfolding sim_det_def_def
by(auto simp add: lossless_R1 lossless_S1 lossless_R2 lossless_S2 lossless_protocol lossless_funct_OT_12)

end

locale np = np_base + cyclic_group ๐ข
begin

lemma protocol_inverse:
assumes "m0 โ carrier ๐ข" "m1 โ carrier ๐ข"
shows" ((โg [^] ((a*b) mod (order ๐ข))) [^] (s1 :: nat)) โ ((โg [^] b) [^] (r1::nat)) โ (if v then m0 else m1) โ inv (((โg [^] a) [^] s1 โ โg [^] r1) [^] b)
= (if v then m0 else m1)"
(is "?lhs = ?rhs")
proof-
have  1: "(a*b)*(s1) + b*r1 =((a::nat)*(s1) + r1)*b " using mult.commute mult.assoc  add_mult_distrib by auto
have "?lhs =
((โg [^] (a*b)) [^] s1) โ ((โg [^] b) [^] r1) โ (if v then m0 else m1) โ inv (((โg [^] a) [^] s1 โ โg [^] r1) [^] b)"
by(simp add: pow_generator_mod)
also have "... = (โg [^] ((a*b)*(s1))) โ ((โg [^] (b*r1))) โ ((if v then m0 else m1) โ inv (((โg [^] ((a*(s1) + r1)*b)))))"
by(auto simp add: nat_pow_pow nat_pow_mult assms cyclic_group_assoc)
also have "... = โg [^] ((a*b)*(s1)) โ โg [^] (b*r1) โ ((inv (((โg [^] ((a*(s1) + r1)*b))))) โ (if v then m0 else m1))"
by(simp add: nat_pow_mult cyclic_group_commute assms)
also have "... = (โg [^] ((a*b)*(s1) + b*r1) โ inv (((โg [^] ((a*(s1) + r1)*b))))) โ (if v then m0 else m1)"
by(simp add: nat_pow_mult cyclic_group_assoc assms)
also have "... = (โg [^] ((a*b)*(s1) + b*r1) โ inv (((โg [^] (((a*b)*(s1) + r1*b)))))) โ (if v then m0 else m1)"
using 1 by (simp add: mult.commute)
ultimately show ?thesis
using l_cancel_inv assms  by (simp add: mult.commute)
qed

lemma correctness:
assumes "m0 โ carrier ๐ข" "m1 โ carrier ๐ข"
shows "sim_def.correctness (m0,m1) ฯ"
proof-
have "protocol (m0, m1) ฯ = funct_OT_12 (m0, m1) ฯ"
proof-
have "protocol (m0, m1) ฯ = do {
a :: nat โ sample_uniform (order ๐ข);
b :: nat โ sample_uniform (order ๐ข);
r1 :: nat โ sample_uniform_units (order ๐ข);
s1 :: nat โ sample_uniform_units (order ๐ข);
let out_2 = ((โg [^] ((a*b) mod (order ๐ข))) [^] s1) โ ((โg [^] b) [^] r1) โ (if ฯ then m1 else m0) โ inv (((โg [^] a) [^] s1 โ โg [^] r1) [^] b);
return_spmf ((), out_2)}"
by(simp add: protocol_def lossless_sample_uniform_units bind_spmf_const weight_sample_uniform_units or_gt_0)
also have "... = do {
let out_2 = (if ฯ then m1 else m0);
return_spmf ((), out_2)}"
by(simp add: protocol_inverse assms lossless_sample_uniform_units bind_spmf_const weight_sample_uniform_units or_gt_0)
ultimately show ?thesis by(simp add: Let_def funct_OT_12_def)
qed
thus ?thesis
by(simp add: sim_def.correctness_def)
qed

lemma security_P1:
shows "sim_def.adv_P1 msgs ฯ D โค ddh.advantage (R1_inter_adversary D msgs) + ddh.advantage (inter_S1_adversary D msgs)"
(is "?lhs โค ?rhs")
proof(cases ฯ)
case True
have "R1 msgs ฯ = S1 msgs out1" for out1
by(simp add: R1_def S1_def True)
then have "sim_def.adv_P1 msgs ฯ D = 0"
by(simp add: sim_def.adv_P1_def funct_OT_12_def)
also have "ddh.advantage A โฅ 0" for A using ddh.advantage_def by simp
ultimately show ?thesis by simp
next
case False
have bounded_advantage: "ยฆ(a :: real) - bยฆ = e1 โน ยฆb - cยฆ = e2 โน ยฆa - cยฆ โค e1 + e2"
for a b e1 c e2 by simp
also have R1_inter_dist: "ยฆspmf (R1 msgs False โค D) True - spmf ((inter msgs) โค D) Trueยฆ = ddh.advantage (R1_inter_adversary D msgs)"
unfolding R1_def inter_def ddh.advantage_def ddh.ddh_0_def ddh.ddh_1_def Let_def split_def by(simp)
also  have inter_S1_dist: "ยฆspmf ((inter msgs) โค D) True - spmf (S1 msgs out1 โค D) Trueยฆ = ddh.advantage (inter_S1_adversary D msgs)"
for out1 including monad_normalisation
by(simp add: S1_def inter_def ddh.advantage_def ddh.ddh_0_def ddh.ddh_1_def)
ultimately have "ยฆspmf (R1 msgs False โค (ฮปview. D view)) True - spmf (S1 msgs out1 โค (ฮปview. D view)) Trueยฆ โค ?rhs"
for out1 using R1_inter_dist by auto
thus ?thesis by(simp add: sim_def.adv_P1_def funct_OT_12_def False)
qed

lemma add_mult_one_time_pad:
assumes "s0 < order ๐ข"
and "s0 โ  0"
shows "map_spmf (ฮป cโฉv'. (((b* r0) + (s0 * cโฉv')) mod(order ๐ข))) (sample_uniform (order ๐ข)) = sample_uniform (order ๐ข)"
proof-
have "gcd s0 (order ๐ข) = 1"
using assms prime_field by simp
thus ?thesis
using add_mult_one_time_pad by force
qed

lemma security_P2:
assumes "m0 โ carrier ๐ข" "m1 โ carrier ๐ข"
shows "sim_def.perfect_sec_P2 (m0,m1) ฯ"
proof-
have "R2 (m0, m1) ฯ = S2 ฯ (if ฯ then m1 else m0)"
including monad_normalisation
proof-
have "R2 (m0, m1) ฯ = do {
a :: nat โ sample_uniform (order ๐ข);
b :: nat โ sample_uniform (order ๐ข);
let cโฉv = (a*b) mod (order ๐ข);
cโฉv' :: nat โ sample_uniform (order ๐ข);
r0 :: nat โ sample_uniform_units (order ๐ข);
s0 :: nat โ sample_uniform_units (order ๐ข);
let w0 = (โg [^] a) [^] s0 โ โg [^] r0;
let s' = (((b* r0) + ((cโฉv')*(s0))) mod(order ๐ข));
let z = โg [^] s' ;
r1 :: nat โ sample_uniform_units (order ๐ข);
s1 :: nat โ sample_uniform_units (order ๐ข);
let w1 = (โg [^] a) [^] s1 โ โg [^] r1;
let z' = ((โg [^] (cโฉv)) [^] s1) โ ((โg [^] b) [^] r1);
let enc_m = z โ (if ฯ then m0 else m1);
let enc_m' = z' โ (if ฯ then m1 else m0) ;
return_spmf(ฯ, โg [^] a, โg [^] b, โg [^] cโฉv, w0, enc_m, w1, enc_m')}"
by(simp add: R2_def nat_pow_pow nat_pow_mult pow_generator_mod add.commute)
also have "... =  do {
a :: nat โ sample_uniform (order ๐ข);
b :: nat โ sample_uniform (order ๐ข);
let cโฉv = (a*b) mod (order ๐ข);
r0 :: nat โ sample_uniform_units (order ๐ข);
s0 :: nat โ sample_uniform_units (order ๐ข);
let w0 = (โg [^] a) [^] s0 โ โg [^] r0;
s' โ map_spmf (ฮป cโฉv'. (((b* r0) + ((cโฉv')*(s0))) mod(order ๐ข))) (sample_uniform (order ๐ข));
let z = โg [^] s';
r1 :: nat โ sample_uniform_units (order ๐ข);
s1 :: nat โ sample_uniform_units (order ๐ข);
let w1 = (โg [^] a) [^] s1 โ โg [^] r1;
let z' = ((โg [^] (cโฉv)) [^] s1) โ ((โg [^] b) [^] r1);
let enc_m = z โ (if ฯ then m0 else m1);
let enc_m' = z' โ (if ฯ then m1 else m0) ;
return_spmf(ฯ, โg [^] a, โg [^] b, โg [^] cโฉv, w0, enc_m, w1, enc_m')}"
by(simp add: bind_map_spmf o_def Let_def)
also have "... =  do {
a :: nat โ sample_uniform (order ๐ข);
b :: nat โ sample_uniform (order ๐ข);
let cโฉv = (a*b) mod (order ๐ข);
r0 :: nat โ sample_uniform_units (order ๐ข);
s0 :: nat โ sample_uniform_units (order ๐ข);
let w0 = (โg [^] a) [^] s0 โ โg [^] r0;
s' โ  (sample_uniform (order ๐ข));
let z = โg [^] s';
r1 :: nat โ sample_uniform_units (order ๐ข);
s1 :: nat โ sample_uniform_units (order ๐ข);
let w1 = (โg [^] a) [^] s1 โ โg [^] r1;
let z' = ((โg [^] (cโฉv)) [^] s1) โ ((โg [^] b) [^] r1);
let enc_m = z โ (if ฯ then m0 else m1);
let enc_m' = z' โ (if ฯ then m1 else m0) ;
return_spmf(ฯ, โg [^] a, โg [^] b, โg [^] cโฉv, w0, enc_m, w1, enc_m')}"
by(simp add: add_mult_one_time_pad Let_def mult.commute cong: bind_spmf_cong_simp)
also have "... =  do {
a :: nat โ sample_uniform (order ๐ข);
b :: nat โ sample_uniform (order ๐ข);
let cโฉv = (a*b) mod (order ๐ข);
r0 :: nat โ sample_uniform_units (order ๐ข);
s0 :: nat โ sample_uniform_units (order ๐ข);
let w0 = (โg [^] a) [^] s0 โ โg [^] r0;
r1 :: nat โ sample_uniform_units (order ๐ข);
s1 :: nat โ sample_uniform_units (order ๐ข);
let w1 = (โg [^] a) [^] s1 โ โg [^] r1;
let z' = ((โg [^] (cโฉv)) [^] s1) โ ((โg [^] b) [^] r1);
enc_m โ map_spmf (ฮป s'.  โg [^] s' โ (if ฯ then m0 else m1)) (sample_uniform (order ๐ข));
let enc_m' = z' โ (if ฯ then m1 else m0) ;
return_spmf(ฯ, โg [^] a, โg [^] b, โg [^] cโฉv, w0, enc_m, w1, enc_m')}"
by(simp add: bind_map_spmf o_def Let_def)
also have "... =  do {
a :: nat โ sample_uniform (order ๐ข);
b :: nat โ sample_uniform (order ๐ข);
let cโฉv = (a*b) mod (order ๐ข);
r0 :: nat โ sample_uniform_units (order ๐ข);
s0 :: nat โ sample_uniform_units (order ๐ข);
let w0 = (โg [^] a) [^] s0 โ โg [^] r0;
r1 :: nat โ sample_uniform_units (order ๐ข);
s1 :: nat โ sample_uniform_units (order ๐ข);
let w1 = (โg [^] a) [^] s1 โ โg [^] r1;
let z' = ((โg [^] (cโฉv)) [^] s1) โ ((โg [^] b) [^] r1);
enc_m โ map_spmf (ฮป s'.  โg [^] s') (sample_uniform (order ๐ข));
let enc_m' = z' โ (if ฯ then m1 else m0) ;
return_spmf(ฯ, โg [^] a, โg [^] b, โg [^] cโฉv, w0, enc_m, w1, enc_m')}"
by(simp add: sample_uniform_one_time_pad assms)
ultimately show ?thesis by(simp add: S2_def Let_def bind_map_spmf o_def)
qed
thus ?thesis
by(simp add: sim_def.perfect_sec_P2_def funct_OT_12_def)
qed

end

locale np_asymp =
fixes ๐ข :: "security โ 'grp cyclic_group"
assumes np: "โฮท. np (๐ข ฮท)"
begin

sublocale np "๐ข ฮท" for ฮท by(simp add: np)

theorem correctness_asymp:
assumes "m0 โ carrier (๐ข ฮท)" "m1 โ carrier (๐ข ฮท)"
shows "sim_def.correctness ฮท (m0, m1) ฯ"
by(simp add: correctness assms)

theorem security_P1_asymp:
assumes "negligible (ฮป ฮท. ddh.advantage ฮท (inter_S1_adversary ฮท D msgs))"
and "negligible (ฮป ฮท. ddh.advantage ฮท (R1_inter_adversary ฮท  D msgs))"
shows "negligible (ฮป ฮท. sim_def.adv_P1 ฮท msgs ฯ D)"
proof-
have "sim_def.adv_P1 ฮท msgs ฯ D โค ddh.advantage ฮท (R1_inter_adversary ฮท  D msgs) + ddh.advantage ฮท (inter_S1_adversary ฮท D msgs)"
for ฮท
using security_P1 by simp
moreover have "negligible (ฮป ฮท. ddh.advantage ฮท (R1_inter_adversary ฮท  D msgs) + ddh.advantage ฮท (inter_S1_adversary ฮท D msgs))"
using assms
by (simp add: negligible_plus)
ultimately show ?thesis
using negligible_le sim_def.adv_P1_def by auto
qed

theorem security_P2_asymp:
assumes "m0 โ carrier (๐ข ฮท)" "m1 โ carrier (๐ข ฮท)"
shows "sim_def.perfect_sec_P2 ฮท (m0,m1) ฯ"
by(simp add: security_P2 assms)

end

end

# Theory OT14

subsection โน1-out-of-2 OT to 1-out-of-4 OTโบ

text โนHere we construct a protocol that achieves 1-out-of-4 OT from 1-out-of-2 OT. We follow the protocol
for constructing 1-out-of-n OT from 1-out-of-2 OT from \cite{DBLP:books/cu/Goldreich2004}. We assume the security
properties on 1-out-of-2 OT.โบ

theory OT14 imports
Semi_Honest_Def
OT_Functionalities
Uniform_Sampling
begin

type_synonym input1 = "bool ร bool ร bool ร bool"
type_synonym input2 = "bool ร bool"
type_synonym 'v_OT121' view1 = "(input1 ร (bool ร bool ร bool ร bool ร bool ร bool) ร 'v_OT121' ร 'v_OT121' ร 'v_OT121')"
type_synonym 'v_OT122' view2 = "(input2 ร (bool ร bool ร bool ร bool) ร 'v_OT122' ร 'v_OT122' ร 'v_OT122')"

locale ot14_base =
fixes S1_OT12 :: "(bool ร bool) โ unit โ 'v_OT121 spmf" โ โนsimulator for party 1 in OT12โบ
and R1_OT12 :: "(bool ร bool) โ bool โ 'v_OT121 spmf" โ โนreal view for party 1 in OT12โบ
and adv_OT12 :: real
and S2_OT12 :: "bool โ bool โ 'v_OT122 spmf"
and R2_OT12 :: "(bool ร bool) โ bool โ 'v_OT122 spmf"
and protocol_OT12 :: "(bool ร bool) โ bool โ (unit ร bool) spmf"
assumes ass_adv_OT12: "sim_det_def.adv_P1 R1_OT12 S1_OT12 funct_OT12 (m0,m1) c D โค adv_OT12" โ โนbound the advantage of OT12 for party 1โบ
and inf_th_OT12_P2:  "sim_det_def.perfect_sec_P2 R2_OT12 S2_OT12 funct_OT12 (m0,m1) ฯ" โ โนinformation theoretic security for party 2โบ
and correct: "protocol_OT12 msgs b = funct_OT_12 msgs b"
and lossless_R1_12: "lossless_spmf (R1_OT12 m c)"
and lossless_S1_12: "lossless_spmf (S1_OT12 m out1)"
and lossless_S2_12: "lossless_spmf (S2_OT12 c out2)"
and lossless_R2_12: "lossless_spmf (R2_OT12 M c)"
and lossless_funct_OT12: "lossless_spmf (funct_OT12 (m0,m1) c)"
and lossless_protocol_OT12: "lossless_spmf (protocol_OT12 M C)"
begin

sublocale OT_12_sim: sim_det_def R1_OT12 S1_OT12 R2_OT12 S2_OT12 funct_OT_12 protocol_OT12
unfolding sim_det_def_def
by(simp add: lossless_R1_12 lossless_S1_12 lossless_funct_OT12 lossless_R2_12 lossless_S2_12)

lemma OT_12_P1_assms_bound': "ยฆspmf (bind_spmf (R1_OT12 (m0,m1) c) (ฮป view. ((D::'v_OT121 โ bool spmf) view ))) True
- spmf (bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (D view ))) Trueยฆ โค adv_OT12"
proof-
have "sim_det_def.adv_P1 R1_OT12 S1_OT12 funct_OT_12 (m0,m1) c D =
ยฆspmf (bind_spmf (R1_OT12 (m0,m1) c) (ฮป view. (D view ))) True
- spmf (funct_OT_12 (m0,m1) c โค (ฮป ((out1::unit), (out2::bool)).
S1_OT12 (m0,m1) out1 โค (ฮป view. D view))) Trueยฆ"
using sim_det_def.adv_P1_def
using  OT_12_sim.adv_P1_def by auto
also have "... = ยฆspmf (bind_spmf (R1_OT12 (m0,m1) c) (ฮป view. ((D::'v_OT121 โ bool spmf) view ))) True
- spmf (bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (D view ))) Trueยฆ"
by(simp add: funct_OT_12_def)
ultimately show ?thesis
by(metis ass_adv_OT12)
qed

lemma OT_12_P2_assm: "R2_OT12 (m0,m1) ฯ = funct_OT_12 (m0,m1) ฯ โค (ฮป (out1, out2). S2_OT12 ฯ out2)"
using inf_th_OT12_P2 OT_12_sim.perfect_sec_P2_def by blast

definition protocol_14_OT :: "input1 โ input2 โ (unit ร bool) spmf"
where "protocol_14_OT M C = do {
let (c0,c1) = C;
let (m00, m01, m10, m11) = M;
S0 โ coin_spmf;
S1 โ coin_spmf;
S2 โ coin_spmf;
S3 โ coin_spmf;
S4 โ coin_spmf;
S5 โ coin_spmf;
let a0 = S0 โ S2 โ m00;
let a1 = S0 โ S3 โ m01;
let a2 = S1 โ S4 โ m10;
let a3 = S1 โ S5 โ m11;
(_,Si) โ protocol_OT12 (S0, S1) c0;
(_,Sj) โ protocol_OT12 (S2, S3) c1;
(_,Sk) โ protocol_OT12 (S4, S5) c1;
let s2 = Si โ (if c0 then Sk else Sj) โ (if c0 then (if c1 then a3 else a2) else (if c1 then a1 else a0));
return_spmf ((), s2)}"

lemma lossless_protocol_14_OT: "lossless_spmf (protocol_14_OT M C)"
by(simp add: protocol_14_OT_def lossless_protocol_OT12 split_def)

definition R1_14 :: "input1 โ input2 โ 'v_OT121 view1 spmf"
where "R1_14 msgs choice = do {
let (m00, m01, m10, m11) = msgs;
let (c0, c1) = choice;
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a :: 'v_OT121 โ R1_OT12 (S0, S1) c0;
b :: 'v_OT121 โ R1_OT12 (S2, S3) c1;
c :: 'v_OT121 โ R1_OT12 (S4, S5) c1;
return_spmf (msgs, (S0, S1, S2, S3, S4, S5), a, b, c)}"

lemma lossless_R1_14: "lossless_spmf (R1_14 msgs C)"
by(simp add: R1_14_def split_def lossless_R1_12)

definition R1_14_interm1 :: "input1 โ input2 โ 'v_OT121 view1 spmf"
where "R1_14_interm1 msgs choice = do {
let (m00, m01, m10, m11) = msgs;
let (c0, c1) = choice;
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a :: 'v_OT121 โ S1_OT12 (S0, S1) ();
b :: 'v_OT121 โ R1_OT12 (S2, S3) c1;
c :: 'v_OT121 โ R1_OT12 (S4, S5) c1;
return_spmf (msgs, (S0, S1, S2, S3, S4, S5), a, b, c)}"

lemma lossless_R1_14_interm1: "lossless_spmf (R1_14_interm1 msgs C)"
by(simp add: R1_14_interm1_def split_def lossless_R1_12 lossless_S1_12)

definition R1_14_interm2 :: "input1 โ input2 โ 'v_OT121 view1 spmf"
where "R1_14_interm2 msgs choice = do {
let (m00, m01, m10, m11) = msgs;
let (c0, c1) = choice;
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a :: 'v_OT121 โ S1_OT12 (S0, S1) ();
b :: 'v_OT121 โ S1_OT12 (S2, S3) ();
c :: 'v_OT121 โ R1_OT12 (S4, S5) c1;
return_spmf (msgs, (S0, S1, S2, S3, S4, S5), a, b, c)}"

lemma lossless_R1_14_interm2: "lossless_spmf (R1_14_interm2 msgs C)"
by(simp add: R1_14_interm2_def split_def lossless_R1_12 lossless_S1_12)

definition S1_14 :: "input1 โ unit โ 'v_OT121 view1 spmf"
where "S1_14 msgs _ = do {
let (m00, m01, m10, m11) = msgs;
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a :: 'v_OT121 โ S1_OT12 (S0, S1) ();
b :: 'v_OT121 โ S1_OT12 (S2, S3) ();
c :: 'v_OT121 โ S1_OT12 (S4, S5) ();
return_spmf (msgs, (S0, S1, S2, S3, S4, S5), a, b, c)}"

lemma lossless_S1_14: "lossless_spmf (S1_14 m out)"
by(simp add: S1_14_def lossless_S1_12)

lemma reduction_step1:
shows "โ A1. ยฆspmf (bind_spmf (R1_14 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm1 M (c0, c1)) D) Trueยฆ =
ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c0) (ฮป view. (A1 view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A1 view (m0,m1))))) Trueยฆ"
including monad_normalisation
proof-
define A1' where "A1' == ฮป (view :: 'v_OT121) (m0,m1). do {
S2 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
b :: 'v_OT121 โ R1_OT12 (S2, S3) c1;
c :: 'v_OT121 โ R1_OT12 (S4, S5) c1;
let R = (M, (m0,m1, S2, S3, S4, S5), view, b, c);
D R}"
have "ยฆspmf (bind_spmf (R1_14 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm1 M (c0, c1)) D) Trueยฆ =
ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c0) (ฮป view. (A1' view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A1' view (m0,m1))))) Trueยฆ"
apply(simp add: pair_spmf_alt_def R1_14_def R1_14_interm1_def A1'_def Let_def split_def)
apply(subst bind_commute_spmf[of "S1_OT12 _ _"])
apply(subst bind_commute_spmf[of "S1_OT12 _ _"])
apply(subst bind_commute_spmf[of "S1_OT12 _ _"])
apply(subst bind_commute_spmf[of "S1_OT12 _ _"])
apply(subst bind_commute_spmf[of "S1_OT12 _ _"])
by auto
then show ?thesis by auto
qed

lemma reduction_step1':
shows "ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c0) (ฮป view. (A1 view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A1 view (m0,m1))))) Trueยฆ
โค adv_OT12"
(is "?lhs โค adv_OT12")
proof-
have int1: "integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) (ฮปx. spmf (case x of (m0, m1) โ R1_OT12 (m0, m1) c0 โค (ฮปview. A1 view (m0, m1))) True)"
and int2: "integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) (ฮปx. spmf (case x of (m0, m1) โ S1_OT12 (m0, m1) () โค (ฮปview. A1 view (m0, m1))) True)"
by(rule measure_spmf.integrable_const_bound[where B=1]; simp add: pmf_le_1)+
have "?lhs =
ยฆLINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) โ R1_OT12 (m0, m1) c0 โค (ฮปview. A1 view (m0, m1))) True
- spmf (case x of (m0, m1) โ S1_OT12 (m0, m1) () โค (ฮปview. A1 view (m0, m1))) Trueยฆ"
apply(subst (1 2) spmf_bind) using int1 int2 by simp
also have "... โค LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf).
ยฆspmf (R1_OT12 x c0 โค (ฮปview. A1 view x)) True - spmf (S1_OT12 x () โค (ฮปview. A1 view x)) Trueยฆ"
by(rule integral_abs_bound[THEN order_trans]; simp add: split_beta)
ultimately have "?lhs โค LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf).
ยฆspmf (R1_OT12 x c0 โค (ฮปview. A1 view x)) True - spmf (S1_OT12 x () โค (ฮปview. A1 view x)) Trueยฆ"
by simp
also have "LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf).
ยฆspmf (R1_OT12 x c0 โค (ฮปview::'v_OT121. A1 view x)) True
- spmf (S1_OT12 x () โค (ฮปview::'v_OT121. A1 view x)) Trueยฆ โค adv_OT12"
apply(rule integral_mono[THEN order_trans])
apply(rule measure_spmf.integrable_const_bound[where B=2])
apply clarsimp
apply(rule abs_triangle_ineq4[THEN order_trans])
subgoal for m0 m1
using pmf_le_1[of "R1_OT12 (m0, m1) c0 โค (ฮปview. A1 view (m0, m1))" "Some True"]
pmf_le_1[of "S1_OT12 (m0, m1) () โค (ฮปview. A1 view (m0, m1))" "Some True"]
by simp
apply simp
apply(rule measure_spmf.integrable_const)
apply clarify
apply(rule OT_12_P1_assms_bound'[rule_format])
by simp
ultimately show ?thesis by simp
qed

lemma reduction_step2:
shows "โ A1. ยฆspmf (bind_spmf (R1_14_interm1 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm2 M (c0, c1)) D) Trueยฆ =
ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (ฮป view. (A1 view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A1 view (m0,m1))))) Trueยฆ"
proof-
define A1' where "A1' == ฮป (view :: 'v_OT121) (m0,m1). do {
S2 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a :: 'v_OT121 โ S1_OT12 (S2,S3) ();
c :: 'v_OT121 โ R1_OT12 (S4, S5) c1;
let R = (M, (S2,S3, m0, m1, S4, S5), a, view, c);
D R}"
have "ยฆspmf (bind_spmf (R1_14_interm1 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm2 M (c0, c1)) D) Trueยฆ =
ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (ฮป view. (A1' view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A1' view (m0,m1))))) Trueยฆ"
proof-
have "(bind_spmf (R1_14_interm1 M (c0, c1)) D) = (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (ฮป view. (A1' view (m0,m1)))))"
unfolding R1_14_interm1_def R1_14_interm2_def A1'_def Let_def split_def
apply(simp add: pair_spmf_alt_def)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ"  in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
including monad_normalisation by(simp)
also have "(bind_spmf (R1_14_interm2 M (c0, c1)) D) =  (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A1' view (m0,m1)))))"
unfolding R1_14_interm1_def R1_14_interm2_def A1'_def Let_def split_def
apply(simp add: pair_spmf_alt_def)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ"  in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ"  in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ"  in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ"  in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ"  in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ"  in "_ = โ" bind_commute_spmf)
by(simp)
ultimately show ?thesis by simp
qed
then show ?thesis by auto
qed

lemma reduction_step3:
shows "โ A1. ยฆspmf (bind_spmf (R1_14_interm2 M (c0, c1)) D) True - spmf (bind_spmf (S1_14 M out) D) Trueยฆ =
ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (ฮป view. (A1 view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A1 view (m0,m1))))) Trueยฆ"
proof-
define A1' where "A1' == ฮป (view :: 'v_OT121) (m0,m1). do {
S2 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a :: 'v_OT121 โ S1_OT12 (S2,S3) ();
b :: 'v_OT121 โ S1_OT12 (S4, S5) ();
let R = (M, (S2,S3, S4, S5,m0, m1), a, b, view);
D R}"
have "ยฆspmf (bind_spmf (R1_14_interm2 M (c0, c1)) D) True - spmf (bind_spmf (S1_14 M out) D) Trueยฆ =
ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (ฮป view. (A1' view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A1' view (m0,m1))))) Trueยฆ"
proof-
have "(bind_spmf (R1_14_interm2 M (c0, c1)) D) = (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (ฮป view. (A1' view (m0,m1)))))"
unfolding  R1_14_interm2_def A1'_def Let_def split_def
apply(simp add: pair_spmf_alt_def)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ"  in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ"  in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ"  in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
including monad_normalisation by(simp)
also have "(bind_spmf (S1_14 M out) D) = (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A1' view (m0,m1)))))"
unfolding S1_14_def Let_def A1'_def split_def
apply(simp add: pair_spmf_alt_def)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ"  in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ"  in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ"  in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "โ = _" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "โ = _" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "โ = _" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "โ = _" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "โ = _" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "โ = _" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "โ = _" bind_commute_spmf)
including monad_normalisation by(simp)
ultimately show ?thesis by simp
qed
then show ?thesis by auto
qed

lemma reduction_P1_interm:
shows "ยฆspmf (bind_spmf (R1_14 M (c0,c1)) (D)) True - spmf (bind_spmf (S1_14 M out) (D)) Trueยฆ โค 3 * adv_OT12"
(is "?lhs โค ?rhs")
proof-
have lhs: "?lhs โค ยฆspmf (bind_spmf (R1_14 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm1 M (c0, c1)) D) Trueยฆ +
ยฆspmf (bind_spmf (R1_14_interm1 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm2 M (c0, c1)) D) Trueยฆ +
ยฆspmf (bind_spmf (R1_14_interm2 M (c0, c1)) D) True - spmf (bind_spmf (S1_14 M out) D) Trueยฆ"
by simp
obtain A1 where A1: "ยฆspmf (bind_spmf (R1_14 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm1 M (c0, c1)) D) Trueยฆ =
ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c0) (ฮป view. (A1 view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A1 view (m0,m1))))) Trueยฆ"
using reduction_step1 by blast
obtain A2 where A2: "ยฆspmf (bind_spmf (R1_14_interm1 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm2 M (c0, c1)) D) Trueยฆ =
ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (ฮป view. (A2 view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A2 view (m0,m1))))) Trueยฆ"
using reduction_step2 by blast
obtain A3 where A3: "ยฆspmf (bind_spmf (R1_14_interm2 M (c0, c1)) D) True - spmf (bind_spmf (S1_14 M out) D) Trueยฆ =
ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (ฮป view. (A3 view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A3 view (m0,m1))))) Trueยฆ"
using reduction_step3 by blast
have lhs_bound: "?lhs โค ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c0) (ฮป view. (A1 view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A1 view (m0,m1))))) Trueยฆ +
ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (ฮป view. (A2 view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A2 view (m0,m1))))) Trueยฆ +
ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (ฮป view. (A3 view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A3 view (m0,m1))))) Trueยฆ"
using A1 A2 A3 lhs by simp
have bound1: "ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c0) (ฮป view. (A1 view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A1 view (m0,m1))))) Trueยฆ
โค adv_OT12"
and bound2: "ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (ฮป view. (A2 view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A2 view (m0,m1))))) Trueยฆ
โค adv_OT12"
and bound3: "ยฆspmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (ฮป view. (A3 view (m0,m1))))) True -
spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (ฮป(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (ฮป view. (A3 view (m0,m1))))) Trueยฆ โค adv_OT12"
using reduction_step1' by auto
thus ?thesis
using reduction_step1' lhs_bound by argo
qed

lemma reduction_P1: "ยฆspmf (bind_spmf (R1_14 M (c0,c1)) (D)) True
- spmf (funct_OT_14 M (c0,c1) โค (ฮป (out1,out2). S1_14 M out1 โค (ฮป view. D view))) Trueยฆ
โค 3 * adv_OT12"
by(simp add: funct_OT_14_def split_def Let_def reduction_P1_interm )

textโนParty 2 security.โบ

lemma coin_coin: "map_spmf (ฮป S0. S0 โ S3 โ m1) coin_spmf = coin_spmf"
(is "?lhs = ?rhs")
proof-
have lhs: "?lhs = map_spmf (ฮป S0. S0 โ (S3 โ m1)) coin_spmf" by blast
also have op_eq: "... = map_spmf ((โ) (S3 โ m1)) coin_spmf"
by (metis xor_bool_def)
also have "... = ?rhs"
using xor_uni_samp by fastforce
ultimately show ?thesis
using op_eq by auto
qed

lemma coin_coin': "map_spmf (ฮป S3. S0 โ S3 โ m1) coin_spmf = coin_spmf"
proof-
have "map_spmf (ฮป S3. S0 โ S3 โ m1) coin_spmf = map_spmf (ฮป S3. S3 โ S0 โ m1) coin_spmf"
by (metis xor_left_commute)
thus ?thesis using coin_coin by simp
qed

definition R2_14:: "input1 โ input2 โ 'v_OT122 view2 spmf"
where "R2_14 M C = do {
let (m0,m1,m2,m3) = M;
let (c0,c1) = C;
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
let a0 = S0 โ S2 โ m0;
let a1 = S0 โ S3 โ m1;
let a2 = S1 โ S4 โ m2;
let a3 = S1 โ S5 โ m3;
a :: 'v_OT122 โ R2_OT12 (S0,S1) c0;
b :: 'v_OT122 โ R2_OT12 (S2,S3) c1;
c :: 'v_OT122 โ R2_OT12 (S4,S5) c1;
return_spmf (C, (a0,a1,a2,a3), a,b,c)}"

lemma lossless_R2_14: "lossless_spmf (R2_14 M C)"
by(simp add: R2_14_def split_def lossless_R2_12)

definition S2_14 :: "input2 โ bool โ 'v_OT122 view2 spmf"
where "S2_14 C out = do {
let ((c0::bool),(c1::bool)) = C;
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a0 :: bool โ coin_spmf;
a1 :: bool โ coin_spmf;
a2 :: bool โ coin_spmf;
a3 :: bool โ coin_spmf;
let a0' = (if ((ยฌ c0) โง (ยฌ c1)) then (S0 โ S2 โ out) else a0);
let a1' = (if ((ยฌ c0) โง c1) then (S0 โ S3 โ out) else a1);
let a2' = (if (c0 โง (ยฌ c1)) then (S1 โ S4 โ out) else a2);
let a3' = (if (c0 โง c1) then (S1 โ S5 โ out) else a3);
a :: 'v_OT122 โ S2_OT12 (c0::bool) (if c0 then S1 else S0);
b :: 'v_OT122 โ S2_OT12 (c1::bool) (if c1 then S3 else S2);
c :: 'v_OT122 โ S2_OT12 (c1::bool) (if c1 then S5 else S4);
return_spmf ((c0,c1), (a0',a1',a2',a3'), a,b,c)}"

lemma lossless_S2_14: "lossless_spmf (S2_14 c out)"
by(simp add: S2_14_def lossless_S2_12 split_def)

lemma P2_OT_14_FT: "R2_14 (m0,m1,m2,m3) (False,True) = funct_OT_14 (m0,m1,m2,m3) (False,True) โค (ฮป (out1, out2). S2_14 (False,True) out2)"
including monad_normalisation
proof-
have "R2_14 (m0,m1,m2,m3) (False,True) =  do {
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a0 :: bool โ map_spmf (ฮป S2. S0 โ S2 โ m0) coin_spmf;
let a1 = S0 โ S3 โ m1;
a2 โ map_spmf (ฮป S4. S1 โ S4 โ m2) coin_spmf;
let a3 = S1 โ S5 โ m3;
a :: 'v_OT122 โ S2_OT12 False S0;
b :: 'v_OT122 โ S2_OT12 True S3;
c :: 'v_OT122 โ S2_OT12 True S5;
return_spmf ((False,True), (a0,a1,a2,a3), a,b,c)}"
by(simp add: bind_map_spmf o_def Let_def R2_14_def inf_th_OT12_P2 funct_OT_12_def OT_12_P2_assm)
also have "... =  do {
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a0 :: bool โ coin_spmf;
let a1 = S0 โ S3 โ m1;
a2 โ coin_spmf;
let a3 = S1 โ S5 โ m3;
a :: 'v_OT122 โ S2_OT12 False S0;
b :: 'v_OT122 โ S2_OT12 True S3;
c :: 'v_OT122 โ S2_OT12 True S5;
return_spmf ((False,True), (a0,a1,a2,a3), a,b,c)}"
using coin_coin' by simp
also have "... =  do {
S0 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a0 :: bool โ coin_spmf;
let a1 = S0 โ S3 โ m1;
a2 :: bool โ coin_spmf;
a3 โ map_spmf (ฮป S1. S1 โ S5 โ m3) coin_spmf;
a :: 'v_OT122 โ S2_OT12 False S0;
b :: 'v_OT122 โ S2_OT12 True S3;
c :: 'v_OT122 โ S2_OT12 True S5;
return_spmf ((False,True), (a0,a1,a2,a3), a,b,c)}"
by(simp add: bind_map_spmf o_def Let_def)
also have "... =  do {
S0 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a0 :: bool โ coin_spmf;
let a1 = S0 โ S3 โ m1;
a2 :: bool โ coin_spmf;
a3 โ coin_spmf;
a :: 'v_OT122 โ S2_OT12 False S0;
b :: 'v_OT122 โ S2_OT12 True S3;
c :: 'v_OT122 โ S2_OT12 True S5;
return_spmf ((False,True), (a0,a1,a2,a3), a,b,c)}"
using coin_coin by simp
ultimately show ?thesis
by(simp add: funct_OT_14_def S2_14_def bind_spmf_const)
qed

lemma P2_OT_14_TT: "R2_14 (m0,m1,m2,m3) (True,True) = funct_OT_14 (m0,m1,m2,m3) (True,True) โค (ฮป (out1, out2). S2_14 (True,True) out2)"
including monad_normalisation
proof-
have "R2_14 (m0,m1,m2,m3) (True,True) =  do {
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a0 :: bool โ map_spmf (ฮป S2. S0 โ S2 โ m0) coin_spmf;
let a1 = S0 โ S3 โ m1;
a2 โ map_spmf (ฮป S4. S1 โ S4 โ m2) coin_spmf;
let a3 = S1 โ S5 โ m3;
a :: 'v_OT122 โ S2_OT12 True S1;
b :: 'v_OT122 โ S2_OT12 True S3;
c :: 'v_OT122 โ S2_OT12 True S5;
return_spmf ((True,True), (a0,a1,a2,a3), a,b,c)}"
by(simp add: bind_map_spmf o_def R2_14_def inf_th_OT12_P2 funct_OT_12_def OT_12_P2_assm Let_def)
also have "... = do {
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a0 :: bool โ coin_spmf;
let a1 = S0 โ S3 โ m1;
a2 โ coin_spmf;
let a3 = S1 โ S5 โ m3;
a :: 'v_OT122 โ S2_OT12 True S1;
b :: 'v_OT122 โ S2_OT12 True S3;
c :: 'v_OT122 โ S2_OT12 True S5;
return_spmf ((True,True), (a0,a1,a2,a3), a,b,c)}"
using coin_coin' by simp
also have "... = do {
S1 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a0 :: bool โ coin_spmf;
a1 :: bool โ map_spmf (ฮป S0. S0 โ S3 โ m1) coin_spmf;
a2 โ coin_spmf;
let a3 = S1 โ S5 โ m3;
a :: 'v_OT122 โ S2_OT12 True S1;
b :: 'v_OT122 โ S2_OT12 True S3;
c :: 'v_OT122 โ S2_OT12 True S5;
return_spmf ((True,True), (a0,a1,a2,a3), a,b,c)}"
by(simp add: bind_map_spmf o_def Let_def)
also have "... = do {
S1 :: bool โ coin_spmf;
S3 :: bool โ coin_spmf;
S5 :: bool โ coin_spmf;
a0 :: bool โ coin_spmf;
a1 :: bool โ coin_spmf;
a2 โ coin_spmf;
let a3 = S1 โ S5 โ m3;
a :: 'v_OT122 โ S2_OT12 True S1;
b :: 'v_OT122 โ S2_OT12 True S3;
c :: 'v_OT122 โ S2_OT12 True S5;
return_spmf ((True,True), (a0,a1,a2,a3), a,b,c)}"
using coin_coin by simp
ultimately show ?thesis
by(simp add: funct_OT_14_def S2_14_def bind_spmf_const)
qed

lemma P2_OT_14_FF: "R2_14 (m0,m1,m2,m3) (False, False) = funct_OT_14 (m0,m1,m2,m3) (False, False) โค (ฮป (out1, out2). S2_14 (False, False) out2)"
including monad_normalisation
proof-
have "R2_14 (m0,m1,m2,m3) (False,False) =  do {
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
let a0 = S0 โ S2 โ m0;
a1 :: bool โ map_spmf (ฮป S3. S0 โ S3 โ m1) coin_spmf;
let a2 = S1 โ S4 โ m2;
a3 โ map_spmf (ฮป S5. S1 โ S5 โ m3) coin_spmf;
a :: 'v_OT122 โ S2_OT12 False S0;
b :: 'v_OT122 โ S2_OT12 False S2;
c :: 'v_OT122 โ S2_OT12 False S4;
return_spmf ((False,False), (a0,a1,a2,a3), a,b,c)}"
by(simp add: bind_map_spmf o_def R2_14_def inf_th_OT12_P2 funct_OT_12_def OT_12_P2_assm Let_def)
also have "... = do {
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
let a0 = S0 โ S2 โ m0;
a1 :: bool โ coin_spmf;
let a2 = S1 โ S4 โ m2;
a3 โ coin_spmf;
a :: 'v_OT122 โ S2_OT12 False S0;
b :: 'v_OT122 โ S2_OT12 False S2;
c :: 'v_OT122 โ S2_OT12 False S4;
return_spmf ((False,False), (a0,a1,a2,a3), a,b,c)}"
using coin_coin' by simp
also have "... = do {
S0 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
let a0 = S0 โ S2 โ m0;
a1 :: bool โ coin_spmf;
a2 :: bool โ map_spmf (ฮป S1. S1 โ S4 โ m2) coin_spmf;
a3 โ coin_spmf;
a :: 'v_OT122 โ S2_OT12 False S0;
b :: 'v_OT122 โ S2_OT12 False S2;
c :: 'v_OT122 โ S2_OT12 False S4;
return_spmf ((False,False), (a0,a1,a2,a3), a,b,c)}"
by(simp add: bind_map_spmf o_def Let_def)
also have "... = do {
S0 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
let a0 = S0 โ S2 โ m0;
a1 :: bool โ coin_spmf;
a2 :: bool โ coin_spmf;
a3 โ coin_spmf;
a :: 'v_OT122 โ S2_OT12 False S0;
b :: 'v_OT122 โ S2_OT12 False S2;
c :: 'v_OT122 โ S2_OT12 False S4;
return_spmf ((False,False), (a0,a1,a2,a3), a,b,c)}"
using coin_coin by simp
ultimately show ?thesis
by(simp add: funct_OT_14_def S2_14_def bind_spmf_const)
qed

lemma P2_OT_14_TF: "R2_14 (m0,m1,m2,m3) (True,False) = funct_OT_14 (m0,m1,m2,m3) (True,False) โค (ฮป (out1, out2). S2_14 (True,False) out2)"
including monad_normalisation
proof-
have "R2_14 (m0,m1,m2,m3) (True,False) = do {
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
let a0 = S0 โ S2 โ m0;
a1 :: bool โ map_spmf (ฮป S3. S0 โ S3 โ m1) coin_spmf;
let a2 = S1 โ S4 โ m2;
a3 โ map_spmf (ฮป S5. S1 โ S5 โ m3) coin_spmf;
a :: 'v_OT122 โ S2_OT12 True S1;
b :: 'v_OT122 โ S2_OT12 False S2;
c :: 'v_OT122 โ S2_OT12 False S4;
return_spmf ((True,False), (a0,a1,a2,a3), a,b,c)}"
apply(simp add: R2_14_def inf_th_OT12_P2 OT_12_P2_assm funct_OT_12_def Let_def)
apply(rewrite in "bind_spmf _ โ" in "โ = _" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "โ = _" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ"  in "bind_spmf _ โ" in "โ = _" bind_commute_spmf)
by(simp add: bind_map_spmf o_def Let_def)
also have "... = do {
S0 :: bool โ coin_spmf;
S1 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
let a0 = S0 โ S2 โ m0;
a1 :: bool โ coin_spmf;
let a2 = S1 โ S4 โ m2;
a3 โ coin_spmf;
a :: 'v_OT122 โ S2_OT12 True S1;
b :: 'v_OT122 โ S2_OT12 False S2;
c :: 'v_OT122 โ S2_OT12 False S4;
return_spmf ((True,False), (a0,a1,a2,a3), a,b,c)}"
using coin_coin' by simp
also have "... = do {
S1 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
a0 :: bool โ map_spmf (ฮป S0. S0 โ S2 โ m0) coin_spmf;
a1 :: bool โ coin_spmf;
let a2 = S1 โ S4 โ m2;
a3 โ coin_spmf;
a :: 'v_OT122 โ S2_OT12 True S1;
b :: 'v_OT122 โ S2_OT12 False S2;
c :: 'v_OT122 โ S2_OT12 False S4;
return_spmf ((True,False), (a0,a1,a2,a3), a,b,c)}"
by(simp add: bind_map_spmf o_def Let_def)
also have "... = do {
S1 :: bool โ coin_spmf;
S2 :: bool โ coin_spmf;
S4 :: bool โ coin_spmf;
a0 :: bool โ coin_spmf;
a1 :: bool โ coin_spmf;
let a2 = S1 โ S4 โ m2;
a3 โ coin_spmf;
a :: 'v_OT122 โ S2_OT12 True S1;
b :: 'v_OT122 โ S2_OT12 False S2;
c :: 'v_OT122 โ S2_OT12 False S4;
return_spmf ((True,False), (a0,a1,a2,a3), a,b,c)}"
using coin_coin by simp
ultimately show ?thesis
apply(simp add: funct_OT_14_def S2_14_def bind_spmf_const)
apply(rewrite in "bind_spmf _ โ"  in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
apply(rewrite in "bind_spmf _ โ" in "bind_spmf _ โ" in "bind_spmf _ โ" in "_ = โ" bind_commute_spmf)
by simp
qed

lemma P2_sec_OT_14_split: "R2_14 (m0,m1,m2,m3) (c0,c1) = funct_OT_14 (m0,m1,m2,m3) (c0,c1) โค (ฮป (out1, out2). S2_14 (c0,c1) out2)"
by(cases c0; cases c1; auto simp add: P2_OT_14_FF P2_OT_14_TF P2_OT_14_FT P2_OT_14_TT)

lemma P2_sec_OT_14: "R2_14 M C = funct_OT_14 M C โค (ฮป (out1, out2). S2_14 C out2)"
by(metis P2_sec_OT_14_split surj_pair)

sublocale OT_14: sim_det_def R1_14 S1_14 R2_14 S2_14 funct_OT_14 protocol_14_OT
unfolding sim_det_def_def
by(simp add: lossless_R1_14 lossless_S1_14 lossless_funct_14_OT lossless_R2_14 lossless_S2_14 )

lemma correctness_OT_14:
shows "funct_OT_14 M C = protocol_14_OT M C"
proof-
have "S1 = (S5 = (S1 = (S5 = d))) = d" for S1 S5 d by auto
thus ?thesis
by(cases "fst C"; cases "snd C"; simp add: funct_OT_14_def protocol_14_OT_def correct funct_OT_12_def lossless_funct_OT_12 bind_spmf_const split_def)
qed

lemma OT_14_correct: "OT_14.correctness M C"
unfolding OT_14.correctness_def
using correctness_OT_14 by auto

lemma OT_14_P2_sec: "OT_14.perfect_sec_P2 m1 m2"
unfolding OT_14.perfect_sec_P2_def
using P2_sec_OT_14 by blast

lemma OT_14_P1_sec: "OT_14.adv_P1 m1 m2 D โค 3 * adv_OT12"
unfolding OT_14.adv_P1_def
by (metis reduction_P1 surj_pair)

end

locale OT_14_asymp = sim_det_def +
fixes S1_OT12 :: "nat โ (bool ร bool) โ unit โ 'v_OT121 spmf"
and R1_OT12 :: "nat โ (bool ร bool) โ bool โ 'v_OT121 spmf"
and adv_OT12 :: "nat โ real"
and S2_OT12 :: "nat โ bool โ bool โ 'v_OT122 spmf"
and R2_OT12 :: "nat โ (bool ร bool) โ bool โ 'v_OT122 spmf"
and protocol_OT12 :: "(bool ร bool) โ bool โ (unit ร bool) spmf"
assumes ot14_base: "โ (n::nat). ot14_base (S1_OT12 n) (R1_12_0T n) (adv_OT12 n) (S2_OT12 n) (R2_12OT n) (protocol_OT12)"
begin

sublocale ot14_base "(S1_OT12 n)" "(R1_12_0T n)" "(adv_OT12 n)" "(S2_OT12 n)" "(R2_12OT n)" using local.ot14_base by simp

lemma OT_14_P1_sec: "OT_14.adv_P1 (R1_12_0T n) n m1 m2 D โค 3 * (adv_OT12 n)"
unfolding OT_14.adv_P1_def using reduction_P1 surj_pair by metis

theorem OT_14_P1_asym_sec: "negligible (ฮป n. OT_14.adv_P1 (R1_12_0T n) n m1 m2 D)" if "negligible (ฮป n. adv_OT12 n)"
proof-
have adv_neg: "negligible (ฮปn. 3 * adv_OT12 n)" using that negligible_cmultI by simp
have "ยฆOT_14.adv_P1 (R1_12_0T n) n m1 m2 Dยฆ โค ยฆ3 * (adv_OT12 n)ยฆ" for n
proof -
have "ยฆOT_14.adv_P1 (R1_12_0T n) n m1 m2 Dยฆ โค 3 * adv_OT12 n"
using OT_14.adv_P1_def OT_14_P1_sec by auto
then show ?thesis
by (meson abs_ge_self order_trans)
qed
thus ?thesis using OT_14_P1_sec negligible_le adv_neg
by (metis (no_types, lifting) negligible_absI)
qed

theorem OT_14_P2_asym_sec: "OT_14.perfect_sec_P2 R2_OT12 n m1 m2"
using OT_14_P2_sec by simp

end

end



# Theory GMW

subsection โน1-out-of-4 OT to GMWโบ

textโนWe prove security for the gates of the GMW protocol in the semi honest model. We assume security on
1-out-of-4 OT.โบ

theory`