Theory KZG_knowledge_sound
theory KZG_knowledge_sound
imports KZG_eval_bind Algebraic_Group_Model
begin
section ‹Knowledge Soundness of the 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-strong Diffie-Hellman problem in the
KZG\_eval\_bind theory.›
hide_const restrict
locale KZG_PCS_knowledge_sound = KZG_PCS_binding
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
type_synonym ('e', 'state', 'a') knowledge_soundness_adversary2_AGM
= "('a' ck × 'state') ⇒ ('e' argument × ('e' 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›
text ‹realized by the following two interpretations:›
interpretation AGM1: Algebraic_Algorithm G⇩p "listS G⇩p.groupS" "prodC G⇩p.groupC noConstrain"
by (unfold_locales)
interpretation AGM2: Algebraic_Algorithm G⇩p "prodS (listS G⇩p.groupS) noSelect"
"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, p_i, w, wvec) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i',w') = Eval ck td p i;
return_spmf (verify_eval vk c i (p_i,w) ∧ p_i ≠ p_i' ∧ valid_argument i ∧ valid_eval (p_i,w))
} ELSE return_spmf False"
text ‹reduction to the evaluation bind game
The main idea is that if the adversary can break knowledge soundness, i.e. give an
evaluation (+ proof) that differs from the evaluation of the polynomial provided by the extractor,
the evaluation of the polynomial provided by the extractor will still yield a valid evaluation
(+ proof). Hence, one obtains two distinct valid evaluations of the same value, thus breaking
evaluation binding.›
definition knowledge_soundness_reduction
:: "('a, 'e) extractor ⇒ ('state, 'a) AGM_knowledge_soundness_adversary1
⇒ ('e, 'state, 'a) knowledge_soundness_adversary2_AGM
⇒ ('a ck, 'a commit, 'e argument, 'e evaluation, 'a witness) eval_bind_adversary"
where
"knowledge_soundness_reduction ℰ 𝒜1 𝒜2 ck = do {
((c,cvec),σ) ← AGM1.restrict 𝒜1 ck;
(p,td) ← ℰ (c,cvec);
(i, p_i, w, wvec) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i',w') = Eval ck td p i;
return_spmf (c, i, p_i, w, p_i', w')}"
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),())"
subsection ‹Helping definitions›
text ‹The knowledge soundness reduction adversary extended for asserts that
are present in the evaluation binding game. We use this definition to show equivalence to
the evaluation binding game. Later on we can then easily over-estimate the probability from
this extended version to the normal reduction.›
definition knowledge_soundness_reduction_ext
:: "('a, 'e) extractor ⇒ ('state, 'a) AGM_knowledge_soundness_adversary1
⇒ ('e, 'state, 'a) knowledge_soundness_adversary2_AGM
⇒ ('a ck, 'a commit, 'e argument, 'e evaluation, 'a witness) eval_bind_adversary"
where
"knowledge_soundness_reduction_ext ℰ 𝒜1 𝒜2 ck = do {
((c,cvec),σ) ← AGM1.restrict 𝒜1 ck;
(p,td) ← ℰ (c,cvec);
(i, p_i, w, wvec) ← AGM2.restrict 𝒜2 (ck,σ);
_ :: unit ← assert_spmf (valid_eval (p_i, w));
let (p_i',w') = Eval ck td p i;
return_spmf (c, i, p_i, w, p_i', w')}"
subsection ‹Helping lemmas›
text ‹proof related helping lemmas›
lemma ks_imp_eval_bind_asserts:
" 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') = Eval ck td (Poly (map of_int_mod_ring cvec)) i
in
length ck = length (cvec::int list)
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ verify_eval vk c i (p_i,w)
∧ p_i ≠ p_i'
∧ valid_argument i
∧ valid_eval (p_i,w)
⟷
length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ p_i ≠ p_i'
∧ valid_argument i
∧ valid_eval (p_i,w)
∧ valid_eval (p_i', w')
∧ verify_eval vk c i (p_i, w)
∧ verify_eval vk c i (p_i', 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 cvec)) i)"
define w' where w'_def: "w' = snd (Eval ck td (Poly (map of_int_mod_ring cvec)) i)"
have " length ck = length (cvec::int list)
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ verify_eval vk c i (p_i,w)
∧ p_i ≠ p_i'
∧ valid_argument i
∧ valid_eval (p_i,w)
⟷
length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭
∧ p_i ≠ p_i'
∧ valid_argument i
∧ valid_eval (p_i,w)
∧ valid_eval (p_i', w')
∧ verify_eval vk c i (p_i, w)
∧ verify_eval vk c i (p_i', w')"
(is "?lhs ⟷ ?rhs")
proof
assume asm: "?lhs"
show "?rhs"
proof(intro conjI)
from asm show valid_eval_adv: "valid_eval (p_i, w)" by force
from asm show "verify_eval vk c i (p_i, w)" by force
show valid_eval_gen: "valid_eval (p_i', w')"
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'_def)
qed
show verify_eval_gen: "verify_eval vk c i (p_i', w')"
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 coeffs_Poly le_diff_conv length_strip_while_le)
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'_def eq_on_e fst_conv snd_conv)
qed
qed (force simp add: asm)+
next
assume asm: "?rhs"
show "?lhs"
proof(intro conjI)
from asm show "valid_eval (p_i, w)" by force
from asm show "verify_eval vk c i (p_i, w)" by force
qed (simp add: asm)+
qed
then show ?thesis
unfolding ck_def vk_def p_i'_def w'_def Let_def split_def by fast
qed
lemma knowledge_soundness_game_alt_def:
"knowledge_soundness_game_AGM 𝒜1 𝒜2 E =
eval_bind_game (knowledge_soundness_reduction_ext E 𝒜1 𝒜2)"
proof -
note [simp] = Let_def split_def
have "knowledge_soundness_game_AGM 𝒜1 𝒜2 E =
TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← AGM1.restrict 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, p_i, w, wvec) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i',w') = Eval ck td p i;
return_spmf (verify_eval vk c i (p_i,w) ∧ p_i ≠ p_i' ∧ valid_argument i ∧ valid_eval (p_i,w))
} ELSE return_spmf False"
by (simp add: knowledge_soundness_game_AGM_def del: Let_def split_def)
also have "… =
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, p_i, (w, wvec)) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i',w') = Eval ck td p i;
return_spmf (verify_eval vk c i (p_i,w) ∧ p_i ≠ p_i' ∧ valid_argument i ∧ valid_eval (p_i,w))
} ELSE return_spmf False"
unfolding 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 Let_def split_def
by simp
also have "… =
TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, p_i, (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] 𝟭);
return_spmf (verify_eval vk c i (p_i,w) ∧ p_i ≠ p_i' ∧ valid_argument i ∧ valid_eval (p_i,w))
} ELSE return_spmf False"
by (rule try_spmf_cong)(simp add: assert_commute)+
also have "… =
TRY do {
(ck,vk) ← key_gen;
TRY do {
((c,cvec),σ) ← 𝒜1 ck;
TRY do {
(p,td) ← E (c,cvec);
TRY do {
(i, p_i, (w, wvec)) ← AGM2.restrict 𝒜2 (ck,σ);
TRY do {
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] 𝟭);
TRY do {
return_spmf (verify_eval vk c i (p_i,w) ∧ p_i ≠ p_i' ∧ valid_argument i ∧ valid_eval (p_i,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"
unfolding Let_def split_def
by (fold try_bind_spmf_lossless2[OF lossless_return_spmf])simp
also have "… =
TRY do {
(ck,vk) ← key_gen;
TRY do {
((c,cvec),σ) ← 𝒜1 ck;
TRY do {
(p,td) ← E (c,cvec);
TRY do {
(i, p_i, (w, wvec)) ← AGM2.restrict 𝒜2 (ck,σ);
TRY do {
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 vk c i (p_i,w) ∧ p_i ≠ p_i' ∧ valid_argument i ∧ valid_eval (p_i,w));
return_spmf True
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False"
by(auto simp add: try_bind_assert_spmf try_spmf_return_spmf1 intro!: try_spmf_cong bind_spmf_cong)
also have "… =
TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, p_i, (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 vk c i (p_i,w) ∧ p_i ≠ p_i' ∧ valid_argument i ∧ valid_eval (p_i,w));
return_spmf True
} ELSE return_spmf False"
unfolding Let_def split_def
by (fold try_bind_spmf_lossless2[OF lossless_return_spmf])simp
also have "… =
TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, p_i, (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 vk c i (p_i,w)
∧ p_i ≠ p_i'
∧ valid_argument i
∧ valid_eval (p_i,w));
return_spmf True
} ELSE return_spmf False"
by (simp add: assert_collapse)
also have "… = 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, p_i, (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 vk c i (p_i,w)
∧ p_i ≠ p_i'
∧ valid_argument i
∧ valid_eval (p_i,w));
return_spmf True
} ELSE return_spmf False"
unfolding key_gen_def Setup_def by auto
also have "… =
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, p_i, (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] 𝟭
∧ p_i ≠ p_i'
∧ valid_argument i
∧ valid_eval (p_i,w)
∧ valid_eval (p_i', w')
∧ verify_eval vk c i (p_i, w)
∧ verify_eval vk c i (p_i', w'));
return_spmf True
} ELSE return_spmf False"
apply(unfold spmf_rel_eq[symmetric])
apply (rule rel_spmf_try_spmf)
apply(unfold Let_def split_def)
apply(rule rel_spmf_bindI[of "(=)"] | force)+
apply(rule assert_cong)
apply(insert ks_imp_eval_bind_asserts)
apply(unfold Let_def split_def)
apply simp+
done
also have "… =
TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, p_i, (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] 𝟭
∧ p_i ≠ p_i'
∧ valid_argument i
∧ valid_eval (p_i,w)
∧ valid_eval (p_i', w')
∧ verify_eval vk c i (p_i, w)
∧ verify_eval vk c i (p_i', w'));
return_spmf True
} ELSE return_spmf False"
unfolding key_gen_def Setup_def by force
also have "… =
TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, p_i, (w, wvec)) ← AGM2.restrict 𝒜2 (ck,σ);
_ :: unit ← assert_spmf (length ck = length cvec
∧ c = fold (λ i acc. acc ⊗ ck!i [^] (cvec!i)) [0..<length ck] 𝟭);
let (p_i',w') = Eval ck td p i;
_ :: unit ← assert_spmf (
p_i ≠ p_i'
∧ valid_argument i
∧ valid_eval (p_i,w)
∧ valid_eval (p_i', w')
∧ verify_eval vk c i (p_i, w)
∧ verify_eval vk c i (p_i', w'));
return_spmf True
} ELSE return_spmf False"
by (simp add: assert_collapse)
also have "… =
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, p_i, (w, wvec)) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i',w') = Eval ck td p i;
_ :: unit ← assert_spmf (
p_i ≠ p_i'
∧ valid_argument i
∧ valid_eval (p_i,w)
∧ valid_eval (p_i', w')
∧ verify_eval vk c i (p_i, w)
∧ verify_eval vk c i (p_i', w'));
return_spmf True
} ELSE return_spmf False"
apply (rule try_spmf_cong)
apply simp
apply(subst assert_commute)
apply blast+
done
also have "… =
TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← AGM1.restrict 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, p_i, (w, wvec)) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i',w') = Eval ck td p i;
_ :: unit ← assert_spmf (
p_i ≠ p_i'
∧ valid_argument i
∧ valid_eval (p_i,w)
∧ valid_eval (p_i', w')
∧ verify_eval vk c i (p_i, w)
∧ verify_eval vk c i (p_i', w'));
return_spmf True
} ELSE return_spmf False"
unfolding 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 Let_def split_def
by fastforce
also have "… =
TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← AGM1.restrict 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, p_i, (w, wvec)) ← AGM2.restrict 𝒜2 (ck,σ);
let (p_i',w') = Eval ck td p i;
_ :: unit ← assert_spmf (
valid_eval (p_i,w)
∧ p_i ≠ p_i'
∧ valid_argument i
∧ valid_eval (p_i,w)
∧ valid_eval (p_i', w')
∧ verify_eval vk c i (p_i, w)
∧ verify_eval vk c i (p_i', w'));
return_spmf True
} ELSE return_spmf False"
apply(unfold spmf_rel_eq[symmetric])
apply (rule rel_spmf_try_spmf)
apply(unfold Let_def split_def)
apply(rule rel_spmf_bindI[of "(=)"] | force)+
apply(rule assert_cong)
apply force+
done
also have "… =
TRY do {
(ck,vk) ← key_gen;
((c,cvec),σ) ← AGM1.restrict 𝒜1 ck;
(p,td) ← E (c,cvec);
(i, p_i, (w, wvec)) ← AGM2.restrict 𝒜2 (ck,σ);
_ :: unit ← assert_spmf ( valid_eval (p_i,w));
let (p_i',w') = Eval ck td p i;
_ :: unit ← assert_spmf (
p_i ≠ p_i'
∧ valid_argument i
∧ valid_eval (p_i,w)
∧ valid_eval (p_i', w'));
_ :: unit ← assert_spmf(
verify_eval vk c i (p_i, w)
∧ verify_eval vk c i (p_i', w'));
return_spmf True
} ELSE return_spmf False"
by (simp add: assert_collapse)
also have "… =
TRY do {
(ck,vk) ← key_gen;
(c, i, v, w, v', w') ← knowledge_soundness_reduction_ext E 𝒜1 𝒜2 ck;
_ :: unit ← assert_spmf (
v ≠ v'
∧ valid_argument i
∧ valid_eval (v,w)
∧ valid_eval (v', w'));
_ :: unit ← assert_spmf(
verify_eval vk c i (v, w)
∧ verify_eval vk c i (v', w'));
return_spmf True
} ELSE return_spmf False"
unfolding knowledge_soundness_reduction_ext_def by force
also have "… =
TRY do {
(ck,vk) ← key_gen;
TRY do {
(c, i, v, w, v', w') ← knowledge_soundness_reduction_ext E 𝒜1 𝒜2 ck;
TRY do {
_ :: unit ← assert_spmf (
v ≠ v'
∧ valid_argument i
∧ valid_eval (v,w)
∧ valid_eval (v', w'));
TRY do {
_ :: unit ← assert_spmf(
verify_eval vk c i (v, w)
∧ verify_eval vk c i (v', w'));
return_spmf True
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False"
unfolding Let_def split_def
by (fold try_bind_spmf_lossless2[OF lossless_return_spmf])simp
also have "… =
TRY do {
(ck,vk) ← key_gen;
TRY do {
(c, i, v, w, v', w') ← knowledge_soundness_reduction_ext E 𝒜1 𝒜2 ck;
TRY do {
_ :: unit ← assert_spmf (
v ≠ v'
∧ valid_argument i
∧ valid_eval (v,w)
∧ valid_eval (v', w'));
TRY do {
return_spmf (verify_eval vk c i (v, w) ∧ verify_eval vk c i (v', w'))
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False"
by(auto simp add: try_bind_assert_spmf try_spmf_return_spmf1 intro!: try_spmf_cong bind_spmf_cong)
also have "… =
TRY do {
(ck,vk) ← key_gen;
(c, i, v, w, v', w') ← knowledge_soundness_reduction_ext E 𝒜1 𝒜2 ck;
_ :: unit ← assert_spmf (
v ≠ v'
∧ valid_argument i
∧ valid_eval (v,w)
∧ valid_eval (v', w'));
return_spmf( verify_eval vk c i (v, w) ∧ verify_eval vk c i (v', w'))
} ELSE return_spmf False"
unfolding Let_def split_def
by (fold try_bind_spmf_lossless2[OF lossless_return_spmf])simp
also have "… = eval_bind_game (knowledge_soundness_reduction_ext E 𝒜1 𝒜2)"
unfolding eval_bind_game_def by presburger
finally show ?thesis .
qed
text ‹We overestimate the probability of winning the evaluation binding game with the extended adversary
by winning it with the normal adversary.›
lemma overestimate_reductions: "spmf (eval_bind_game (knowledge_soundness_reduction_ext E 𝒜 𝒜')) True
≤ spmf (eval_bind_game (knowledge_soundness_reduction E 𝒜 𝒜')) True"
proof -
note [simp] = Let_def split_def
text ‹We extend the evaluation binding game with the extended reduction adversary to a complete
game.›
have w_assert_ext: "eval_bind_game (knowledge_soundness_reduction_ext E 𝒜 𝒜') =
TRY do {
(ck, vk) ← key_gen;
((c,cvec),σ) ← AGM1.restrict 𝒜 ck;
(p,td) ← E (c,cvec);
(i, v, (w, wvec)) ← AGM2.restrict 𝒜' (ck,σ);
_ :: unit ← assert_spmf (valid_eval (v, w));
let (v',w') = Eval ck td p i;
_ :: unit ← assert_spmf (v ≠ v' ∧ valid_argument i ∧ valid_eval (v, w) ∧ valid_eval (v', w'));
let b = verify_eval vk c i (v,w);
let b' = verify_eval vk c i (v',w');
return_spmf (b ∧ b')} ELSE return_spmf False"
unfolding eval_bind_game_def knowledge_soundness_reduction_ext_def
by simp
text ‹We extend the evaluation binding game with the normal reduction adversary to a complete
game.›
have wo_assert_ext: "eval_bind_game (knowledge_soundness_reduction E 𝒜 𝒜') =
TRY do {
(ck, vk) ← key_gen;
((c,cvec),σ) ← AGM1.restrict 𝒜 ck;
(p,td) ← E (c,cvec);
(i, v, (w, wvec)) ← AGM2.restrict 𝒜' (ck,σ);
let (v',w') = Eval ck td p i;
_ :: unit ← assert_spmf (v ≠ v' ∧ valid_argument i ∧ valid_eval (v, w) ∧ valid_eval (v', w'));
let b = verify_eval vk c i (v,w);
let b' = verify_eval vk c i (v',w');
return_spmf (b ∧ b')} ELSE return_spmf False"
unfolding eval_bind_game_def knowledge_soundness_reduction_def
by simp
text ‹We show the thesis in ennreal, which implies the plain thesis›
have "ennreal (spmf (eval_bind_game (knowledge_soundness_reduction_ext E 𝒜 𝒜')) True)
≤ ennreal (spmf (eval_bind_game (knowledge_soundness_reduction E 𝒜 𝒜')) True)"
unfolding w_assert_ext wo_assert_ext
apply (simp add: spmf_try_spmf ennreal_spmf_bind)
apply (rule nn_integral_mono)+
apply (simp add: assert_spmf_def)
apply (simp add: measure_spmf.emeasure_eq_measure)
done
then show ?thesis by simp
qed
text ‹Finally we put everything together:
we conclude that for every efficient adversary in the AGM the advantage over winning the
knowledge soundness game is less than or equal to breaking the t-SDH assumption.›
theorem knowledge_soundness:
"spmf (knowledge_soundness_game_AGM 𝒜1 𝒜2 E) True
≤ t_SDH_G⇩p.advantage (eval_bind_reduction (knowledge_soundness_reduction E 𝒜1 𝒜2))"
using evaluation_binding[of "knowledge_soundness_reduction E 𝒜1 𝒜2"]
overestimate_reductions[of 𝒜1 𝒜2]
unfolding eval_bind_advantage_def knowledge_soundness_game_alt_def
by linarith
end
end