Theory BatchKZG_eval_bind
theory BatchKZG_eval_bind
imports BatchKZG_correct tBSDH_assumption CryptHOL_ext
begin
section ‹Evaluation Binding of the batched KZG›
locale BatchEvalKZG_PCS_eval_bind = BatchEvalKZG_PCS_correct
begin
text ‹We prove two evaluation binding properties:
1. the classical evaluation binding game from PCS
2. the binding game from the original KZG paper \<^cite>‹KZG10›
The difference is that 1. shows that the batched evaluation function is binding following the
classical definition (i.e. two batched evaluations for the same argument must be equal) and
2. shows that the batched evaluation function is binding with respect to single evaluation
function. ›
subsection ‹t-BSDH game›
text ‹We instantiate the t-BSDH game for the pairing e, with the group Gp as preimage group and GT
as target group.›
sublocale t_BSDH: t_BSDH G⇩p G⇩T max_deg "of_int_mod_ring ∘ int" "pow_mod_ring G⇩p" "pow_mod_ring G⇩T" e
unfolding t_BSDH_def
using G⇩T.cyclic_group_axioms G⇩p.cyclic_group_axioms by presburger
subsection ‹Binding for the batched evaluation according to KZG10›
type_synonym ('a', 'e') adversary =
"'a' ck ⇒
('a' commit × 'e' argument × 'e' evaluation × 'a' witness × 'e' argument set
× 'a' witness × 'e' batch_evaluation) spmf"
text ‹This is the formalized evaluation binding game›
definition bind_game :: "('a, 'e) adversary ⇒ bool spmf"
where "bind_game 𝒜 = TRY do {
(ck,vk) ← key_gen;
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 ck;
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B ∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B));
let b = verify_eval vk C i (φ_i, w_i);
let b' = verify_eval_batch vk C B (r_x,w_B);
return_spmf (b ∧ b')} ELSE return_spmf False"
text ‹The advantage of the adversary over the evaluation binding game is the probability that it
wins.›
definition bind_advantage :: "('a, 'e) adversary ⇒ real"
where "bind_advantage 𝒜 ≡ spmf (bind_game 𝒜) True"
subsubsection ‹Defining a reduction function to t-BSDH›
text ‹The reduction function takes an adversary for the evaluation binding game and returns an
adversary for the t-BSDH game. Specifically, the reduction uses the evaluation binding adversary to
construct a winning strategy for the t-BSDH game (i.e. to win it every time).
Essentially, it uses the fact that the values supplied by the adversary already break the t-BSDH
assumption.›
fun reduction
:: "('a, 'e) adversary ⇒ ('a,'e,'c) t_BSDH.adversary"
where
"reduction 𝒜 PK = do {
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 PK;
let p' = g_pow_PK_Prod PK (prod (λi. [:-i,1:]) B div [:-i,1:]);
let r' = g_pow_PK_Prod PK ((r_x - [:poly r_x i:]) div [:-i,1:]);
return_spmf (-i::'e mod_ring, (e p' w_B ⊗⇘G⇩T⇙ e (r' ÷⇘G⇩p⇙ w_i) ❙g) ^⇘G⇩T⇙ (1/(φ_i - poly r_x i))) }"
text ‹The 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.›
fun ext_reduction
:: "('a, 'e) adversary ⇒ ('a,'e,'c) t_BSDH.adversary"
where
"ext_reduction 𝒜 PK = do {
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 PK;
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B
∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B)
∧ verify_eval PK C i (φ_i, w_i) ∧ verify_eval_batch PK C B (r_x, w_B));
let p' = g_pow_PK_Prod PK (prod (λi. [:-i,1:]) B div [:-i,1:]);
let r' = g_pow_PK_Prod PK ((r_x - [:poly r_x i:]) div [:-i,1:]);
return_spmf (-i::'e mod_ring, (e p' w_B ⊗⇘G⇩T⇙ e (r' ÷⇘G⇩p⇙ w_i) ❙g) ^⇘G⇩T⇙ (1/(φ_i - poly r_x i))) }"
subsubsection ‹Helping lemmas›
text ‹An alternative but equivalent game for the evaluation binding game.
This alternative game encapsulates the
event that the Adversary wins in the assert\_spmf statement.
It's a closely adapted proof from Sigma\_Commit\_Crypto.Commitment\_Schemes bind\_game\_alt\_def›
lemma bind_game_alt_def:
"bind_game 𝒜 = TRY do {
(ck,vk) ← key_gen;
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 ck;
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B ∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B));
let b = verify_eval vk C i (φ_i, w_i);
let b' = verify_eval_batch vk C B (r_x, w_B);
_::unit ← assert_spmf (b ∧ b');
return_spmf True} ELSE return_spmf False"
(is "?lhs = ?rhs")
proof -
have "?lhs = TRY do {
(ck,vk) ← key_gen;
TRY do {
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 ck;
TRY do {
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B ∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B));
TRY do {
let b = verify_eval vk C i (φ_i, w_i);
let b' = verify_eval_batch vk C B (r_x, w_B);
return_spmf (b ∧ b')
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False"
unfolding split_def bind_game_def
by(fold try_bind_spmf_lossless2[OF lossless_return_spmf]) simp
also have "… = TRY do {
(ck,vk) ← key_gen;
TRY do {
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 ck;
TRY do {
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B ∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B));
TRY do {
let b = verify_eval vk C i (φ_i, w_i);
let b' = verify_eval_batch vk C B (r_x, w_B);
_::unit ← assert_spmf (b ∧ b');
return_spmf True
} 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 "… = ?rhs"
unfolding split_def Let_def
by(fold try_bind_spmf_lossless2[OF lossless_return_spmf]) simp
finally show ?thesis .
qed
text ‹show that VerifyEvalBatch of B and r(x) and VerifEval on ‹i ∈ B› and ‹φ_i› such that ‹φ_i ≠ r(x)›
implies that the t-BSDH is broken.
This lemma captures that the adversaries messages already break the t-BSDH assumption.›
lemma verifys_impl_t_BSDH_break:
assumes "i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B
∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B)
∧ verify_eval (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1]) C i (φ_i, w_i)
∧ verify_eval_batch (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1]) C B (r_x, w_B)"
shows " e ❙g ❙g ^⇘G⇩T⇙ (1 / (α + - i))
=
(e (g_pow_PK_Prod (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1])
((∏i∈B. [:- i, 1:]) div [:- i, 1:]))
w_B
⊗⇘G⇩T⇙
e (g_pow_PK_Prod (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1])
((r_x - [:poly r_x i:]) div [:- i, 1:]) ⊗
inv w_i)
❙g) ^⇘G⇩T⇙
(1 / (φ_i - poly r_x i))"
(is "?goal = ?cmpt")
proof -
obtain b where b: "w_B = ❙g ^ b"
apply (insert assms)
apply (simp only: valid_eval_batch_def Let_def split_def)
apply (simp split: prod.split)
apply (metis G⇩p.generatorE g_pow_to_int_mod_ring_of_int_mod_ring int_pow_int)
done
obtain y where y: "w_i = ❙g ^ y"
apply (insert assms)
apply (simp only: valid_eval_def Let_def split_def)
apply (simp split: prod.split)
by (metis G⇩p.generatorE g_pow_to_int_mod_ring_of_int_mod_ring int_pow_int)
obtain r'_x where r'_x: "r'_x = (r_x - [:poly r_x i:]) div [:- i, 1:]" by blast
then have r'_x_r_x: "r_x = r'_x *[:- i, 1:] + [:poly r_x i:]"
by (metis Groups.mult_ac(2) diff_eq_eq nonzero_mult_div_cancel_left one_neq_zero pCons_eq_0_iff synthetic_div_correct')
obtain p'_x where p'_x:"p'_x = (∏i∈B. [:- i, 1:]) div [:- i, 1:]" by blast
then have p'_x_p_x: "(∏i∈B. [:- i, 1:]) = p'_x * [:- i, 1:]"
using assms
by (metis (no_types, lifting) Groups.mult_ac(2) arith_extra_simps(6) i_in_B_prod_B_zero nonzero_mult_div_cancel_left one_neq_zero pCons_eq_0_iff synthetic_div_correct')
text ‹the proof is essentially rearranging equations, an outline can be found in the batched versions
evaluation binding proof section in the thesis paper.›
from assms have "e w_i (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1] ! 1 ⊗ inv (❙g ^ i)) ⊗⇘G⇩T⇙ e ❙g ❙g ^⇘G⇩T⇙ φ_i
= e (g_pow_PK_Prod (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1]) (∏i∈B. [:- i, 1:])) w_B ⊗⇘G⇩T⇙
e ❙g (g_pow_PK_Prod (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1]) r_x)" (is "?lhs = ?rhs")
unfolding verify_eval_def verify_eval_batch_def Let_def split_def by auto
moreover have "?lhs = e (❙g ^ y) (❙g ^ (α-i) ) ⊗⇘G⇩T⇙ e ❙g ❙g ^⇘G⇩T⇙ φ_i"
unfolding y using PK_i d_pos mod_ring_pow_mult_inv_G⇩p by auto
moreover have "?rhs = e (❙g ^ poly (∏i∈B. [:- i, 1:]) α) (❙g ^ b) ⊗⇘G⇩T⇙ e ❙g (❙g ^ poly r_x α)"
proof -
have "g_pow_PK_Prod (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1]) (∏i∈B. [:- i, 1:])
= ❙g ^ poly (∏i∈B. [:- i, 1:]) α"
using g_pow_PK_Prod_correct assms deg_Prod le_simps(1)
unfolding valid_eval_batch_def valid_argument_batch_def by presburger
moreover have "g_pow_PK_Prod (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1]) r_x = ❙g ^ poly r_x α"
using g_pow_PK_Prod_correct assms unfolding verify_eval_batch_def valid_argument_batch_def
valid_eval_batch_def
by (simp split: prod.split add: split_def Let_def del: g_pow_PK_Prod.simps)
ultimately show ?thesis unfolding b by argo
qed
ultimately have "e (❙g ^ y) (❙g ^ (α-i) ) ⊗⇘G⇩T⇙ e ❙g ❙g ^⇘G⇩T⇙ φ_i = e (❙g ^ poly (∏i∈B. [:- i, 1:]) α) (❙g ^ b) ⊗⇘G⇩T⇙ e ❙g (❙g ^ poly r_x α)"
by argo
then have "y*(α-i) + φ_i = (poly (∏i∈B. [:- i, 1:]) α)*b + poly r_x α"
using e_bilinear e_linear_in_snd
using addition_in_exponents_on_e pow_on_eq_card_GT_carrier_ext' by auto
text ‹mimicking steps from the batch opening binding proof in the original paper; see Appendix C.3 of \<^cite>‹KZG10›.›
then have "(poly (∏i∈B. [:- i, 1:]) α)*b - (α-i)*y = φ_i - poly r_x α"
by (metis (no_types, lifting) add_diff_cancel_left' add_diff_cancel_right' add_diff_eq mult.commute)
then have "(poly (∏i∈B. [:- i, 1:]) α)*b - (α-i)*y = φ_i - (poly r'_x α)*(α-i) - poly [:poly r_x i:] α"
using r'_x_r_x poly_mult poly_add
by (smt (z3) ab_group_add_class.ab_diff_conv_add_uminus add_cancel_left_right group_cancel.add2 more_arith_simps(6) more_arith_simps(9) mult_cancel_right1 poly_0 poly_pCons uminus_add_conv_diff)
then have "(α-i)*(poly p'_x α)*b - (α-i)*y = φ_i - (poly r'_x α)*(α-i) - poly [:poly r_x i:] α"
using p'_x_p_x
by (smt (verit) Groups.add_ac(2) add_uminus_conv_diff more_arith_simps(6) mult.commute one_pCons poly_1 poly_mult poly_pCons)
then have "(α-i)*((poly p'_x α)*b - y + poly r'_x α) = φ_i - poly [:poly r_x i:] α"
by (simp add: Groups.mult_ac(2) Groups.mult_ac(3) Rings.ring_distribs(1) Rings.ring_distribs(4))
then have "(α-i)*((poly p'_x α)*b - y + poly r'_x α) = φ_i - poly r_x i"
by auto
then have poly_eq_res: "1/(α-i) = ((poly p'_x α)*b - y + poly r'_x α)/(φ_i - poly r_x i)"
by (metis (no_types, lifting) assms div_self divide_divide_eq_left mult.commute mult_eq_0_iff right_minus_eq)
moreover have "?cmpt = (e (❙g ^⇘G⇩p⇙ (poly p'_x α)) (❙g ^⇘G⇩p⇙ b) ⊗⇘G⇩T⇙ e (❙g ^⇘G⇩p⇙ (poly r'_x α) ÷⇘G⇩p⇙ (❙g ^⇘G⇩p⇙ y))
❙g) ^⇘G⇩T⇙ (1 / (φ_i - poly r_x i))"
proof -
have "g_pow_PK_Prod (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1]) ((∏i∈B. [:- i, 1:]) div [:- i, 1:])
= ❙g ^⇘G⇩p⇙ (poly p'_x α)"
unfolding p'_x
by (rule g_pow_PK_Prod_correct)(metis (no_types, lifting) assms verify_eval_batch_def valid_argument_batch_def deg_Prod deg_div le_trans nat_le_linear not_less)
moreover have "g_pow_PK_Prod (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1]) ((r_x - [:poly r_x i:]) div [:- i, 1:])
= ❙g ^⇘G⇩p⇙ (poly r'_x α)"
unfolding r'_x
apply (rule g_pow_PK_Prod_correct)
apply (insert assms)
apply (simp add: verify_eval_batch_def valid_argument_batch_def valid_eval_batch_def
del: One_nat_def g_pow_PK_Prod.simps)
apply (metis (mono_tags, opaque_lifting) deg_div degree_diff_le degree_pCons_0
le_trans less_or_eq_imp_le zero_le)
done
ultimately show ?thesis unfolding y b by argo
qed
moreover have "… = e ❙g ❙g ^⇘G⇩T⇙ (((poly p'_x α)*b - y + poly r'_x α)/(φ_i - poly r_x i))"
proof -
have "(e (❙g ^⇘G⇩p⇙ poly p'_x α) (❙g ^⇘G⇩p⇙ b) ⊗⇘G⇩T⇙
e (❙g ^⇘G⇩p⇙ poly r'_x α ⊗ inv (❙g ^⇘G⇩p⇙ y)) ❙g) ^⇘G⇩T⇙ (1 / (φ_i - poly r_x i))
= (e (❙g ^⇘G⇩p⇙ poly p'_x α) (❙g ^⇘G⇩p⇙ b) ⊗⇘G⇩T⇙
e (❙g ^⇘G⇩p⇙ (poly r'_x α - y)) ❙g) ^⇘G⇩T⇙ (1 / (φ_i - poly r_x i))"
using mod_ring_pow_mult_inv_G⇩p by presburger
also have "… = (e ❙g ❙g ^⇘G⇩T⇙ ((poly p'_x α)*b) ⊗⇘G⇩T⇙
e ❙g ❙g ^⇘G⇩T⇙ (poly r'_x α - y)) ^⇘G⇩T⇙ (1 / (φ_i - poly r_x i))"
using e_linear_in_fst G⇩p.generator_closed e_bilinear by presburger
also have "… = (e ❙g ❙g ^⇘G⇩T⇙ ((poly p'_x α)*b + poly r'_x α - y)) ^⇘G⇩T⇙ (1 / (φ_i - poly r_x i))"
using add_diff_eq
by (metis G⇩p.generator_closed addition_in_exponents_on_e)
also have "… = e ❙g ❙g ^⇘G⇩T⇙ (((poly p'_x α)*b + poly r'_x α - y)/(φ_i - poly r_x i))"
using G⇩T.int_pow_pow e_bilinear by force
finally show ?thesis
by (simp add: cross3_simps(14,8))
qed
ultimately
show ?thesis by fastforce
qed
subsection ‹Literal helping lemma›
text ‹CryptHOL has some difficulties with simplifying, thus we need to use literal helping lemmas,
that state the equalities we want to exchange literally.›
lemma literal_helping:
"(i ∈ (B::'e argument set) ∧
(φ_i:: 'e evaluation) ≠ (poly r_x i:: 'e evaluation) ∧
valid_argument_batch B ∧
valid_eval (φ_i,w_i) ∧ valid_eval_batch (r_x,w_B) ∧
verify_eval (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) C i (φ_i,w_i) ∧
verify_eval_batch (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α::'e mod_ring) ^ t) [0..<max_deg + 1]) C B (r_x,w_B) ∧
e ❙g ❙g ^⇘G⇩T⇙ (1 / (α + - i)) =
(e (g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1])
((∏i∈B. [:- i, 1:]) div [:- i, 1:]))
w_B ⊗⇘G⇩T⇙
e (g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1])
((r_x - [:poly r_x i:]) div [:- i, 1:]) ⊗
inv w_i)
❙g) ^⇘G⇩T⇙
((1::'e mod_ring) / (φ_i - poly r_x i)))
⟷
(i ∈ B ∧
φ_i ≠ poly r_x i ∧
valid_argument_batch B ∧
valid_eval (φ_i,w_i) ∧ valid_eval_batch (r_x,w_B) ∧
verify_eval (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) C i (φ_i,w_i) ∧
verify_eval_batch (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) C B (r_x,w_B))"
using verifys_impl_t_BSDH_break by fast
subsection ‹KZG eval bind game to reduction game - equivalence theorem›
text ‹We show that the binding game is equivalent to the t-BSDH game with the extended reduction
adversary.›
lemma bind_game_eq_t_BSDH_red: "bind_game 𝒜 = t_BSDH.game (ext_reduction 𝒜)"
proof -
note [simp] = Let_def split_def
text ‹abbreviations for the mod\_ring version of sample uniform nat
and the public key›
let ?mr = "λα. (of_int_mod_ring (int α)::'e mod_ring)"
let ?PK = "λα. (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((?mr α)^t)) [0..<max_deg+1])"
text ‹Firstly, unfold the t-BSDH game and the reduction adversary›
have "t_BSDH.game (ext_reduction 𝒜) = TRY do {
α ← sample_uniform (order G⇩p);
(c, g) ← (ext_reduction 𝒜) (?PK α);
_::unit ← assert_spmf((e ❙g ❙g) ^⇘G⇩T⇙ (1/((?mr α)+c)) = g);
return_spmf True
} ELSE return_spmf False"
unfolding t_BSDH.game_alt_def by (metis o_def)
also have "… = TRY do {
α ← sample_uniform (order G⇩p);
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 (?PK α);
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B
∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B)
∧ verify_eval (?PK α) C i (φ_i, w_i) ∧ verify_eval_batch (?PK α) C B (r_x, w_B));
let p' = g_pow_PK_Prod (?PK α) (prod (λi. [:-i,1:]) B div [:-i,1:]);
let r' = g_pow_PK_Prod (?PK α) ((r_x - [:poly r_x i:]) div [:-i,1:]);
_::unit ← assert_spmf ((e ❙g ❙g) ^⇘G⇩T⇙ (1/((?mr α)+(-i))) = (e p' w_B ⊗⇘G⇩T⇙ e (r' ÷⇘G⇩p⇙ w_i) ❙g) ^⇘G⇩T⇙ (1/(φ_i - poly r_x i)));
return_spmf True
} ELSE return_spmf False"
by force
text ‹fold the two asserts together so we can reason about their joined content.›
also have "… = TRY do {
α ← sample_uniform (order G⇩p);
TRY do {
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 (?PK α);
TRY do {
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B
∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B)
∧ verify_eval (?PK α) C i (φ_i, w_i) ∧ verify_eval_batch (?PK α) C B (r_x, w_B));
let p' = g_pow_PK_Prod (?PK α) (prod (λi. [:-i,1:]) B div [:-i,1:]);
let r' = g_pow_PK_Prod (?PK α) ((r_x - [:poly r_x i:]) div [:-i,1:]);
_::unit ← assert_spmf ((e ❙g ❙g) ^⇘G⇩T⇙ (1/((?mr α)+(-i))) = (e p' w_B ⊗⇘G⇩T⇙ e (r' ÷⇘G⇩p⇙ w_i) ❙g) ^⇘G⇩T⇙ (1/(φ_i - poly r_x i)));
return_spmf True
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False"
unfolding split_def Let_def
by(fold try_bind_spmf_lossless2[OF lossless_return_spmf]) simp
also have "… = TRY do {
α ← sample_uniform (order G⇩p);
TRY do {
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 (?PK α);
TRY do {
let p' = g_pow_PK_Prod (?PK α) (prod (λi. [:-i,1:]) B div [:-i,1:]);
let r' = g_pow_PK_Prod (?PK α) ((r_x - [:poly r_x i:]) div [:-i,1:]);
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B
∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B)
∧ verify_eval (?PK α) C i (φ_i, w_i) ∧ verify_eval_batch (?PK α) C B (r_x, w_B)
∧ (e ❙g ❙g) ^⇘G⇩T⇙ (1/((?mr α)+(-i)))
= (e p' w_B ⊗⇘G⇩T⇙ e (r' ÷⇘G⇩p⇙ w_i) ❙g) ^⇘G⇩T⇙ (1/(φ_i - poly r_x i)));
return_spmf True
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False"
by (simp add: assert_collapse del: g_pow_PK_Prod.simps)
also have "… = TRY do {
α ← sample_uniform (order G⇩p);
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 (?PK α);
let p' = g_pow_PK_Prod (?PK α) (prod (λi. [:-i,1:]) B div [:-i,1:]);
let r' = g_pow_PK_Prod (?PK α) ((r_x - [:poly r_x i:]) div [:-i,1:]);
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B
∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B)
∧ verify_eval (?PK α) C i (φ_i, w_i) ∧ verify_eval_batch (?PK α) C B (r_x, w_B)
∧ (e ❙g ❙g) ^⇘G⇩T⇙ (1/((?mr α)+(-i)))
= (e p' w_B ⊗⇘G⇩T⇙ e (r' ÷⇘G⇩p⇙ w_i) ❙g) ^⇘G⇩T⇙ (1/(φ_i - poly r_x i)));
return_spmf True
} ELSE return_spmf False"
unfolding split_def Let_def
by(fold try_bind_spmf_lossless2[OF lossless_return_spmf]) simp
text ‹erase the pairing check with the literal helping lemma to get closer to the eval bind game›
also have "… = TRY do {
α ← sample_uniform (order G⇩p);
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 (?PK α);
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B
∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B)
∧ verify_eval (?PK α) C i (φ_i, w_i) ∧ verify_eval_batch (?PK α) C B (r_x, w_B));
return_spmf True
} ELSE return_spmf False"
unfolding Let_def using literal_helping by algebra
text ‹Split the message checks off the Evaluations checks, as it is done in the eval bind game›
also have "… = TRY do {
α ← sample_uniform (order G⇩p);
TRY do {
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 (?PK α);
TRY do {
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B
∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B)
∧ verify_eval (?PK α) C i (φ_i, w_i) ∧ verify_eval_batch (?PK α) C B (r_x, w_B));
return_spmf True
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False"
unfolding split_def Let_def
by(fold try_bind_spmf_lossless2[OF lossless_return_spmf]) simp
also have "… = TRY do {
α ← sample_uniform (order G⇩p);
TRY do {
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 (?PK α);
TRY do {
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B
∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B));
_ :: unit ← assert_spmf (verify_eval (?PK α) C i (φ_i, w_i) ∧ verify_eval_batch (?PK α) C B (r_x, w_B));
return_spmf True
} ELSE return_spmf False
} ELSE return_spmf False
} ELSE return_spmf False"
by (simp add: assert_collapse del: g_pow_PK_Prod.simps)
also have "… = TRY do {
α ← sample_uniform (order G⇩p);
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 (?PK α);
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B
∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B));
_ :: unit ← assert_spmf (verify_eval (?PK α) C i (φ_i, w_i) ∧ verify_eval_batch (?PK α) C B (r_x, w_B));
return_spmf True
} ELSE return_spmf False"
unfolding split_def Let_def
by(fold try_bind_spmf_lossless2[OF lossless_return_spmf]) simp
text ‹the obtained game is already the evaluation binding game.›
also have "…= bind_game 𝒜"
using bind_game_alt_def unfolding key_gen_def Setup_def by simp
finally show ?thesis ..
qed
text ‹From the previous lemma we conclude that the adversary's advantage on winning the evaluation
binding game is the same as winning the t-BSDH game with the extended reduction adversary.›
lemma evaluation_binding_ext_red: "bind_advantage 𝒜 = t_BSDH.advantage (ext_reduction 𝒜)"
unfolding bind_advantage_def t_BSDH.advantage_def
using bind_game_eq_t_BSDH_red by presburger
text ‹Now we use overestimation to show that the advantage of winning the t-BSDH game with the
extended reduction adversary is less than or equal to winning it with the normal reduction adversary.›
lemma overestimate_reductions: "spmf (t_BSDH.game (ext_reduction 𝒜)) True
≤ spmf (t_BSDH.game (reduction 𝒜)) True"
(is "spmf ?lhgame True ≤ spmf ?rhgame True")
proof -
note [simp] = Let_def split_def
text ‹abbreviations for the mod\_ring version of sample uniform nat
and the public key›
let ?α = "λα. (of_int_mod_ring (int α)::'e mod_ring)"
let ?PK = "λα. (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((?α α)^t)) [0..<max_deg+1])"
text ‹We extend the t-BSDH game with the extended reduction adversary to a complete game.›
have bind_red_ext: "t_BSDH.game (ext_reduction 𝒜) = TRY do {
α ← sample_uniform (order G⇩p);
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 (?PK α);
_ :: unit ← assert_spmf (i ∈ B ∧ φ_i ≠ poly r_x i
∧ valid_argument_batch B
∧ valid_eval (φ_i, w_i) ∧ valid_eval_batch (r_x, w_B)
∧ verify_eval (?PK α) C i (φ_i, w_i) ∧ verify_eval_batch (?PK α) C B (r_x, w_B));
let p' = g_pow_PK_Prod (?PK α) (prod (λi. [:-i,1:]) B div [:-i,1:]);
let r' = g_pow_PK_Prod (?PK α) ((r_x - [:poly r_x i:]) div [:-i,1:]);
_::unit ← assert_spmf ((e ❙g ❙g) ^⇘G⇩T⇙ (1/((?α α)+(-i))) = (e p' w_B ⊗⇘G⇩T⇙ e (r' ÷⇘G⇩p⇙ w_i) ❙g) ^⇘G⇩T⇙ (1/(φ_i - poly r_x i)));
return_spmf True
} ELSE return_spmf False"
by (force simp add: t_BSDH.game_alt_def[of "(ext_reduction 𝒜)"])
text ‹We extend the t-BSDH game with reduction adversary to a complete game.›
have eval_bind_red_ext: "t_BSDH.game (reduction 𝒜) = TRY do {
α ← sample_uniform (order G⇩p);
(C, i, φ_i, w_i, B, w_B, r_x) ← 𝒜 (?PK α);
let p' = g_pow_PK_Prod (?PK α) (prod (λi. [:-i,1:]) B div [:-i,1:]);
let r' = g_pow_PK_Prod (?PK α) ((r_x - [:poly r_x i:]) div [:-i,1:]);
_::unit ← assert_spmf ((e ❙g ❙g) ^⇘G⇩T⇙ (1/((?α α)+(-i))) = (e p' w_B ⊗⇘G⇩T⇙ e (r' ÷⇘G⇩p⇙ w_i) ❙g) ^⇘G⇩T⇙ (1/(φ_i - poly r_x i)));
return_spmf True
} ELSE return_spmf False"
by (force simp add: t_BSDH.game_alt_def[of "(reduction 𝒜)"])
text ‹We show the thesis in ennreal, which implies the plain thesis›
have "ennreal (spmf (t_BSDH.game (ext_reduction 𝒜)) True)
≤ ennreal (spmf (t_BSDH.game (reduction 𝒜)) True)"
unfolding bind_red_ext eval_bind_red_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 the advantage of winning the
evaluation binding game for the batched KZG is less than or equal to breaking the t-BSDH assumption.›
theorem evaluation_binding: "bind_advantage 𝒜 ≤ t_BSDH.advantage (reduction 𝒜)"
using evaluation_binding_ext_red overestimate_reductions
unfolding t_BSDH.advantage_def
by algebra
end
end