Theory Sigma_AND

subsection‹‹Σ›-AND statements›

theory Sigma_AND imports
  Sigma_Protocols
  Xor
begin 

locale Σ_AND_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 lossless_𝒜ss: "lossless_spmf (𝒜ss0 x0 (a0,e,z0) (a0,e',z0'))" "lossless_spmf (𝒜ss1 x1 (a1,e,z1) (a1,e',z1'))" 
    and lossless_G: "lossless_spmf G"
    and set_spmf_G [simp]: "(h,w) ∈ set_spmf G ⟹ Rel h w"
begin

definition "challenge_space = carrier L"

definition Rel_AND :: "(('pub0 × 'pub1) × 'witness0 × 'witness1) set" 
  where "Rel_AND = {((x0,x1), (w0,w1)). ((x0,w0) ∈ Rel0 ∧ (x1,w1) ∈ Rel1)}"

definition init_AND :: "('pub0 × 'pub1) ⇒ ('witness0 × 'witness1) ⇒ (('rand0 × 'rand1) × 'msg0 × 'msg1) spmf" 
  where "init_AND X W = do {
    let (x0, x1) = X;
    let (w0,w1) = W;
    (r0, a0) ← init0 x0 w0;
    (r1, a1) ← init1 x1 w1;
    return_spmf ((r0,r1), (a0,a1))}"   

lemma lossless_init_AND: "lossless_spmf (init_AND X W)"
  by(simp add: lossless_init init_AND_def split_def)
    
definition response_AND :: "('rand0 × 'rand1) ⇒ ('witness0 × 'witness1) ⇒ 'bool ⇒ ('response0 × 'response1) spmf"
  where "response_AND R W s = do {
    let (r0,r1) = R;
    let (w0,w1) = W;  
    z0 ← response0 r0 w0 s;
    z1  :: 'response1 ← response1 r1 w1 s;
    return_spmf (z0,z1)}" 

lemma lossless_response_AND: "lossless_spmf (response_AND R W s)"
  by(simp add: response_AND_def lossless_response split_def)

fun check_AND :: "('pub0 × 'pub1) ⇒ ('msg0 × 'msg1) ⇒ 'bool ⇒ ('response0 × 'response1) ⇒ bool"
  where "check_AND (x0,x1) (a0,a1) s (z0,z1) = (check0 x0 a0 s z0 ∧ check1 x1 a1 s z1)"

definition S_AND :: "'pub0 × 'pub1 ⇒ 'bool ⇒ (('msg0 × 'msg1) × 'response0 × 'response1) spmf"
  where "S_AND X e = do {
    let (x0,x1) = X;
    (a0, z0) ← S0_raw x0 e;
    (a1, z1) ← S1_raw x1 e;
    return_spmf ((a0,a1),(z0,z1))}"

fun 𝒜ss_AND :: "'pub0 × 'pub1 ⇒ ('msg0 × 'msg1) × 'bool × 'response0 × 'response1 ⇒ ('msg0 × 'msg1) × 'bool × 'response0 × 'response1 ⇒ ('witness0 × 'witness1) spmf"
  where "𝒜ss_AND (x0,x1) ((a0,a1), e, (z0,z1)) ((a0',a1'), e', (z0',z1')) = do {
    w0 :: 'witness0 ← 𝒜ss0 x0 (a0,e,z0) (a0',e',z0');
    w1 ← 𝒜ss1 x1 (a1,e,z1) (a1',e',z1');
    return_spmf (w0,w1)}"

definition "valid_pub_AND = {(x0,x1). x0 ∈ valid_pub0 ∧ x1 ∈ valid_pub1}"

sublocale Σ_AND: Σ_protocols_base init_AND response_AND check_AND Rel_AND S_AND 𝒜ss_AND challenge_space valid_pub_AND 
  apply unfold_locales apply(simp add: Rel_AND_def valid_pub_AND_def)
  using Σ1.domain_subset_valid_pub Σ0.domain_subset_valid_pub by blast

end 

