Theory BatchKZG_knowledge_sound
theory BatchKZG_knowledge_sound
imports BatchKZG_eval_bind Algebraic_Group_Model
begin
section ‹Knowledge Soundness of the batched KZG›
text ‹In this theory we prove knowledge soundness for the KZG, concretely the knowledge soundness
as defined in the abstract polynomial commitment scheme. The proof is a reduction to the
evaluation binding game which has been reduced to the t-Bilinear strong Diffie-Hellman problem in the
BatchKZG\_eval\_bind theory.›
hide_const restrict
locale BatchEvalKZG_PCS_knowledge_sound = BatchEvalKZG_PCS_eval_bind
begin
text ‹the AGM adversary types that are useful in defining reductions (i.e. the reduction to the
evaluation binding game)›
lift_to_algebraicT "('a ck, 'a commit, 'state) knowledge_soundness_adversary1" "G⇩p"
=> AGM_knowledge_soundness_adversary1
lift_to_algebraicT "('state, 'a ck, 'e mod_ring, 'e evaluation, 'a witness) knowledge_soundness_adversary2"
"G⇩p" => AGM_knowledge_soundness_adversary2
text ‹We adapt the knowledge soundness adversary in round 2 to the batch version.
Concretely, we ask the adversary to give a single point $i \in I$ at which the evaluation polynomial
$r$ is distinct from the extractor polynomial›
type_synonym ('e', 'state', 'a') knowledge_soundness_adversary2_AGM
= "('a' ck × 'state') ⇒ ('e' mod_ring × 'e' argument set × ('e' batch_evaluation × ('a' witness × int list))) spmf"
text ‹The extractor is an algorithm that plays against the adversary. It is granted access to the
adversaries messages and state (which we neglect in this case as we do not need it because the
calculation vector is enough to create sensible values) and has to come up with a polynomial such
that the adversary cannot create valid opening points that are not part of the polynomial.›
type_synonym ('a', 'e') =
"('a' commit × int list) ⇒
('e' mod_ring poly × unit) spmf"
text ‹restrict for AGM adversaries 1 and 2›
interpretation AGM1: Algebraic_Algorithm G⇩p "listS G⇩p.groupS" "prodC G⇩p.groupC noConstrain"
by (unfold_locales)
text ‹‹'ck' ⇒ 'state' ⇒ ('argument' × ('evaluation' × 'witness')) spmf››
interpretation AGM2: Algebraic_Algorithm G⇩p "prodS (listS G⇩p.groupS) noSelect"
"prodC noConstrain (prodC noConstrain (prodC noConstrain G⇩p.groupC))"
by (unfold_locales)
definition knowledge_soundness_game_AGM :: "('state, 'a) AGM_knowledge_soundness_adversary1
⇒ ('e, 'state, 'a) knowledge_soundness_adversary2_AGM ⇒ ('a, 'e) extractor ⇒ bool spmf"
where "knowledge_soundness_game_AGM 𝒜1 𝒜2 ℰ = TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← AGM1.restrict 𝒜1 ck;
(p,td) ← ℰ (c,cvec);
(i, I, (r, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w') = Eval ck td p i;
return_spmf (verify_eval_batch vk c I (r,w) ∧ poly r i ≠ p_i
∧ valid_argument_batch I ∧ valid_eval_batch (r,w) ∧ i ∈ I)
} ELSE return_spmf False"
definition ks_to_eval_bind_reduction :: "('state, 'a) AGM_knowledge_soundness_adversary1
⇒ ('e, 'state, 'a) knowledge_soundness_adversary2_AGM ⇒ ('a, 'e) extractor
⇒ ('a, 'e) adversary" where
"ks_to_eval_bind_reduction 𝒜1 𝒜2 ℰ ck = do {
((c,cvec),σ) ← AGM1.restrict 𝒜1 ck;
(p,td) ← ℰ (c,cvec);
(i, I, (r_x, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w') = Eval ck td p i;
return_spmf (c,i, p_i, w', I, w, r_x)
}"
text ‹Extractor definition›
fun E :: "('a, 'e) extractor" where
"E (c,cvec) = return_spmf (Poly (map (of_int_mod_ring::int ⇒'e mod_ring) cvec),())"
lemma reduction_map_imp: "
let ck = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
vk = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
(p_i,w_i) = Eval ck td (Poly (map (of_int_mod_ring::int ⇒'e mod_ring) cvec)) i
in
length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ verify_eval_batch vk c I (r_x,w) ∧ poly r_x i ≠ p_i
∧ valid_argument_batch I ∧ valid_eval_batch (r_x,w) ∧ i ∈ I
⟶
length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ i ∈ I ∧ p_i ≠ poly r_x i
∧ valid_argument_batch I ∧ valid_eval (p_i, w_i) ∧ valid_eval_batch (r_x, w)
∧ verify_eval vk c i (p_i, w_i)
∧ verify_eval_batch vk c I (r_x,w)"
proof -
define ck where ck_def: "ck = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1]"
define vk where vk_def: "vk = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1]"
define p_i where p_i_def: "p_i = fst (Eval ck td (Poly (map (of_int_mod_ring::int ⇒'e mod_ring) cvec)) i )"
define w_i where w_i_def: "w_i = snd (Eval ck td (Poly (map (of_int_mod_ring::int ⇒'e mod_ring) cvec)) i )"
have "length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ verify_eval_batch vk c I (r_x,w) ∧ poly r_x i ≠ p_i
∧ valid_argument_batch I ∧ valid_eval_batch (r_x,w) ∧ i ∈ I
⟶
length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ i ∈ I ∧ p_i ≠ poly r_x i
∧ valid_argument_batch I ∧ valid_eval (p_i, w_i) ∧ valid_eval_batch (r_x, w)
∧ verify_eval vk c i (p_i, w_i)
∧ verify_eval_batch vk c I (r_x,w)"
(is "?lhs ⟶ ?rhs")
proof
assume asm: "?lhs"
show "?rhs"
proof(intro conjI)
from asm show "length ck = length cvec" by blast
from asm show "c = fold (λ(i::nat) acc::'a. acc ⊗ ck ! i [^] cvec ! i) [0..<length ck] 𝟭" by blast
from asm show "i ∈ I" by blast
from asm show " p_i ≠ poly r_x i" by blast
from asm show "valid_argument_batch I" by blast
from asm show "valid_eval_batch (r_x, w)" by blast
from asm show "verify_eval_batch vk c I (r_x, w)" by blast
show "valid_eval (p_i, w_i)"
proof -
have "g_pow_PK_Prod ck (ψ_of (Poly (map of_int_mod_ring cvec)) i)
= ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly (ψ_of (Poly (map of_int_mod_ring cvec)) i) α)"
unfolding ck_def
proof (rule g_pow_PK_Prod_correct)
show "degree (ψ_of (Poly (map of_int_mod_ring cvec)) i) ≤ max_deg"
proof (rule le_trans[OF degree_q_le_φ])
have "length (map of_int_mod_ring cvec) = max_deg +1"
using asm unfolding ck_def by force
moreover have "length (coeffs (Poly (map of_int_mod_ring cvec))) ≤ length (map of_int_mod_ring cvec)"
by (metis coeffs_Poly length_map length_strip_while_le)
ultimately show "degree (Poly (map of_int_mod_ring cvec)) ≤ max_deg"
using degree_eq_length_coeffs[of "Poly (map of_int_mod_ring cvec)"]
by (metis le_diff_conv)
qed
qed
then show ?thesis
unfolding valid_eval_def
by (simp add: Eval_def p_i_def w_i_def)
qed
show "verify_eval vk c i (p_i, w_i)"
proof -
let ?cvec = "(map of_int_mod_ring cvec::'e mod_ring list)"
have length_cvec: "length ?cvec = max_deg +1"
using asm unfolding ck_def by force
moreover have "length (coeffs (Poly ?cvec)) ≤ length ?cvec"
by (metis coeffs_Poly length_strip_while_le)
ultimately have deg_poly_calc_vec_le_max_deg: "degree (Poly ?cvec) ≤ max_deg"
using degree_eq_length_coeffs[of "Poly ?cvec"]
by (metis le_diff_conv)
have 1: "(g_pow_PK_Prod (map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1])
(ψ_of (Poly ?cvec) i))
= (❙g ^⇘G⇩p⇙ poly (ψ_of (Poly ?cvec) i) α)"
proof(rule g_pow_PK_Prod_correct)
show "degree (ψ_of (Poly ?cvec) i) ≤ max_deg"
by (rule le_trans[OF degree_q_le_φ])(fact deg_poly_calc_vec_le_max_deg)
qed
have 2: "map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1] ! 1 = ❙g ^⇘G⇩p⇙ α"
by (metis (no_types, lifting) One_nat_def add.commute d_pos diff_zero le_add_same_cancel1 le_zero_eq length_upt nth_map nth_upt plus_1_eq_Suc power_one_right zero_compare_simps(1))
have 3: "(❙g ^⇘G⇩p⇙ poly (Poly ?cvec) α) = c"
proof -
have "(❙g ^⇘G⇩p⇙ poly (Poly ?cvec) α)
= g_pow_PK_Prod (map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) (Poly ?cvec)"
by (rule g_pow_PK_Prod_correct[symmetric])(fact deg_poly_calc_vec_le_max_deg)
also have g_pow_to_fold: "… = fold (λi acc. acc ⊗⇘G⇩p⇙ (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^i)) ^⇘G⇩p⇙ (poly.coeff (Poly ?cvec) i))
[0..<Suc (degree (Poly ?cvec))] 𝟭⇘G⇩p⇙"
by (rule g_pow_PK_Prod_to_fold)(fact deg_poly_calc_vec_le_max_deg)
also have "…
=fold (λ i acc. acc ⊗⇘G⇩p⇙ (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^i)) ^⇘G⇩p⇙ (?cvec!i)) [0..<max_deg+1] 𝟭⇘G⇩p⇙"
proof -
have "fold (λi acc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ i) ^⇘G⇩p⇙ ?cvec ! i) [0..<max_deg + 1] 𝟭
= fold (λi acc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ i) ^⇘G⇩p⇙ ?cvec ! i)
([0..<Suc (degree (Poly ?cvec))] @ [Suc (degree (Poly ?cvec))..<max_deg + 1])
𝟭"
proof -
have "Suc (degree (Poly ?cvec)) ≤ max_deg +1"
by (simp add: deg_poly_calc_vec_le_max_deg)
then show ?thesis
by (metis (lifting) nat_le_iff_add upt_add_eq_append zero_order(1))
qed
also have "… = fold (λi acc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ i) ^⇘G⇩p⇙ ?cvec ! i)
[Suc (degree (Poly ?cvec))..<max_deg + 1]
(fold (λi acc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ i) ^⇘G⇩p⇙ ?cvec ! i)
[0..<Suc (degree (Poly ?cvec))] 𝟭)"
by fastforce
also have "… = fold (λi acc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ i) ^⇘G⇩p⇙ poly.coeff (Poly ?cvec) i)
[0..<Suc (degree (Poly ?cvec))]
𝟭"
proof -
have "fold (λi acc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ i) ^⇘G⇩p⇙ ?cvec ! i) [0..<Suc (degree (Poly ?cvec))] 𝟭
= fold (λi acc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ i) ^⇘G⇩p⇙ poly.coeff (Poly ?cvec) i) [0..<Suc (degree (Poly ?cvec))] 𝟭"
proof (rule List.fold_cong)
show " ⋀x. x ∈ set [0..<Suc (degree (Poly ?cvec))] ⟹
(λacc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ x) ^⇘G⇩p⇙ ?cvec ! x) =
(λacc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ x) ^⇘G⇩p⇙ poly.coeff (Poly ?cvec) x)"
proof
fix x::nat
fix acc::'a
assume asm: "x ∈ set [0..<Suc (degree (Poly ?cvec))]"
then have "?cvec ! x = poly.coeff (Poly ?cvec) x"
by (metis ‹length ?cvec = max_deg + 1› atLeastLessThan_iff coeff_Poly deg_poly_calc_vec_le_max_deg dual_order.trans less_Suc_eq_le nth_default_nth semiring_norm(174) set_upt)
then show "acc ⊗ (❙g ^⇘G⇩p⇙ α ^ x) ^⇘G⇩p⇙ ?cvec ! x = acc ⊗ (❙g ^⇘G⇩p⇙ α ^ x) ^⇘G⇩p⇙ poly.coeff (Poly ?cvec) x "
by presburger
qed
qed simp+
moreover have "∀init ∈ carrier G⇩p.
fold (λi acc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ i) ^⇘G⇩p⇙ ?cvec ! i)
[Suc (degree (Poly ?cvec))..<max_deg + 1]
init
= init"
proof
fix init ::'a
assume init_in_carrier: "init ∈ carrier G⇩p"
have "fold (λi acc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ i) ^⇘G⇩p⇙ ?cvec ! i)
[Suc (degree (Poly ?cvec))..<max_deg + 1]
init = fold (λi acc. acc ⊗ 𝟭)
[Suc (degree (Poly ?cvec))..<max_deg + 1]
init"
proof (rule List.fold_cong)
show " ⋀x. x ∈ set [Suc (degree (Poly ?cvec))..<max_deg + 1] ⟹
(λacc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ x) ^⇘G⇩p⇙ ?cvec ! x) = (λacc. acc ⊗ 𝟭)"
proof
fix x::nat
fix acc ::'a
assume asm: "x ∈ set [Suc (degree (Poly ?cvec))..<max_deg + 1]"
show "acc ⊗ (❙g ^⇘G⇩p⇙ α ^ x) ^⇘G⇩p⇙ ?cvec ! x = acc ⊗ 𝟭"
proof -
have " ?cvec ! x = 0" using asm length_cvec
by (smt (verit) add.commute coeff_Poly_eq in_set_conv_nth le_degree length_upt less_diff_conv not_less_eq_eq nth_default_eq_dflt_iff nth_upt order.refl trans_le_add2)
then have "(❙g ^⇘G⇩p⇙ α ^ x) ^⇘G⇩p⇙ ?cvec ! x = 𝟭" by simp
then show ?thesis by argo
qed
qed
qed simp+
also have "… = init"
proof (induction max_deg)
case 0
then show ?case by fastforce
next
case (Suc max_deg)
have "fold (λi acc. acc ⊗ 𝟭) [Suc (degree (Poly ?cvec))..<Suc max_deg + 1] init
= fold (λi acc. acc ⊗ 𝟭) ([Suc (degree (Poly ?cvec))..<max_deg + 1] @ [Suc max_deg]) init"
by (simp add: init_in_carrier)
also have "… = fold (λi acc. acc ⊗ 𝟭) [Suc max_deg] (fold (λi acc. acc ⊗ 𝟭) [Suc (degree (Poly ?cvec))..<max_deg + 1] init)"
by force
also have "… = fold (λi acc. acc ⊗ 𝟭) [Suc max_deg] init" using Suc.IH by argo
also have "… = init ⊗ 𝟭" by force
also have "… = init" by (simp add: init_in_carrier)
finally show ?case .
qed
finally show "fold (λi acc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ i) ^⇘G⇩p⇙ ?cvec ! i)
[Suc (degree (Poly ?cvec))..<max_deg + 1]
init
= init" .
qed
ultimately show ?thesis
by (metis (no_types, lifting) G⇩p.generator_closed G⇩p.int_pow_closed ‹❙g ^⇘G⇩p⇙ poly (Poly ?cvec) α = g_pow_PK_Prod (map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) (Poly ?cvec)› g_pow_to_fold)
qed
finally show ?thesis by presburger
qed
also have "…
=fold (λ i acc. acc ⊗⇘G⇩p⇙ (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1])!i ^⇘G⇩p⇙ (?cvec!i)) [0..<max_deg+1] 𝟭⇘G⇩p⇙"
proof(rule List.fold_cong)
show "𝟭 = 𝟭" by simp
show "[0..<max_deg + 1] = [0..<max_deg + 1]" by simp
show "⋀x. x ∈ set [0..<max_deg + 1] ⟹
(λacc. acc ⊗ (❙g ^⇘G⇩p⇙ α ^ x) ^⇘G⇩p⇙ ?cvec ! x) =
(λacc. acc ⊗ map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1] ! x ^⇘G⇩p⇙ ?cvec ! x)"
proof
fix x::nat
fix acc :: 'a
assume asm: "x ∈ set [0..<max_deg + 1]"
show " acc ⊗ (❙g ^⇘G⇩p⇙ α ^ x) ^⇘G⇩p⇙ ?cvec ! x
= acc ⊗ map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1] ! x ^⇘G⇩p⇙ ?cvec ! x"
using PK_i[symmetric] asm
by (metis Suc_eq_plus1 atLeastLessThan_iff less_Suc_eq_le set_upt)
qed
qed
also have "…
=fold (λ i acc. acc ⊗⇘G⇩p⇙ (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1])!i ^⇘G⇩p⇙ (of_int_mod_ring (cvec!i))) [0..<max_deg+1] 𝟭⇘G⇩p⇙"
proof(rule List.fold_cong)
fix x
assume "x ∈ set [0..<max_deg + 1]"
then have "x < length cvec"
using asm unfolding ck_def
by fastforce
then show "(λacc. acc ⊗ map (λt. ❙g ^ α ^ t) [0..<max_deg + 1] ! x ^ map of_int_mod_ring cvec ! x) =
(λacc. acc ⊗ map (λt. ❙g ^ α ^ t) [0..<max_deg + 1] ! x ^ of_int_mod_ring (cvec ! x))"
by force
qed simp+
also have "… = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭"
proof -
have length_eq_max_deg: "length (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1]) = max_deg +1"
by force
have mod_ring_trnsf_eq_plain: "⋀g x. g ∈ carrier G⇩p ⟹ g [^]⇘G⇩p⇙ (to_int_mod_ring (of_int_mod_ring x::'e mod_ring)) = g [^]⇘G⇩p⇙ x"
proof -
fix g x
assume g_in_carrier: "g ∈ carrier G⇩p"
have mod_red: "to_int_mod_ring (of_int_mod_ring x::'e mod_ring) = x mod p"
unfolding of_int_mod_ring_def to_int_mod_ring_def
by (metis CARD_q of_int_mod_ring.rep_eq of_int_mod_ring_def to_int_mod_ring.rep_eq to_int_mod_ring_def)
then show "g [^]⇘G⇩p⇙ (to_int_mod_ring (of_int_mod_ring x::'e mod_ring)) = g [^]⇘G⇩p⇙ x"
using carrier_pow_mod_order_G⇩p g_in_carrier mod_red by metis
qed
show ?thesis
proof(rule List.fold_cong)
fix x
assume "x ∈ set [0..<max_deg + 1]"
then show "(λacc. acc ⊗ map (λt. ❙g ^ α ^ t) [0..<max_deg + 1] ! x ^ of_int_mod_ring (cvec ! x)) = (λacc. acc ⊗ ck ! x [^] cvec ! x)"
unfolding ck_def length_eq_max_deg using mod_ring_trnsf_eq_plain
by (metis (no_types, lifting) G⇩p.generator_closed G⇩p.int_pow_closed atLeastLessThan_iff length_upt nth_map set_upt verit_minus_simplify(2))
qed (simp add: ck_def)+
qed
also have "… = c"
using asm unfolding ck_def by fast
finally show ?thesis .
qed
show ?thesis
unfolding verify_eval_def Eval_def Let_def split_def g_pow_PK_Prod_correct
using eq_on_e[of "(Poly ?cvec)" i α]
by (metis "1" "2" 3 Eval_def ck_def vk_def p_i_def w_i_def eq_on_e fst_conv snd_conv)
qed
qed
qed
then show ?thesis
unfolding ck_def vk_def p_i_def w_i_def Let_def split_def
by blast
qed
theorem ks_game_to_eval_bind_game: "spmf (knowledge_soundness_game_AGM 𝒜1 𝒜2 E) True
≤ spmf (bind_game (ks_to_eval_bind_reduction 𝒜1 𝒜2 E)) True"
(is "?lhs ≤ ?rhs")
proof -
note [simp] = Let_def split_def
have "spmf (knowledge_soundness_game_AGM 𝒜1 𝒜2 E) True = spmf (TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← 𝒜1 ck;
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭);
(p,td) ← E (c,cvec);
(i, I, (r, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w') = Eval ck td p i;
return_spmf (verify_eval_batch vk c I (r,w) ∧ poly r i ≠ p_i
∧ valid_argument_batch I ∧ valid_eval_batch (r,w) ∧ i ∈ I)
} ELSE return_spmf False) True"
unfolding knowledge_soundness_game_AGM_def AGM1.restrict_def listS_def G⇩p.groupS_def noSelect_def
Restrictive_Comp.restrict_def prodC_def G⇩p.groupC_def G⇩p.constrain_grp_def
noConstrain_def
by force
also have "…= spmf (TRY do {
(ck,vk) ← key_gen;
TRY do {
((c,cvec),σ) ← 𝒜1 ck;
TRY do {
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭);
TRY do {
(p,td) ← E (c,cvec);
TRY do {
(i, I, (r, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w') = Eval ck td p i;
TRY do {
return_spmf (verify_eval_batch vk c I (r,w) ∧ poly r i ≠ p_i
∧ valid_argument_batch I ∧ valid_eval_batch (r,w) ∧ i ∈ I)
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False) True"
unfolding Let_def split_def
by (fold try_bind_spmf_lossless2[OF lossless_return_spmf])simp
also have "…= spmf (TRY do {
(ck,vk) ← key_gen;
TRY do {
((c,cvec),σ) ← 𝒜1 ck;
TRY do {
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭);
TRY do {
(p,td) ← E (c,cvec);
TRY do {
(i, I, (r, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w') = Eval ck td p i;
TRY do {
_ :: unit ← assert_spmf (verify_eval_batch vk c I (r,w) ∧ poly r i ≠ p_i
∧ valid_argument_batch I ∧ valid_eval_batch (r,w) ∧ i ∈ I);
return_spmf True
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False) True"
by (rule spmf_eqI')(auto simp add: try_bind_assert_spmf try_spmf_return_spmf1 intro!: try_spmf_cong bind_spmf_cong)
also have "…= spmf (TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← 𝒜1 ck;
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭);
(p,td) ← E (c,cvec);
(i, I, (r, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w') = Eval ck td p i;
_ :: unit ← assert_spmf (verify_eval_batch vk c I (r,w) ∧ poly r i ≠ p_i
∧ valid_argument_batch I ∧ valid_eval_batch (r,w) ∧ i ∈ I);
return_spmf True
} ELSE return_spmf False) True"
unfolding Let_def split_def
by (fold try_bind_spmf_lossless2[OF lossless_return_spmf])simp
also have "…= spmf(TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, I, (r, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w') = Eval ck td p i;
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭);
_ :: unit ← assert_spmf (verify_eval_batch vk c I (r,w) ∧ poly r i ≠ p_i
∧ valid_argument_batch I ∧ valid_eval_batch (r,w) ∧ i ∈ I);
return_spmf True
} ELSE return_spmf False) True"
apply (rule spmf_eqI')
apply (rule try_spmf_cong)
apply (rule unpack_bind_spmf'; simp)+
apply (subst assert_commute)
apply simp+
done
also have "…= spmf (TRY do {
x :: nat ← sample_uniform (order G⇩p);
let (α::'e mod_ring) = of_int_mod_ring (int x);
let ck = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
let vk = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
((c,cvec),σ) ← 𝒜1 ck;
let (p,td) = (Poly (map (of_int_mod_ring::int ⇒'e mod_ring) cvec),());
(i, I, (r_x, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w') = Eval ck td p i;
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ verify_eval_batch vk c I (r_x,w) ∧ poly r_x i ≠ p_i
∧ valid_argument_batch I ∧ valid_eval_batch (r_x,w) ∧ i ∈ I);
return_spmf True
} ELSE return_spmf False) True"
by (simp add: key_gen_def Setup_def assert_collapse)
also have "…≤ spmf (TRY do {
x :: nat ← sample_uniform (order G⇩p);
let (α::'e mod_ring) = of_int_mod_ring (int x);
let ck = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
let vk = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
((c,cvec),σ) ← 𝒜1 ck;
let (p,td) = (Poly (map (of_int_mod_ring::int ⇒'e mod_ring) cvec),());
(i, I, (r_x, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w_i) = Eval ck td p i;
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ i ∈ I ∧ p_i ≠ poly r_x i
∧ valid_argument_batch I ∧ valid_eval (p_i, w_i) ∧ valid_eval_batch (r_x, w)
∧ verify_eval vk c i (p_i, w_i)
∧ verify_eval_batch vk c I (r_x,w));
return_spmf True
} ELSE return_spmf False) True"
unfolding E.simps key_gen_def Setup_def
apply (rule try_spmf_le)
apply (unfold Let_def split_def)
apply (rule bind_spmf_le)+
apply (rule assert_imp)
apply (insert reduction_map_imp)
apply (unfold Let_def split_def)
apply (intro impI)
apply simp
apply force
done
also have "…= spmf (TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, I, (r_x, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w_i) = Eval ck td p i;
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ i ∈ I ∧ p_i ≠ poly r_x i
∧ valid_argument_batch I ∧ valid_eval (p_i, w_i) ∧ valid_eval_batch (r_x, w)
∧ verify_eval vk c i (p_i, w_i)
∧ verify_eval_batch vk c I (r_x,w));
return_spmf True
} ELSE return_spmf False) True"
by (simp add: key_gen_def Setup_def assert_collapse)
also have "…= spmf (TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, I, (r_x, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w_i) = Eval ck td p i;
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ i ∈ I ∧ p_i ≠ poly r_x i
∧ valid_argument_batch I ∧ valid_eval (p_i, w_i) ∧ valid_eval_batch (r_x, w));
_::unit ← assert_spmf (verify_eval vk c i (p_i, w_i)
∧ verify_eval_batch vk c I (r_x,w));
return_spmf True
} ELSE return_spmf False) True"
by (simp add: assert_collapse)
also have "…= spmf (TRY do {
(ck,vk) ← key_gen;
TRY do {
((c,cvec),σ) ← 𝒜1 ck;
TRY do {
(p,td) ← E (c,cvec);
TRY do{
(i, I, (r_x, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
TRY do{
let (p_i,w_i) = Eval ck td p i;
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ i ∈ I ∧ p_i ≠ poly r_x i
∧ valid_argument_batch I ∧ valid_eval (p_i, w_i) ∧ valid_eval_batch (r_x, w));
TRY do {
_::unit ← assert_spmf (verify_eval vk c i (p_i, w_i)
∧ verify_eval_batch vk c I (r_x,w));
return_spmf True
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False) True"
unfolding Let_def split_def
by (fold try_bind_spmf_lossless2[OF lossless_return_spmf])simp
also have "…= spmf (TRY do {
(ck,vk) ← key_gen;
TRY do {
((c,cvec),σ) ← 𝒜1 ck;
TRY do {
(p,td) ← E (c,cvec);
TRY do{
(i, I, (r_x, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
TRY do{
let (p_i,w_i) = Eval ck td p i;
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ i ∈ I ∧ p_i ≠ poly r_x i
∧ valid_argument_batch I ∧ valid_eval (p_i, w_i) ∧ valid_eval_batch (r_x, w));
TRY do {
return_spmf (verify_eval vk c i (p_i, w_i)
∧ verify_eval_batch vk c I (r_x,w))
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False) True"
by (rule spmf_eqI')(auto simp add: try_bind_assert_spmf try_spmf_return_spmf1 intro!: try_spmf_cong bind_spmf_cong)
also have "…= spmf (TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, I, (r_x, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w_i) = Eval ck td p i;
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ i ∈ I ∧ p_i ≠ poly r_x i
∧ valid_argument_batch I ∧ valid_eval (p_i, w_i) ∧ valid_eval_batch (r_x, w));
return_spmf (verify_eval vk c i (p_i, w_i)
∧ verify_eval_batch vk c I (r_x,w))
} ELSE return_spmf False) True"
unfolding Let_def split_def
by (fold try_bind_spmf_lossless2[OF lossless_return_spmf])simp
also have "…= spmf (TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, I, (r_x, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w_i) = Eval ck td p i;
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭 );
_ :: unit ← assert_spmf (i ∈ I ∧ p_i ≠ poly r_x i
∧ valid_argument_batch I ∧ valid_eval (p_i, w_i) ∧ valid_eval_batch (r_x, w));
return_spmf (verify_eval vk c i (p_i, w_i)
∧ verify_eval_batch vk c I (r_x,w))
} ELSE return_spmf False) True"
by (simp add: assert_collapse)
also have "…= spmf (TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← 𝒜1 ck;
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭 );
(p,td) ← E (c,cvec);
(i, I, (r_x, (w, wvec))) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i,w_i) = Eval ck td p i;
_ :: unit ← assert_spmf (i ∈ I ∧ p_i ≠ poly r_x i
∧ valid_argument_batch I ∧ valid_eval (p_i, w_i) ∧ valid_eval_batch (r_x, w));
return_spmf (verify_eval vk c i (p_i, w_i)
∧ verify_eval_batch vk c I (r_x,w))
} ELSE return_spmf False) True"
apply (rule spmf_eqI')
apply (unfold Let_def split_def)
apply (simp split: prod.split)
apply (rule unpack_try_spmf)
apply (rule unpack_bind_spmf'; rule ext)+
apply (subst assert_commute)
apply (subst assert_commute)
apply blast
done
also have "… ≤ spmf (bind_game (ks_to_eval_bind_reduction 𝒜1 𝒜2 E)) True"
unfolding bind_game_def ks_to_eval_bind_reduction_def
unfolding knowledge_soundness_game_AGM_def AGM1.restrict_def listS_def G⇩p.groupS_def noSelect_def
Restrictive_Comp.restrict_def prodC_def G⇩p.groupC_def G⇩p.constrain_grp_def
noConstrain_def split_def Let_def
by force
finally show ?thesis .
qed
text ‹Finally we put everything together:
we conclude that for every efficient adversary in the AGM the advantage of winning the
knowledge soundness game is less equal to breaking the t-BSDH assumption.›
theorem knowledge_soundness:
"spmf (knowledge_soundness_game_AGM 𝒜1 𝒜2 E) True
≤ t_BSDH.advantage (reduction (ks_to_eval_bind_reduction 𝒜1 𝒜2 E))"
using ks_game_to_eval_bind_game
using evaluation_binding[of "ks_to_eval_bind_reduction 𝒜1 𝒜2 E"]
unfolding bind_advantage_def
using landau_o.R_trans by blast
end
end