Theory Sigma_OR
subsection‹‹Σ›-OR statements›
theory Sigma_OR imports
Sigma_Protocols
Xor
begin
locale Σ_OR_base = Σ0: Σ_protocols_base init0 response0 check0 Rel0 S0_raw 𝒜ss0 "carrier L" valid_pub0
+ Σ1: Σ_protocols_base init1 response1 check1 Rel1 S1_raw 𝒜ss1 "carrier L" valid_pub1
for init1 :: "'pub1 ⇒ 'witness1 ⇒ ('rand1 × 'msg1) spmf"
and response1 :: "'rand1 ⇒ 'witness1 ⇒ 'bool ⇒ 'response1 spmf"
and check1 :: "'pub1 ⇒ 'msg1 ⇒ 'bool ⇒ 'response1 ⇒ bool"
and Rel1 :: "('pub1 × 'witness1) set"
and S1_raw :: "'pub1 ⇒ 'bool ⇒ ('msg1 × 'response1) spmf"
and 𝒜ss1 :: "'pub1 ⇒ 'msg1 × 'bool × 'response1 ⇒ 'msg1 × 'bool × 'response1 ⇒ 'witness1 spmf"
and challenge_space1 :: "'bool set"
and valid_pub1 :: "'pub1 set"
and init0 :: "'pub0 ⇒ 'witness0 ⇒ ('rand0 × 'msg0) spmf"
and response0 :: "'rand0 ⇒ 'witness0 ⇒ 'bool ⇒ 'response0 spmf"
and check0 :: "'pub0 ⇒ 'msg0 ⇒ 'bool ⇒ 'response0 ⇒ bool"
and Rel0 :: "('pub0 × 'witness0) set"
and S0_raw :: "'pub0 ⇒ 'bool ⇒ ('msg0 × 'response0) spmf"
and 𝒜ss0 :: "'pub0 ⇒ 'msg0 × 'bool × 'response0 ⇒ 'msg0 × 'bool × 'response0 ⇒ 'witness0 spmf"
and challenge_space0 :: "'bool set"
and valid_pub0 :: "'pub0 set"
and G :: "(('pub0 × 'pub1) × ('witness0 + 'witness1)) spmf"
and L :: "'bool boolean_algebra" (structure)
+
assumes Σ_prot1: "Σ1.Σ_protocol"
and Σ_prot0: "Σ0.Σ_protocol"
and lossless_init: "lossless_spmf (init0 h0 w0)" "lossless_spmf (init1 h1 w1)"
and lossless_response: "lossless_spmf (response0 r0 w0 e0)" "lossless_spmf (response1 r1 w1 e1)"
and lossless_S: "lossless_spmf (S0 h0 e0)" "lossless_spmf (S1 h1 e1)"
and finite_L: "finite (carrier L)"
and carrier_L_not_empty: "carrier L ≠ {}"
and lossless_G: "lossless_spmf G"
begin
inductive_set Rel_OR :: "(('pub0 × 'pub1) × ('witness0 + 'witness1)) set" where
Rel_OR_I0: "((x0, x1), Inl w0) ∈ Rel_OR" if "(x0, w0) ∈ Rel0 ∧ x1 ∈ valid_pub1"
| Rel_OR_I1: "((x0, x1), Inr w1) ∈ Rel_OR" if "(x1, w1) ∈ Rel1 ∧ x0 ∈ valid_pub0"
inductive_simps Rel_OR_simps [simp]:
"((x0, x1), Inl w0) ∈ Rel_OR"
"((x0, x1), Inr w1) ∈ Rel_OR"
lemma Domain_Rel_cases:
assumes "(x0,x1) ∈ Domain Rel_OR"
shows "(∃ w0. (x0,w0) ∈ Rel0 ∧ x1 ∈ valid_pub1) ∨ (∃ w1. (x1,w1) ∈ Rel1 ∧ x0 ∈ valid_pub0)"
using assms
by (meson DomainE Rel_OR.cases)
lemma set_spmf_lists_sample [simp]: "set_spmf (spmf_of_set (carrier L)) = (carrier L)"
using finite_L by simp
definition "challenge_space = carrier L"
fun init_OR :: "('pub0 × 'pub1) ⇒ ('witness0 + 'witness1) ⇒ (((('rand0 × 'bool × 'response1 + 'rand1 × 'bool × 'response0)) × 'msg0 × 'msg1)) spmf"
where "init_OR (x0,x1) (Inl w0) = do {
(r0,a0) ← init0 x0 w0;
e1 ← spmf_of_set (carrier L);
(a1, e'1, z1) ← Σ1.S x1 e1;
return_spmf (Inl (r0, e1, z1), a0, a1)}" |
"init_OR (x0, x1) (Inr w1) = do {
(r1, a1) ← init1 x1 w1;
e0 ← spmf_of_set (carrier L);
(a0, e'0, z0) ← Σ0.S x0 e0;
return_spmf ((Inr (r1, e0, z0), a0, a1))}"
lemma lossless_Σ_S: "lossless_spmf (Σ1.S x1 e1)" "lossless_spmf (Σ0.S x0 e0)"
using lossless_S by fast +
lemma lossless_init_OR: "lossless_spmf (init_OR (x0,x1) w)"
by(cases w;simp add: lossless_Σ_S split_def lossless_init lossless_S finite_L carrier_L_not_empty)
fun response_OR :: "(('rand0 × 'bool × 'response1 + 'rand1 × 'bool × 'response0)) ⇒ ('witness0 + 'witness1)
⇒ 'bool ⇒ (('bool × 'response0) × ('bool × 'response1)) spmf"
where "response_OR (Inl (r0 , e_1, z1)) (Inl w0) s = do {
let e0 = s ⊕ e_1;
z0 ← response0 r0 w0 e0;
return_spmf ((e0,z0), (e_1,z1))}" |
"response_OR (Inr (r1, e_0, z0)) (Inr w1) s = do {
let e1 = s ⊕ e_0;
z1 ← response1 r1 w1 e1;
return_spmf ((e_0, z0), (e1, z1))}"
definition check_OR :: "('pub0 × 'pub1) ⇒ ('msg0 × 'msg1) ⇒ 'bool ⇒ (('bool × 'response0) × ('bool × 'response1)) ⇒ bool"
where "check_OR X A s Z
= (s = (fst (fst Z)) ⊕ (fst (snd Z))
∧ (fst (fst Z)) ∈ challenge_space ∧ (fst (snd Z)) ∈ challenge_space
∧ check0 (fst X) (fst A) (fst (fst Z)) (snd (fst Z)) ∧ check1 (snd X) (snd A) (fst (snd Z)) (snd (snd Z)))"
lemma "check_OR (x0,x1) (a0,a1) s ((e0,z0), (e1,z1))
= (s = e0 ⊕ e1
∧ e0 ∈ challenge_space ∧ e1 ∈ challenge_space
∧ check0 x0 a0 e0 z0 ∧ check1 x1 a1 e1 z1)"
by(simp add: check_OR_def)
fun S_OR where "S_OR (x0,x1) c = do {
e1 ← spmf_of_set (carrier L);
(a1, e1', z1) ← Σ1.S x1 e1;
let e0 = c ⊕ e1;
(a0, e0', z0) ← Σ0.S x0 e0;
let z = ((e0',z0), (e1',z1));
return_spmf ((a0, a1),z)}"
definition 𝒜ss_OR' :: "'pub0 × 'pub1 ⇒ ('msg0 × 'msg1) × 'bool × ('bool × 'response0) × 'bool × 'response1
⇒ ('msg0 × 'msg1) × 'bool × ('bool × 'response0) × 'bool × 'response1 ⇒ ('witness0 + 'witness1) spmf"
where "𝒜ss_OR' X C1 C2 = TRY do {
_ :: unit ← assert_spmf ((fst (fst (snd (snd C1)))) ≠ (fst (fst (snd (snd C2)))));
w0 :: 'witness0 ← 𝒜ss0 (fst X) (fst (fst C1),fst (fst (snd (snd C1))),snd (fst (snd (snd C1)))) (fst (fst C2),fst (fst (snd (snd C2))),snd (fst (snd (snd C2))));
return_spmf ((Inl w0)) :: ('witness0 + 'witness1) spmf} ELSE do {
w1 :: 'witness1 ← 𝒜ss1 (snd X) (snd (fst C1),fst (snd (snd (snd C1))), snd (snd (snd (snd C1)))) (snd (fst C2), fst (snd (snd (snd C2))), snd (snd (snd (snd C2))));
(return_spmf ((Inr w1)) :: ('witness0 + 'witness1) spmf)}"
definition 𝒜ss_OR :: "'pub0 × 'pub1 ⇒ ('msg0 × 'msg1) × 'bool × ('bool × 'response0) × 'bool × 'response1
⇒ ('msg0 × 'msg1) × 'bool × ('bool × 'response0) × 'bool × 'response1 ⇒ ('witness0 + 'witness1) spmf"
where "𝒜ss_OR X C1 C2 = do {
if ((fst (fst (snd (snd C1)))) ≠ (fst (fst (snd (snd C2))))) then do
{w0 :: 'witness0 ← 𝒜ss0 (fst X) (fst (fst C1),fst (fst (snd (snd C1))),snd (fst (snd (snd C1)))) (fst (fst C2),fst (fst (snd (snd C2))),snd (fst (snd (snd C2)))); return_spmf (Inl w0)}
else
do {w1 :: 'witness1 ← 𝒜ss1 (snd X) (snd (fst C1),fst (snd (snd (snd C1))), snd (snd (snd (snd C1)))) (snd (fst C2), fst (snd (snd (snd C2))), snd (snd (snd (snd C2)))); return_spmf (Inr w1)}}"
lemma 𝒜ss_OR_alt_def: "𝒜ss_OR (x0,x1) ((a0,a1),s,(e0,z0),e1,z1) ((a0,a1),s',(e0',z0'),e1',z1') = do {
if (e0 ≠ e0') then do {w0 :: 'witness0 ← 𝒜ss0 x0 (a0,e0,z0) (a0,e0',z0'); return_spmf (Inl w0)}
else do {w1 :: 'witness1 ← 𝒜ss1 x1 (a1,e1,z1) (a1,e1',z1'); return_spmf (Inr w1)}}"
by(simp add: 𝒜ss_OR_def)
definition "valid_pub_OR = {(x0,x1). x0 ∈ valid_pub0 ∧ x1 ∈ valid_pub1}"
sublocale Σ_OR: Σ_protocols_base init_OR response_OR check_OR Rel_OR S_OR 𝒜ss_OR challenge_space valid_pub_OR
unfolding Σ_protocols_base_def
proof(goal_cases)
case 1
then show ?case
proof
fix x
assume asm: "x ∈ Domain Rel_OR"
then obtain x0 x1 where x: "(x0,x1) = x"
by (metis surj_pair)
show "x ∈ valid_pub_OR"
proof(cases "∃ w0. (x0,w0) ∈ Rel0 ∧ x1 ∈ valid_pub1")
case True
then show ?thesis
using Σ0.domain_subset_valid_pub valid_pub_OR_def x by auto
next
case False
hence "∃ w1. (x1,w1) ∈ Rel1 ∧ x0 ∈ valid_pub0"
using Domain_Rel_cases asm x by auto
then show ?thesis
using Σ1.domain_subset_valid_pub valid_pub_OR_def x by auto
qed
qed
qed
end
locale Σ_OR_proofs = Σ_OR_base + boolean_algebra L +
assumes G_Rel_OR: "((x0, x1), w) ∈ set_spmf G ⟹ ((x0, x1), w) ∈ Rel_OR"
and lossless_response_OR: "lossless_spmf (response_OR R W s)"
begin
lemma HVZK1:
assumes "(x1,w1) ∈ Rel1"
shows "∀ c ∈ challenge_space. Σ_OR.R (x0,x1) (Inr w1) c = Σ_OR.S (x0,x1) c"
including monad_normalisation
proof
fix c
assume c: "c ∈ challenge_space"
show "Σ_OR.R (x0,x1) (Inr w1) c = Σ_OR.S (x0,x1) c"
proof-
have *: "x ∈ carrier L ⟶ c ⊕ c ⊕ x = x" for x
using c challenge_space_def by auto
have "Σ_OR.R (x0,x1) (Inr w1) c = do {
(r1, ab1) ← init1 x1 w1;
eb' ← spmf_of_set (carrier L);
(ab0', eb0'', zb0') ← Σ0.S x0 eb';
let ((r, eb', zb'),a) = ((r1, eb', zb0' ), ab0' , ab1);
let eb = c ⊕ eb';
zb1 ← response1 r w1 eb;
let z = ((eb', zb') , (eb, zb1));
return_spmf (a,c,z)}"
supply [[simproc del: monad_normalisation]]
by(simp add: Σ_OR.R_def split_def Let_def)
also have "... = do {
eb' ← spmf_of_set (carrier L);
(ab0', eb0'', zb0') ← Σ0.S x0 eb';
let eb = c ⊕ eb';
(ab1, c', zb1) ← Σ1.R x1 w1 eb;
let z = ((eb', zb0'), (eb, zb1));
return_spmf ((ab0',ab1),c,z)}"
by(simp add: Σ1.R_def split_def Let_def)
also have "... = do {
eb' ← spmf_of_set (carrier L);
(ab0', eb0'', zb0') ← Σ0.S x0 eb';
let eb = c ⊕ eb';
(ab1, c', zb1) ← Σ1.S x1 eb;
let z = ((eb', zb0'), (eb, zb1));
return_spmf ((ab0',ab1),c,z)}"
using c
by(simp add: split_def Let_def Σ_prot1 Σ1.HVZK_unfold1 assms challenge_space_def cong: bind_spmf_cong_simp)
also have "... = do {
eb ← map_spmf (λ eb'. c ⊕ eb') (spmf_of_set (carrier L));
(ab1, c', zb1) ← Σ1.S x1 eb;
(ab0', eb0'', zb0') ← Σ0.S x0 (c ⊕ eb);
let z = ((c ⊕ eb, zb0'), (eb, zb1));
return_spmf ((ab0',ab1),c,z)}"
apply(simp add: bind_map_spmf o_def Let_def)
by(simp add: * split_def cong: bind_spmf_cong_simp)
also have "... = do {
eb ← (spmf_of_set (carrier L));
(ab1, c', zb1) ← Σ1.S x1 eb;
(ab0', eb0'', zb0') ← Σ0.S x0 (c ⊕ eb);
let z = ((c ⊕ eb, zb0'), (eb, zb1));
return_spmf ((ab0',ab1),c,z)}"
using assms assms one_time_pad c challenge_space_def by simp
also have "... = do {
eb ← (spmf_of_set (carrier L));
(ab1, c', zb1) ← Σ1.S x1 eb;
(ab0', eb0'', zb0') ← Σ0.S x0 (c ⊕ eb);
let z = ((eb0'', zb0'), (c', zb1));
return_spmf ((ab0',ab1),c,z)}"
by(simp add: Σ0.S_def Σ1.S_def bind_map_spmf o_def split_def)
ultimately show ?thesis by(simp add: Let_def map_spmf_conv_bind_spmf Σ_OR.S_def split_def)
qed
qed
lemma HVZK0:
assumes "(x0,w0) ∈ Rel0"
shows "∀ c ∈ challenge_space. Σ_OR.R (x0,x1) (Inl w0) c = Σ_OR.S (x0,x1) c"
proof
fix c
assume c: "c ∈ challenge_space"
show "Σ_OR.R (x0,x1) (Inl w0) c = Σ_OR.S (x0,x1) c"
proof-
have "Σ_OR.R (x0,x1) (Inl w0) c = do {
(r0,ab0) ← init0 x0 w0;
eb' ← spmf_of_set (carrier L);
(ab1', eb1'', zb1') ← Σ1.S x1 eb';
let ((r, eb', zb'),a) = ((r0, eb', zb1'), ab0, ab1');
let eb = c ⊕ eb';
zb0 ← response0 r w0 eb;
let z = ((eb,zb0), (eb',zb'));
return_spmf (a,c,z)}"
by(simp add: Σ_OR.R_def split_def Let_def)
also have "... = do {
eb' ← (spmf_of_set (carrier L));
(ab1', eb1'', zb1') ← Σ1.S x1 eb';
let eb = c ⊕ eb';
(ab0, c', zb0) ← Σ0.R x0 w0 eb;
let z = ((eb,zb0), (eb',zb1'));
return_spmf ((ab0, ab1'),c,z)}"
apply(simp add: Σ0.R_def split_def Let_def)
apply(rewrite bind_commute_spmf)
apply(rewrite bind_commute_spmf[of _ "Σ1.S _ _"])
by simp
also have "... = do {
eb' ← (spmf_of_set (carrier L));
(ab1', eb1'', zb1') ← Σ1.S x1 eb';
let eb = c ⊕ eb';
(ab0, c', zb0) ← Σ0.S x0 eb;
let z = ((eb,zb0), (eb',zb1'));
return_spmf ((ab0, ab1'),c,z)}"
using c
by(simp add: Σ_prot0 Σ0.HVZK_unfold1 assms challenge_space_def split_def Let_def cong: bind_spmf_cong_simp)
ultimately show ?thesis
by(simp add: Σ_OR.S_def Σ1.S_def Σ0.S_def Let_def o_def bind_map_spmf split_def map_spmf_conv_bind_spmf)
qed
qed
lemma HVZK:
shows "Σ_OR.HVZK"
unfolding Σ_OR.HVZK_def
apply auto
subgoal for e a b w
apply(cases w)
using HVZK0 HVZK1 by auto
apply(auto simp add: valid_pub_OR_def Σ_OR.S_def bind_map_spmf o_def check_OR_def image_def Σ0.S_def Σ1.S_def split_def challenge_space_def local.xor_ac(1))
using Σ0.HVZK_unfold2 Σ_prot0 challenge_space_def apply force
using Σ1.HVZK_unfold2 Σ_prot1 challenge_space_def by force
lemma assumes "(x0,x1) ∈ Domain Rel_OR"
shows "(∃ w0. (x0,w0) ∈ Rel0) ∨ (∃ w1. (x1,w1) ∈ Rel1)"
using assms Rel_OR.simps by blast
lemma ss:
assumes valid_pub_OR: "(x0,x1) ∈ valid_pub_OR"
and check: "check_OR (x0,x1) (a0,a1) s ((e0,z0), (e1,z1))"
and check': "check_OR (x0,x1) (a0,a1) s' ((e0',z0'), (e1',z1'))"
and "s ≠ s'"
and challenge_space: "s ∈ challenge_space" "s' ∈ challenge_space"
shows "lossless_spmf (𝒜ss_OR (x0,x1) ((a0,a1),s,(e0,z0), e1,z1) ((a0,a1),s',(e0',z0'), e1',z1')) ∧
(∀w'∈set_spmf (𝒜ss_OR (x0,x1) ((a0,a1),s,(e0,z0), e1,z1) ((a0,a1),s',(e0',z0'), e1',z1')). ((x0,x1), w') ∈ Rel_OR)"
proof-
have e_or: "e0 ≠ e0' ∨ e1 ≠ e1'" using assms check_OR_def by auto
show ?thesis
proof(cases "e0 ≠ e0'")
case True
moreover have 2: "x0 ∈ valid_pub0"
using valid_pub_OR valid_pub_OR_def by simp
moreover have 3: "check0 x0 a0 e0 z0"
using assms check_OR_def by simp
moreover have 4: "check0 x0 a0 e0' z0'"
using assms check_OR_def by simp
moreover have e: "e0 ∈ carrier L" "e0' ∈ carrier L"
using challenge_space_def check check' check_OR_def by auto
ultimately have "(∀w'∈set_spmf (𝒜ss0 x0 (a0,e0,z0) (a0,e0',z0')). (x0, w') ∈ Rel0)"
using True Σ0.Σ_protocol_def Σ0.special_soundness_def Σ_prot0 challenge_space assms by blast
moreover have "lossless_spmf (𝒜ss0 x0 (a0, e0, z0) (a0, e0', z0'))"
using 2 3 4 𝒜ss_OR_def True Σ_prot0 Σ0.Σ_protocol_def Σ0.special_soundness_def challenge_space_def e by blast
ultimately have "∀ w' ∈ set_spmf (𝒜ss_OR (x0,x1) ((a0,a1),s,(e0,z0), e1,z1) ((a0,a1),s',(e0',z0'), e1',z1')). ((x0,x1), w') ∈ Rel_OR"
apply(auto simp only: 𝒜ss_OR_alt_def True)
apply(auto simp add: o_def 𝒜ss_OR_def)
using assms valid_pub_OR_def by blast
moreover have "lossless_spmf (𝒜ss_OR (x0,x1) ((a0,a1),s,(e0,z0), e1,z1) ((a0,a1),s',(e0',z0'), e1',z1'))"
apply(simp add: 𝒜ss_OR_def)
using 2 3 4 True Σ_prot0 Σ0.Σ_protocol_def Σ0.special_soundness_def challenge_space e by blast
ultimately show ?thesis by simp
next
case False
hence e1_neq_e1': "e1 ≠ e1'" using e_or by simp
moreover have 2: "x1 ∈ valid_pub1"
using valid_pub_OR valid_pub_OR_def by simp
moreover have 3: "check1 x1 a1 e1 z1"
using assms check_OR_def by simp
moreover have 4: "check1 x1 a1 e1' z1'"
using assms check_OR_def by simp
moreover have e: "e1 ∈ carrier L" "e1' ∈ carrier L"
using challenge_space_def check check' check_OR_def by auto
ultimately have "(∀w'∈set_spmf (𝒜ss1 x1 (a1,e1,z1) (a1,e1',z1')). (x1,w') ∈ Rel1)"
using False Σ1.Σ_protocol_def Σ1.special_soundness_def Σ_prot1 e1_neq_e1' challenge_space by blast
hence "∀w' ∈ set_spmf (𝒜ss_OR (x0,x1) ((a0,a1),s,(e0,z0), e1,z1) ((a0,a1),s',(e0',z0'), e1',z1')). ((x0,x1), w') ∈ Rel_OR"
apply(auto simp add: o_def 𝒜ss_OR_def)
using False assms Σ1.L_def assms valid_pub_OR_def by auto
moreover have "lossless_spmf (𝒜ss_OR (x0,x1) ((a0,a1),s,(e0,z0), e1,z1) ((a0,a1),s',(e0',z0'), e1',z1'))"
apply(simp add: 𝒜ss_OR_def)
using 2 3 4 Σ_prot1 Σ1.Σ_protocol_def Σ1.special_soundness_def False e1_neq_e1' challenge_space e by blast
ultimately show ?thesis by simp
qed
qed
lemma special_soundness:
shows "Σ_OR.special_soundness"
unfolding Σ_OR.special_soundness_def
using ss prod.collapse by fastforce
lemma correct0:
assumes e_in_carrier: "e ∈ carrier L"
and "(x0,w0) ∈ Rel0"
and valid_pub: "x1 ∈ valid_pub1"
shows "Σ_OR.completeness_game (x0,x1) (Inl w0) e = return_spmf True"
(is "?lhs = ?rhs")
proof-
have "x ∈ carrier L ⟶ e = (e ⊕ x) ⊕ x" for x
using e_in_carrier xor_assoc by simp
hence "?lhs = do {
(r0,ab0) ← init0 x0 w0;
eb' ← spmf_of_set (carrier L);
(ab1', eb1'', zb1') ← Σ1.S x1 eb';
let eb = e ⊕ eb';
zb0 ← response0 r0 w0 eb;
return_spmf ((check0 x0 ab0 eb zb0 ∧ check1 x1 ab1' eb' zb1'))}"
by(simp add: Σ_OR.completeness_game_def split_def Let_def challenge_space_def assms check_OR_def cong: bind_spmf_cong_simp)
also have "... = do {
eb' ← spmf_of_set (carrier L);
(ab1', eb1'', zb1') ← Σ1.S x1 eb';
let eb = e ⊕ eb';
(r0,ab0) ← init0 x0 w0;
zb0 ← response0 r0 w0 eb;
return_spmf ((check0 x0 ab0 eb zb0 ∧ check1 x1 ab1' eb' zb1'))}"
apply(simp add: Let_def split_def)
apply(rewrite bind_commute_spmf)
apply(rewrite bind_commute_spmf[of _ "Σ1.S _ _"])
by simp
also have "... = do {
eb' :: 'e ← spmf_of_set (carrier L);
(ab1', eb1'', zb1') ← Σ1.S x1 eb';
return_spmf (check1 x1 ab1' eb' zb1')}"
apply(simp add: Let_def)
apply(intro bind_spmf_cong; clarsimp?)+
subgoal for e' a e z
apply(cases "check1 x1 a e' z")
using Σ0.complete_game_return_true Σ_prot0 Σ0.completeness_game_def Σ0.Σ_protocol_def
by(auto simp add: assms bind_spmf_const lossless_init lossless_response lossless_weight_spmfD split_def cong: bind_spmf_cong_simp)
done
also have "... = do {
eb' :: 'e ← spmf_of_set (carrier L);
(ab1', eb1'', zb1') ← Σ1.S x1 eb';
return_spmf (True)}"
apply(intro bind_spmf_cong; clarsimp?)
subgoal for x a aa b
using Σ_prot1
apply(auto simp add: Σ1.S_def split_def image_def Σ1.HVZK_unfold2_alt)
using Σ1.S_def split_def image_def Σ1.HVZK_unfold2_alt Σ_prot1 valid_pub by blast
done
ultimately show ?thesis
using Σ1.HVZK_unfold2_alt
by(simp add: bind_spmf_const Let_def Σ1.HVZK_unfold2_alt split_def lossless_Σ_S lossless_weight_spmfD carrier_L_not_empty finite_L)
qed
lemma correct1:
assumes rel1: "(x1,w1) ∈ Rel1"
and valid_pub: "x0 ∈ valid_pub0"
and e_in_carrier: "e ∈ carrier L"
shows "Σ_OR.completeness_game (x0,x1) (Inr w1) e = return_spmf True"
(is "?lhs = ?rhs")
proof-
have x1_inL: "x1 ∈ Σ1.L"
using Σ1.L_def rel1 by auto
have "x ∈ carrier L ⟶ e = x ⊕ e ⊕ x" for x
by (simp add: e_in_carrier xor_assoc xor_commute local.xor_ac(3))
hence "?lhs = do {
(r1, ab1) ← init1 x1 w1;
eb' ← spmf_of_set (carrier L);
(ab0', eb0'', zb0') ← Σ0.S x0 eb';
let eb = e ⊕ eb';
zb1 ← response1 r1 w1 eb;
return_spmf (check0 x0 ab0' eb' zb0' ∧ check1 x1 ab1 eb zb1)}"
by(simp add: Σ_OR.completeness_game_def split_def Let_def assms challenge_space_def check_OR_def cong: bind_spmf_cong_simp)
also have "... = do {
eb' ← spmf_of_set (carrier L);
(ab0', eb0'', zb0') ← Σ0.S x0 eb';
let eb = e ⊕ eb';
(r1, ab1) ← init1 x1 w1;
zb1 ← response1 r1 w1 eb;
return_spmf (check0 x0 ab0' eb' zb0' ∧ check1 x1 ab1 eb zb1)}"
apply(simp add: Let_def split_def)
apply(rewrite bind_commute_spmf)
apply(rewrite bind_commute_spmf[of _ "Σ0.S _ _"])
by simp
also have "... = do {
eb' ← spmf_of_set (carrier L);
(ab0', eb0'', zb0') ← Σ0.S x0 eb';
return_spmf (check0 x0 ab0' eb' zb0')}"
apply(simp add: Let_def)
apply(intro bind_spmf_cong; clarsimp?)+
subgoal for e' a e z
apply(cases "check0 x0 a e' z")
using Σ1.complete_game_return_true Σ_prot1 Σ1.completeness_game_def Σ1.Σ_protocol_def
by(auto simp add: x1_inL assms bind_spmf_const lossless_init lossless_response lossless_weight_spmfD split_def)
done
also have "... = do {
eb' ← spmf_of_set (carrier L);
(ab0', eb0'', zb0') ← Σ0.S x0 eb';
return_spmf (True)}"
apply(intro bind_spmf_cong; clarsimp?)
subgoal for x a aa b
using Σ_prot0
by(auto simp add: valid_pub valid_pub_OR_def Σ0.S_def split_def image_def Σ0.HVZK_unfold2_alt)
done
ultimately show ?thesis
apply(simp add: Σ0.HVZK_unfold2 Let_def)
using Σ0.complete_game_return_true Σ_OR.completeness_game_def
by(simp add: bind_spmf_const split_def lossless_Σ_S(2) lossless_weight_spmfD Let_def carrier_L_not_empty finite_L)
qed
lemma completeness':
assumes Rel_OR_asm: "((x0,x1), w) ∈ Rel_OR"
shows "∀ e ∈ carrier L. spmf (Σ_OR.completeness_game (x0,x1) w e) True = 1"
proof
fix e
assume asm: "e ∈ carrier L"
hence "(Σ_OR.completeness_game (x0,x1) w e) = return_spmf True"
proof(cases w)
case inl: (Inl a)
then show ?thesis
using asm correct0 assms inl by auto
next
case inr: (Inr b)
then show ?thesis
using asm correct1 assms inr by auto
qed
thus "spmf (Σ_OR.completeness_game (x0,x1) w e) True = 1"
by simp
qed
lemma completeness: shows "Σ_OR.completeness"
unfolding Σ_OR.completeness_def
using completeness' challenge_space_def by auto
lemma Σ_protocol: shows "Σ_OR.Σ_protocol"
by(simp add: completeness HVZK special_soundness Σ_OR.Σ_protocol_def)
sublocale OR_Σ_commit: Σ_protocols_to_commitments init_OR response_OR check_OR Rel_OR S_OR 𝒜ss_OR challenge_space valid_pub_OR G
by unfold_locales (auto simp add: Σ_protocol lossless_G lossless_init_OR G_Rel_OR lossless_response_OR)
lemma "OR_Σ_commit.abstract_com.correct"
using OR_Σ_commit.commit_correct by simp
lemma "OR_Σ_commit.abstract_com.perfect_hiding_ind_cpa 𝒜"
using OR_Σ_commit.perfect_hiding by blast
lemma bind_advantage_bound_dis_log:
shows "OR_Σ_commit.abstract_com.bind_advantage 𝒜 ≤ OR_Σ_commit.rel_advantage (OR_Σ_commit.adversary 𝒜)"
using OR_Σ_commit.bind_advantage by simp
end
end