locale Σ_AND = Σ_AND_base +
  assumes set_spmf_G_L: "((x0, x1), w0, w1) ∈ set_spmf G ⟹ ((x0, x1), (w0,w1)) ∈ Rel_AND"
begin

lemma hvzk: 
  assumes Rel_AND: "((x0,x1), (w0,w1)) ∈ Rel_AND"
  and "e ∈ challenge_space" 
  shows "Σ_AND.R (x0,x1) (w0,w1) e = Σ_AND.S (x0,x1) e"
  including monad_normalisation
proof-
  have x_in_dom: "x0 ∈ Domain Rel0" and "x1 ∈ Domain Rel1" 
    using Rel_AND Rel_AND_def by auto
  have "Σ_AND.R (x0,x1) (w0,w1) e = do {
    ((r0,r1),(a0,a1)) ← init_AND (x0,x1) (w0,w1);
    (z0,z1) ← response_AND (r0,r1) (w0,w1) e;
    return_spmf ((a0,a1),e,(z0,z1))}"
    by(simp add: Σ_AND.R_def split_def)
  also have "... = do {
    (r0, a0) ← init0 x0 w0;
    z0 ← response0 r0 w0 e;
    (r1, a1) ← init1 x1 w1;
    z1 :: 'f ← response1 r1 w1 e;
    return_spmf ((a0,a1),e,(z0,z1))}"
    apply(simp add: init_AND_def response_AND_def split_def)
    apply(rewrite bind_commute_spmf[of "response0 _ w0 e"])
    by simp
  also have "... = do {
    (a0, c0, z0) ← Σ0.R x0 w0 e;
    (a1, c1, z1) ← Σ1.R x1 w1 e;
    return_spmf ((a0,a1),e,(z0,z1))}"
    by(simp add: Σ0.R_def Σ1.R_def split_def)
  also have "... = do {
    (a0, c0, z0) ← Σ0.S x0 e;
    (a1, c1, z1) ← Σ1.S x1 e;
    return_spmf ((a0,a1),e,(z0,z1))}"
    using Rel_AND_def S_AND_def Σ_prot1 Σ_prot0 assms  Σ0.HVZK_unfold1 Σ1.HVZK_unfold1 
          valid_pub_AND_def split_def challenge_space_def x_in_dom
    by auto
  ultimately show ?thesis 
    by(simp add: Σ0.S_def Σ1.S_def bind_map_spmf o_def split_def Let_def Σ_AND.S_def map_spmf_conv_bind_spmf S_AND_def)
qed

lemma HVZK: "Σ_AND.HVZK"
  using Σ_AND.HVZK_def hvzk challenge_space_def 
  apply(simp add: S_AND_def split_def)
  using Σ_prot1 Σ_prot0 Σ0.HVZK_unfold2 Σ1.HVZK_unfold2 valid_pub_AND_def by auto

lemma correct: 
  assumes Rel_AND: "((x0,x1), (w0,w1)) ∈ Rel_AND"
  and "e ∈ challenge_space" 
  shows "Σ_AND.completeness_game (x0,x1) (w0,w1) e = return_spmf True"
  including monad_normalisation
proof-
  have "Σ_AND.completeness_game (x0,x1) (w0,w1) e = do {
    ((r0,r1),(a0,a1)) ← init_AND (x0,x1) (w0,w1);
    (z0,z1) ← response_AND (r0,r1) (w0,w1) e;
    return_spmf (check_AND (x0,x1) (a0,a1) e (z0,z1))}" 
    by(simp add: Σ_AND.completeness_game_def split_def del: check_AND.simps)
  also have "... = do {
    (r0, a0) ← init0 x0 w0;
    z0 ← response0 r0 w0 e;
    (r1, a1) ← init1 x1 w1;
    z1 ← response1 r1 w1 e;
    return_spmf ((check0 x0 a0 e z0 ∧ check1 x1 a1 e z1))}" 
    apply(simp add: init_AND_def response_AND_def split_def)
    apply(rewrite bind_commute_spmf[of "response0 _ w0 e"])
    by simp
  ultimately show ?thesis
    using Σ1.complete_game_return_true Σ_prot1 Σ1.Σ_protocol_def Σ1.completeness_game_def assms
          Σ0.complete_game_return_true Σ_prot0 Σ0.Σ_protocol_def Σ0.completeness_game_def challenge_space_def
    apply(auto simp add: Let_def split_def bind_eq_return_spmf lossless_init lossless_response Rel_AND_def)
    by(metis (mono_tags, lifting) assms(2) fst_conv snd_conv)+
