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 GMW imports
OT14
begin
type_synonym share_1 = bool
type_synonym share_2 = bool
type_synonym shares_1 = "bool list"
type_synonym shares_2 = "bool list"
type_synonym msgs_14_OT = "(bool × bool × bool × bool)"
type_synonym choice_14_OT = "(bool × bool)"
type_synonym share_wire = "(share_1 × share_2)"
locale gmw_base =
fixes S1_14_OT :: "msgs_14_OT ⇒ unit ⇒ 'v_14_OT1 spmf"
and R1_14_OT :: "msgs_14_OT ⇒ choice_14_OT ⇒ 'v_14_OT1 spmf"
and S2_14_OT :: "choice_14_OT ⇒ bool ⇒ 'v_14_OT2 spmf"
and R2_14_OT :: "msgs_14_OT ⇒ choice_14_OT ⇒ 'v_14_OT2 spmf"
and protocol_14_OT :: "msgs_14_OT ⇒ choice_14_OT ⇒ (unit × bool) spmf"
and adv_14_OT :: real
assumes P1_OT_14_adv_bound: "sim_det_def.adv_P1 R1_14_OT S1_14_OT funct_14_OT M C D ≤ adv_14_OT"
and P2_OT_12_inf_theoretic: "sim_det_def.perfect_sec_P2 R2_14_OT S2_14_OT funct_14_OT M C"
and correct_14: "funct_OT_14 msgs C = protocol_14_OT msgs C"
and lossless_R1_14_OT: "lossless_spmf (R1_14_OT (m1,m2,m3,m4) (c0,c1))"
and lossless_R2_14_OT: "lossless_spmf (R2_14_OT (m1,m2,m3,m4) (c0,c1))"
and lossless_S1_14_OT: "lossless_spmf (S1_14_OT (m1,m2,m3,m4) ())"
and lossless_S2_14_OT: "lossless_spmf (S2_14_OT (c0,c1) b)"
and lossless_protocol_14_OT: "lossless_spmf (protocol_14_OT S C)"
and lossless_funct_14_OT: "lossless_spmf (funct_14_OT M C)"
begin
lemma funct_14: "funct_OT_14 (m00,m01,m10,m11) (c0,c1)
= return_spmf ((),if c0 then (if c1 then m11 else m10) else (if c1 then m01 else m00))"
by(simp add: funct_OT_14_def)
sublocale OT_14_sim: sim_det_def R1_14_OT S1_14_OT R2_14_OT S2_14_OT funct_14_OT protocol_14_OT
unfolding sim_det_def_def
by(simp add: lossless_R1_14_OT lossless_S1_14_OT lossless_funct_14_OT lossless_R2_14_OT lossless_S2_14_OT)
lemma inf_th_14_OT_P4: "R2_14_OT msgs C = (funct_OT_14 msgs C ⤜ (λ (s1, s2). S2_14_OT C s2))"
using P2_OT_12_inf_theoretic sim_det_def.perfect_sec_P2_def OT_14_sim.perfect_sec_P2_def by auto
lemma ass_adv_14_OT: "¦spmf (bind_spmf (S1_14_OT msgs ()) (λ view. (D view))) True -
spmf (bind_spmf (R1_14_OT msgs (c0,c1)) (λ view. (D view))) True ¦ ≤ adv_14_OT"
(is "?lhs ≤ adv_14_OT")
proof-
have "funct_OT_14 (m0,m1,m2,m3) (c0, c1) ⤜ (λ(o1, o2). S1_14_OT (m0,m1,m2,m3) () ⤜ D) = S1_14_OT (m0,m1,m2,m3) () ⤜ D"
for m0 m1 m2 m3 by(simp add: funct_14)
hence funct: "funct_OT_14 msgs (c0, c1) ⤜ (λ(o1, o2). S1_14_OT msgs () ⤜ D) = S1_14_OT msgs () ⤜ D"
by (metis prod_cases4)
have "?lhs = ¦spmf (bind_spmf (R1_14_OT msgs (c0,c1)) (λ view. (D view))) True
- spmf (bind_spmf (S1_14_OT msgs ()) (λ view. (D view))) True¦"
by linarith
hence "... = ¦(spmf (R1_14_OT msgs (c0,c1) ⤜ (λ view. D view)) True)
- spmf (funct_OT_14 msgs (c0,c1) ⤜ (λ (o1, o2). S1_14_OT msgs o1 ⤜ (λ view. D view))) True¦"
by(simp add: funct)
thus ?thesis using P1_OT_14_adv_bound sim_det_def.adv_P1_def
by (simp add: OT_14_sim.adv_P1_def abs_minus_commute)
qed
text ‹The sharing scheme›
definition share :: "bool ⇒ share_wire spmf"
where "share x = do {
a⇩1 ← coin_spmf;
let b⇩1 = x ⊕ a⇩1;
return_spmf (a⇩1, b⇩1)}"
lemma lossless_share [simp]: "lossless_spmf (share x)"
by(simp add: share_def)
definition reconstruct :: "(share_1 × share_2) ⇒ bool spmf"
where "reconstruct shares = do {
let (a,b) = shares;
return_spmf (a ⊕ b)}"
lemma lossless_reconstruct [simp]: "lossless_spmf (reconstruct s)"
by(simp add: reconstruct_def split_def)
lemma reconstruct_share : "(bind_spmf (share x) reconstruct) = (return_spmf x)"
proof-
have "y = (y = x) = x" for y by auto
thus ?thesis
by(auto simp add: share_def reconstruct_def bind_spmf_const eq_commute)
qed
lemma "(reconstruct (s1,s2) ⤜ (λ rec. share rec ⤜ (λ shares. reconstruct shares))) = return_spmf (s1 ⊕ s2)"
apply(simp add: reconstruct_share reconstruct_def share_def)
apply(cases s1; cases s2) by(auto simp add: bind_spmf_const)
definition xor_evaluate :: "bool ⇒ bool ⇒ bool spmf"
where "xor_evaluate A B = return_spmf (A ⊕ B)"
definition xor_funct :: "share_wire ⇒ share_wire ⇒ (bool × bool) spmf"
where "xor_funct A B = do {
let (a1, b1) = A;
let (a2,b2) = B;
return_spmf (a1 ⊕ a2, b1 ⊕ b2)}"
lemma lossless_xor_funct: "lossless_spmf (xor_funct A B)"
by(simp add: xor_funct_def split_def)
definition xor_protocol :: "share_wire ⇒ share_wire ⇒ (bool × bool) spmf"
where "xor_protocol A B = do {
let (a1, b1) = A;
let (a2,b2) = B;
return_spmf (a1 ⊕ a2, b1 ⊕ b2)}"
lemma lossless_xor_protocol: "lossless_spmf (xor_protocol A B)"
by(simp add: xor_protocol_def split_def)
lemma share_xor_reconstruct:
shows "share x ⤜ (λ w1. share y ⤜ (λ w2. xor_protocol w1 w2
⤜ (λ (a, b). reconstruct (a, b)))) = xor_evaluate x y"
proof-
have "(ya = (¬ yb)) = ((x = (¬ ya)) = (y = (¬ yb))) = (x = (¬ y))" for ya yb
by auto
then show ?thesis
by(simp add: share_def xor_protocol_def reconstruct_def xor_evaluate_def bind_spmf_const)
qed
definition R1_xor :: "(bool × bool) ⇒ (bool × bool) ⇒ (bool × bool) spmf"
where "R1_xor A B = return_spmf A"
lemma lossless_R1_xor: "lossless_spmf (R1_xor A B)"
by(simp add: R1_xor_def)
definition S1_xor :: "(bool × bool) ⇒ bool ⇒ (bool × bool) spmf"
where "S1_xor A out = return_spmf A"
lemma lossless_S1_xor: "lossless_spmf (S1_xor A out)"
by(simp add: S1_xor_def)
lemma P1_xor_inf_th: "R1_xor A B = xor_funct A B ⤜ (λ (out1, out2). S1_xor A out1)"
by(simp add: R1_xor_def xor_funct_def S1_xor_def split_def)
definition R2_xor :: "(bool × bool) ⇒ (bool × bool) ⇒ (bool × bool) spmf"
where "R2_xor A B = return_spmf B"
lemma lossless_R2_xor: "lossless_spmf (R2_xor A B)"
by(simp add: R2_xor_def)
definition S2_xor :: "(bool × bool) ⇒ bool ⇒ (bool × bool) spmf"
where "S2_xor B out = return_spmf B"
lemma lossless_S2_xor: "lossless_spmf (S2_xor A out)"
by(simp add: S2_xor_def)
lemma P2_xor_inf_th: "R2_xor A B = xor_funct A B ⤜ (λ (out1, out2). S2_xor B out2)"
by(simp add: R2_xor_def xor_funct_def S2_xor_def split_def)
sublocale xor_sim_det: sim_det_def R1_xor S1_xor R2_xor S2_xor xor_funct xor_protocol
unfolding sim_det_def_def
by(simp add: lossless_R1_xor lossless_S1_xor lossless_R2_xor lossless_S2_xor lossless_xor_funct)
lemma "xor_sim_det.perfect_sec_P1 m1 m2"
by(simp add: xor_sim_det.perfect_sec_P1_def P1_xor_inf_th)
lemma "xor_sim_det.perfect_sec_P2 m1 m2"
by(simp add: xor_sim_det.perfect_sec_P2_def P2_xor_inf_th)
definition and_funct :: "(share_1 × share_2) ⇒ (share_1 × share_2) ⇒ share_wire spmf"
where "and_funct A B = do {
let (a1, a2) = A;
let (b1,b2) = B;
σ ← coin_spmf;
return_spmf (σ, σ ⊕ ((a1 ⊕ b1) ∧ (a2 ⊕ b2)))}"
lemma lossless_and_funct: "lossless_spmf (and_funct A B)"
by(simp add: and_funct_def split_def)
definition and_evaluate :: "bool ⇒ bool ⇒ bool spmf"
where "and_evaluate A B = return_spmf (A ∧ B)"
definition and_protocol :: "share_wire ⇒ share_wire ⇒ share_wire spmf"
where "and_protocol A B = do {
let (a1, b1) = A;
let (a2,b2) = B;
σ ← coin_spmf;
let s0 = σ ⊕ ((a1 ⊕ False) ∧ (b1 ⊕ False));
let s1 = σ ⊕ ((a1 ⊕ False) ∧ (b1 ⊕ True));
let s2 = σ ⊕ ((a1 ⊕ True) ∧ (b1 ⊕ False));
let s3 = σ ⊕ ((a1 ⊕ True) ∧ (b1 ⊕ True));
(_, s) ← protocol_14_OT (s0,s1,s2,s3) (a2,b2);
return_spmf (σ, s)}"
lemma lossless_and_protocol: "lossless_spmf (and_protocol A B)"
by(simp add: and_protocol_def split_def lossless_protocol_14_OT)
lemma and_correct: "and_protocol (a1, b1) (a2,b2) = and_funct (a1, b1) (a2,b2)"
apply(simp add: and_protocol_def and_funct_def correct_14[symmetric] funct_14)
by(cases b2 ; cases b1; cases a1; cases a2; auto)
lemma share_and_reconstruct:
shows "share x ⤜ (λ (a1,a2). share y ⤜ (λ (b1,b2).
and_protocol (a1,b1) (a2,b2) ⤜ (λ (a, b). reconstruct (a, b)))) = and_evaluate x y"
proof-
have "(yc = (¬ (if x = (¬ ya) then if snd (snd (ya, x = (¬ ya)), snd (yb, y = (¬ yb))) then yc
= (fst (fst (ya, x = (¬ ya)), fst (yb, y = (¬ yb))) ∨ snd (fst (ya, x = (¬ ya)), fst (yb, y = (¬ yb))))
else yc = (fst (fst (ya, x = (¬ ya)), fst (yb, y = (¬ yb))) ∨ ¬ snd (fst (ya, x = (¬ ya)), fst (yb, y = (¬ yb))))
else if snd (snd (ya, x = (¬ ya)), snd (yb, y = (¬ yb))) then yc = (fst (fst (ya, x = (¬ ya)), fst (yb, y = (¬ yb)))
⟶ snd (fst (ya, x = (¬ ya)), fst (yb, y = (¬ yb))))
else yc = (fst (fst (ya, x = (¬ ya)), fst (yb, y = (¬ yb)))
⟶ ¬ snd (fst (ya, x = (¬ ya)), fst (yb, y = (¬ yb))))))) = (x ∧ y)"
for yc yb ya by auto
then show ?thesis
by(auto simp add: share_def reconstruct_def and_protocol_def and_evaluate_def split_def correct_14[symmetric] funct_14 bind_spmf_const Let_def)
qed
definition and_R1 :: "(share_1 × share_1) ⇒ (share_2 × share_2) ⇒ (((share_1 × share_1) × bool × 'v_14_OT1) × (share_1 × share_2)) spmf"
where "and_R1 A B = do {
let (a1, a2) = A;
let (b1,b2) = B;
σ ← coin_spmf;
let s0 = σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ False));
let s1 = σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ True));
let s2 = σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ False));
let s3 = σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ True));
V ← R1_14_OT (s0,s1,s2,s3) (b1,b2);
(_, s) ← protocol_14_OT (s0,s1,s2,s3) (b1,b2);
return_spmf (((a1,a2), σ, V), (σ, s))}"
lemma lossless_and_R1: "lossless_spmf (and_R1 A B)"
apply(simp add: and_R1_def split_def lossless_R1_14_OT lossless_protocol_14_OT Let_def)
by (metis prod.collapse lossless_R1_14_OT)
definition S1_and :: "(share_1 × share_1) ⇒ bool ⇒ (((bool × bool) × bool × 'v_14_OT1)) spmf"
where "S1_and A σ = do {
let (a1,a2) = A;
let s0 = σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ False));
let s1 = σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ True));
let s2 = σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ False));
let s3 = σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ True));
V ← S1_14_OT (s0,s1,s2,s3) ();
return_spmf ((a1,a2), σ, V)}"
definition out1 :: "(share_1 × share_1) ⇒ (share_2 × share_2) ⇒ bool ⇒ (share_1 × share_2) spmf"
where "out1 A B σ = do {
let (a1,a2) = A;
let (b1,b2) = B;
return_spmf (σ, σ ⊕ ((a1 ⊕ b1) ∧ (a2 ⊕ b2)))}"
definition S1_and' :: "(share_1 × share_1) ⇒ (share_2 × share_2) ⇒ bool ⇒ (((bool × bool) × bool × 'v_14_OT1) × (share_1 × share_2)) spmf"
where "S1_and' A B σ = do {
let (a1,a2) = A;
let (b1,b2) = B;
let s0 = σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ False));
let s1 = σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ True));
let s2 = σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ False));
let s3 = σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ True));
V ← S1_14_OT (s0,s1,s2,s3) ();
return_spmf (((a1,a2), σ, V), (σ, σ ⊕ ((a1 ⊕ b1) ∧ (a2 ⊕ b2))))}"
lemma sec_ex_P1_and:
shows "∃ (A :: 'v_14_OT1 ⇒ bool ⇒ bool spmf).
¦spmf ((and_funct (a1, a2) (b1,b2)) ⤜ (λ (s1, s2). (S1_and' (a1,a2) (b1,b2) s1)
⤜ (D :: (((bool × bool) × bool × 'v_14_OT1) × (share_1 × share_2)) ⇒ bool spmf))) True - spmf ((and_R1 (a1, a2) (b1,b2)) ⤜ D) True¦ =
¦spmf (coin_spmf ⤜ (λ σ. S1_14_OT ((σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ True))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ True)))) ()
⤜ (λ view. A view σ))) True
- spmf (coin_spmf ⤜ (λ σ. R1_14_OT ((σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ True))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ True)))) (b1, b2)
⤜ (λ view. A view σ))) True¦"
including monad_normalisation
proof-
define A' where "A' == λ view σ. (D (((a1,a2), σ, view), (σ, σ ⊕ ((a1 ⊕ b1) ∧ (a2 ⊕ b2)))))"
have "¦spmf ((and_funct (a1, a2) (b1,b2)) ⤜ (λ (s1, s2). (S1_and' (a1,a2) (b1,b2) s1)
⤜ (D :: (((bool × bool) × bool × 'v_14_OT1) × (share_1 × share_2)) ⇒ bool spmf))) True -
spmf ((and_R1 (a1, a2) (b1,b2)) ⤜ (D :: (((bool × bool) × bool × 'v_14_OT1) × (bool × bool)) ⇒ bool spmf)) True¦ =
¦spmf (coin_spmf ⤜ (λ σ :: bool. S1_14_OT ((σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ True))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ True)))) ()
⤜ (λ view. A' view σ))) True - spmf (coin_spmf ⤜ (λ σ. R1_14_OT ((σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ True))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ True)))) (b1, b2)
⤜ (λ view. A' view σ))) True¦"
by(auto simp add: S1_and'_def A'_def and_funct_def and_R1_def Let_def split_def correct_14[symmetric] funct_14; cases a1; cases a2; cases b1; cases b2; auto)
then show ?thesis by auto
qed
lemma bound_14_OT:
"¦spmf (coin_spmf ⤜ (λ σ. S1_14_OT ((σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ True))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ True)))) ()
⤜ (λ view. (A :: 'v_14_OT1 ⇒ bool ⇒ bool spmf) view σ))) True - spmf (coin_spmf ⤜ (λ σ. R1_14_OT ((σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ True))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ True)))) (b1, b2)
⤜ (λ view. A view σ))) True¦ ≤ adv_14_OT"
(is "?lhs ≤ adv_14_OT")
proof-
have int1: "integrable (measure_spmf coin_spmf) (λx. spmf (S1_14_OT (x ⊕ (a1 ⊕ False ∧ a2 ⊕ False), x ⊕ (a1 ⊕ False ∧ a2 ⊕ True), x ⊕ (a1 ⊕ True ∧ a2 ⊕ False), x ⊕ (a1 ⊕ True ∧ a2 ⊕ True)) () ⤜ (λview. A view x)) True)"
and int2: "integrable (measure_spmf coin_spmf) (λx. spmf (R1_14_OT (x ⊕ (a1 ⊕ False ∧ a2 ⊕ False), x ⊕ (a1 ⊕ False ∧ a2 ⊕ True), x ⊕ (a1 ⊕ True ∧ a2 ⊕ False), x ⊕ (a1 ⊕ True ∧ a2 ⊕ True)) (b1, b2) ⤜ (λview. A view x)) True)"
by(rule measure_spmf.integrable_const_bound[where B=1]; simp add: pmf_le_1)+
have "?lhs = ¦LINT x|measure_spmf coin_spmf.
spmf (S1_14_OT (x ⊕ (a1 ⊕ False ∧ a2 ⊕ False), x ⊕ (a1 ⊕ False ∧ a2 ⊕ True), x ⊕ (a1 ⊕ True ∧ a2 ⊕ False), x ⊕ (a1 ⊕ True ∧ a2 ⊕ True)) () ⤜ (λview. A view x)) True -
spmf (R1_14_OT (x ⊕ (a1 ⊕ False ∧ a2 ⊕ False), x ⊕ (a1 ⊕ False ∧ a2 ⊕ True), x ⊕ (a1 ⊕ True ∧ a2 ⊕ False), x ⊕ (a1 ⊕ True ∧ a2 ⊕ True)) (b1, b2) ⤜ (λview. A view x)) True¦"
apply(subst (1 2) spmf_bind) using int1 int2 by simp
also have "... ≤ LINT x|measure_spmf coin_spmf. ¦spmf (S1_14_OT (x = (a1 ⟶ ¬ a2), x = (a1 ⟶ a2), x = (a1 ∨ ¬ a2), x = (a1 ∨ a2)) () ⤜ (λview. A view x)) True
- spmf (R1_14_OT (x = (a1 ⟶ ¬ a2), x = (a1 ⟶ a2), x = (a1 ∨ ¬ a2), x = (a1 ∨ a2)) (b1, b2) ⤜ (λview. A view x)) True¦"
by(rule integral_abs_bound[THEN order_trans]; simp add: split_beta)
ultimately have "?lhs ≤ LINT x|measure_spmf coin_spmf. ¦spmf (S1_14_OT (x = (a1 ⟶ ¬ a2), x = (a1 ⟶ a2), x = (a1 ∨ ¬ a2), x = (a1 ∨ a2)) () ⤜ (λview. A view x)) True
- spmf (R1_14_OT (x = (a1 ⟶ ¬ a2), x = (a1 ⟶ a2), x = (a1 ∨ ¬ a2), x = (a1 ∨ a2)) (b1, b2) ⤜ (λview. A view x)) True¦"
by simp
also have "LINT x|measure_spmf coin_spmf. ¦spmf (S1_14_OT (x = (a1 ⟶ ¬ a2), x = (a1 ⟶ a2), x = (a1 ∨ ¬ a2), x = (a1 ∨ a2)) () ⤜ (λview. A view x)) True
- spmf (R1_14_OT (x = (a1 ⟶ ¬ a2), x = (a1 ⟶ a2), x = (a1 ∨ ¬ a2), x = (a1 ∨ a2)) (b1, b2) ⤜ (λview. A view x)) True¦ ≤ adv_14_OT"
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])
apply(cases a1) apply(cases a2)
subgoal for M
using pmf_le_1[of "R1_14_OT (¬ M, M, M, M) (b1,b2) ⤜ (λ view. A view M)" "Some True"]
pmf_le_1[of "S1_14_OT (¬ M, M, M, M) () ⤜ (λ view. A view M)" "Some True"]
by simp
subgoal for M
using pmf_le_1[of "R1_14_OT (M, ¬ M, M, M) (b1,b2) ⤜ (λ view. A view M)" "Some True"]
pmf_le_1[of "S1_14_OT (M, ¬ M, M, M) () ⤜ (λ view. A view M)" "Some True"]
by simp
apply(cases a2) apply(auto)
subgoal for M
using pmf_le_1[of "R1_14_OT (M, M, ¬ M, M) (b1,b2) ⤜ (λ view. A view M)" "Some True"]
pmf_le_1[of "S1_14_OT (M, M, ¬ M, M) () ⤜ (λ view. A view M)" "Some True"]
by(simp)
subgoal for M
using pmf_le_1[of "R1_14_OT (M, M, M, ¬ M) (b1,b2) ⤜ (λ view. A view M)" "Some True"]
pmf_le_1[of "S1_14_OT (M, M, M, ¬ M) () ⤜ (λ view. A view M)" "Some True"]
by(simp)
using ass_adv_14_OT by fast
ultimately show ?thesis by simp
qed
lemma security_and_P1:
shows "¦spmf ((and_funct (a1, a2) (b1,b2)) ⤜ (λ (s1, s2). (S1_and' (a1,a2) (b1,b2) s1)
⤜ (D :: (((bool × bool) × bool × 'v_14_OT1) × (share_1 × share_2)) ⇒ bool spmf))) True -
spmf ((and_R1 (a1, a2) (b1,b2)) ⤜ D) True¦ ≤ adv_14_OT"
proof-
obtain A :: "'v_14_OT1 ⇒ bool ⇒ bool spmf" where A:
"¦spmf ((and_funct (a1, a2) (b1,b2)) ⤜ (λ (s1, s2). (S1_and' (a1,a2) (b1,b2) s1) ⤜ D)) True - spmf ((and_R1 (a1, a2) (b1,b2)) ⤜ D) True¦ =
¦spmf (coin_spmf ⤜ (λ σ. S1_14_OT ((σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ True))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ True)))) ()
⤜ (λ view. A view σ))) True - spmf (coin_spmf
⤜ (λ σ. R1_14_OT ((σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ True))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ False))), (σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ True)))) (b1, b2)
⤜ (λ view. A view σ))) True¦"
using sec_ex_P1_and by blast
then show ?thesis using bound_14_OT[of "a1" "a2" "A" "b1" "b2" ] by metis
qed
lemma security_and_P1':
shows "¦spmf ((and_R1 (a1, a2) (b1,b2)) ⤜ D) True -
spmf ((and_funct (a1, a2) (b1,b2)) ⤜ (λ (s1, s2). (S1_and' (a1,a2) (b1,b2) s1)
⤜ (D :: (((bool × bool) × bool × 'v_14_OT1) × (share_1 × share_2)) ⇒ bool spmf))) True¦ ≤ adv_14_OT"
proof-
have "¦spmf ((and_R1 (a1, a2) (b1,b2)) ⤜ D) True -
spmf ((and_funct (a1, a2) (b1,b2)) ⤜ (λ (s1, s2). (S1_and' (a1,a2) (b1,b2) s1)
⤜ (D :: (((bool × bool) × bool × 'v_14_OT1) × (share_1 × share_2)) ⇒ bool spmf))) True¦ =
¦spmf ((and_funct (a1, a2) (b1,b2)) ⤜ (λ (s1, s2). (S1_and' (a1,a2) (b1,b2) s1)
⤜ (D :: (((bool × bool) × bool × 'v_14_OT1) × (share_1 × share_2)) ⇒ bool spmf))) True -
spmf ((and_R1 (a1, a2) (b1,b2)) ⤜ D) True¦" using abs_minus_commute by blast
thus ?thesis using security_and_P1 by simp
qed
definition and_R2 :: "(share_1 × share_2) ⇒ (share_2 × share_1) ⇒ (((bool × bool) × 'v_14_OT2) × (share_1 × share_2)) spmf"
where "and_R2 A B = do {
let (a1, a2) = A;
let (b1,b2) = B;
σ ← coin_spmf;
let s0 = σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ False));
let s1 = σ ⊕ ((a1 ⊕ False) ∧ (a2 ⊕ True));
let s2 = σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ False));
let s3 = σ ⊕ ((a1 ⊕ True) ∧ (a2 ⊕ True));
(_, s) ← protocol_14_OT (s0,s1,s2,s3) B;
V ← R2_14_OT (s0,s1,s2,s3) B;
return_spmf ((B, V), (σ, s))}"
lemma lossless_and_R2: "lossless_spmf (and_R2 A B)"
apply(simp add: and_R2_def split_def lossless_R2_14_OT lossless_protocol_14_OT Let_def)
by (metis lossless_R2_14_OT prod.collapse)
definition S2_and :: "(share_1 × share_2) ⇒ bool ⇒ (((bool × bool) × 'v_14_OT2)) spmf"
where "S2_and B s2 = do {
let (a2,b2) = B;
V :: 'v_14_OT2 ← S2_14_OT (a2,b2) s2;
return_spmf ((B, V))}"
definition out2 :: "(share_1 × share_2) ⇒ (share_1 × share_2) ⇒ bool ⇒ (share_1 × share_2) spmf"
where "out2 B A s2 = do {
let (a1, b1) = A;
let (a2,b2) = B;
let s1 = s2 ⊕ ((a1 ⊕ a2) ∧ (b1 ⊕ b2));
return_spmf (s1, s2)}"
definition S2_and' :: "(share_1 × share_2) ⇒ (share_1 × share_2) ⇒ bool ⇒ (((bool × bool) × 'v_14_OT2) × (share_1 × share_2)) spmf"
where "S2_and' B A s2 = do {
let (a1, a2) = A;
let (b1,b2) = B;
V :: 'v_14_OT2 ← S2_14_OT B s2;
let s1 = s2 ⊕ ((a1 ⊕ b1) ∧ (a2 ⊕ b2));
return_spmf ((B, V), s1, s2)}"
lemma lossless_S2_and: "lossless_spmf (S2_and B s2)"
apply(simp add: S2_and_def split_def)
by(metis prod.collapse lossless_S2_14_OT)
sublocale and_secret_sharing: sim_non_det_def and_R1 S1_and out1 and_R2 S2_and out2 and_funct .
lemma ideal_S1_and: "and_secret_sharing.Ideal1 (a1, b1) (a2, b2) s2 = S1_and' (a1, b1) (a2, b2) s2"
by(simp add: Let_def and_secret_sharing.Ideal1_def S1_and'_def split_def out1_def S1_and_def)
lemma and_P2_security: "and_secret_sharing.perfect_sec_P2 m1 m2"
proof-
have "and_R2 (a1, b1) (a2, b2) = and_funct (a1, b1) (a2, b2) ⤜ (λ(s1, s2). and_secret_sharing.Ideal2 (a2, b2) (a1, b1) s2)"
for a1 a2 b1 b2
apply(auto simp add: split_def inf_th_14_OT_P4 S2_and'_def and_R2_def and_funct_def Let_def correct_14[symmetric] and_secret_sharing.Ideal2_def S2_and_def out2_def)
apply(simp only: funct_14)
apply auto
by(cases b1;cases b2; cases a1; cases a2; auto)
thus ?thesis
by(simp add: and_secret_sharing.perfect_sec_P2_def; metis prod.collapse)
qed
lemma and_P1_security: "and_secret_sharing.adv_P1 m1 m2 D ≤ adv_14_OT"
proof-
have "¦spmf (and_R1 (a1, a2) (b1, b2) ⤜ D) True -
spmf (and_funct (a1, a2) (b1, b2) ⤜ (λ(s1, s2).
and_secret_sharing.Ideal1 (a1, a2) (b1, b2) s1 ⤜ D)) True¦
≤ adv_14_OT" for a1 a2 b1 b2
using security_and_P1' ideal_S1_and prod.collapse by simp
thus ?thesis
by(simp add: and_secret_sharing.adv_P1_def; metis prod.collapse)
qed
definition "F = {and_evaluate, xor_evaluate}"
lemma share_reconstruct_xor: "share x ⤜ (λ(a1, a2). share y ⤜ (λ(b1, b2).
xor_protocol (a1, b1) (a2, b2) ⤜ (λ(a, b).
reconstruct (a, b)))) = xor_evaluate x y"
proof-
have "(((ya = (x = ya)) = (yb = (y = (¬ yb))))) = (x = (¬ y))" for ya yb by auto
thus ?thesis
by(simp add: xor_protocol_def share_def reconstruct_def xor_evaluate_def bind_spmf_const)
qed
sublocale share_correct: secret_sharing_scheme share reconstruct F .
lemma "share_correct.sharing_correct input"
by(simp add: share_correct.sharing_correct_def reconstruct_share)
lemma "share_correct.correct_share_eval input1 input2"
unfolding share_correct.correct_share_eval_def
apply(auto simp add: F_def)
using share_and_reconstruct apply auto
using share_reconstruct_xor by force
end
locale gmw_asym =
fixes S1_14_OT :: "nat ⇒ msgs_14_OT ⇒ unit ⇒ 'v_14_OT1 spmf"
and R1_14_OT :: "nat ⇒ msgs_14_OT ⇒ choice_14_OT ⇒ 'v_14_OT1 spmf"
and S2_14_OT :: "nat ⇒ choice_14_OT ⇒ bool ⇒ 'v_14_OT2 spmf"
and R2_14_OT :: "nat ⇒ msgs_14_OT ⇒ choice_14_OT ⇒ 'v_14_OT2 spmf"
and protocol_14_OT :: "nat ⇒ msgs_14_OT ⇒ choice_14_OT ⇒ (unit × bool) spmf"
and adv_14_OT :: "nat ⇒ real"
assumes gmw_base: "⋀ (n::nat). gmw_base (S1_14_OT n) (R1_14_OT n) (S2_14_OT n) (R2_14_OT n) (protocol_14_OT n) (adv_14_OT n)"
begin
sublocale gmw_base "(S1_14_OT n)" "(R1_14_OT n)" "(S2_14_OT n)" "(R2_14_OT n)" "(protocol_14_OT n)" "(adv_14_OT n)"
by (simp add: gmw_base)
lemma "xor_sim_det.perfect_sec_P1 m1 m2"
by (simp add: P1_xor_inf_th xor_sim_det.perfect_sec_P1_def)
lemma "xor_sim_det.perfect_sec_P2 m1 m2"
by (simp add: P2_xor_inf_th xor_sim_det.perfect_sec_P2_def)
lemma and_P1_adv_negligible:
assumes "negligible (λ n. adv_14_OT n)"
shows "negligible (λ n. and_secret_sharing.adv_P1 n m1 m2 D)"
proof-
have "and_secret_sharing.adv_P1 n m1 m2 D ≤ adv_14_OT n" for n
by (simp add: and_P1_security)
thus ?thesis
using and_secret_sharing.adv_P1_def assms negligible_le by auto
qed
lemma and_P2_security: "and_secret_sharing.perfect_sec_P2 n m1 m2"
by (simp add: and_P2_security)
end
end