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"
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