qed

lemma completeness: "Σ_AND.completeness"
  using Σ_AND.completeness_def correct challenge_space_def by force

lemma ss:
  assumes e_neq_e': "s ≠ s'"
    and valid_pub: "(x0,x1) ∈ valid_pub_AND"
    and challenge_space: "s ∈ challenge_space" "s' ∈ challenge_space"
    and "check_AND (x0,x1) (a0,a1) s (z0,z1)" 
    and "check_AND  (x0,x1) (a0,a1) s' (z0',z1')" 
  shows  "lossless_spmf (𝒜ss_AND  (x0,x1) ((a0,a1), s, (z0,z1)) ((a0,a1), s', (z0',z1'))) 
              ∧ (∀w'∈set_spmf (𝒜ss_AND  (x0,x1) ((a0,a1), s, (z0,z1)) ((a0,a1), s', (z0',z1'))). ((x0,x1), w') ∈ Rel_AND)"
proof-
  have x0_in_dom: "x0 ∈ valid_pub0" and x1_in_dom: "x1 ∈ valid_pub1" 
    using valid_pub valid_pub_AND_def by auto
  moreover have 3: "check0 x0 a0 s z0"
      using assms  by simp 
  moreover have 4: "check1 x1 a1 s' z1'"
    using assms by simp 
  moreover have "w0 ∈ set_spmf (𝒜ss0 x0 (a0, s, z0) (a0, s', z0')) ⟶ (x0,w0) ∈ Rel0" for w0
    using 3 4 Σ0.special_soundness_def Σ_prot0 Σ0.Σ_protocol_def x0_in_dom challenge_space_def assms valid_pub_AND_def valid_pub by fastforce
  moreover have "w1 ∈ set_spmf (𝒜ss1 x1 (a1, s, z1) (a1, s', z1')) ⟶ (x1,w1) ∈ Rel1" for w1
     using 3 4 Σ1.special_soundness_def Σ_prot1 Σ1.Σ_protocol_def x1_in_dom challenge_space_def assms valid_pub_AND_def valid_pub by fastforce 
  ultimately show ?thesis
    by(auto simp add: lossless_𝒜ss Rel_AND_def) 
qed

lemma special_soundness:
  shows "Σ_AND.special_soundness"
  using Σ_AND.special_soundness_def ss by fast

theorem Σ_protocol:
  shows "Σ_AND.Σ_protocol"
  by(auto simp add: Σ_AND.Σ_protocol_def completeness HVZK special_soundness)

sublocale AND_Σ_commit: Σ_protocols_to_commitments init_AND response_AND check_AND Rel_AND S_AND 𝒜ss_AND challenge_space valid_pub_AND G 
  apply unfold_locales
  by(auto simp add: Σ_protocol set_spmf_G_L lossless_G lossless_init_AND lossless_response_AND)

lemma "AND_Σ_commit.abstract_com.correct"
  using AND_Σ_commit.commit_correct by simp

lemma "AND_Σ_commit.abstract_com.perfect_hiding_ind_cpa 𝒜"
  using AND_Σ_commit.perfect_hiding by blast

lemma bind_advantage_bound_dis_log: 
  shows "AND_Σ_commit.abstract_com.bind_advantage 𝒜 ≤ AND_Σ_commit.rel_advantage (AND_Σ_commit.adversary 𝒜)"
  using AND_Σ_commit.bind_advantage by simp

end

end