Theory Sigma_Protocols
section‹‹Σ›-Protocols›
text‹‹Σ›-protocols were first introduced as an abstract notion by Cramer \<^cite>‹"Cramerthesis"›.
We point the reader to \<^cite>‹"sigma_protocols"› for a good introduction to the primitive as well as informal proofs
of many of the constructions we formalise in this work. In particular the construction of commitment schemes from
‹Σ›-protocols and the construction of compound AND and OR statements.
In this section we define ‹Σ›-protocols then provide a general proof that they can be used to construct commitment schemes.
Defining security for ‹Σ›-protocols uses a mixture of the game-based and simulation-based paradigms. The honest verifier
zero knowledge property is considered using simulation-based proof, thus we follow the follow the simulation-based formalisation
of \<^cite>‹"DBLP:journals/afp/AspinallB19"› and \<^cite>‹"DBLP:conf/itp/Butler0G17"›.›
subsection‹Defining ‹Σ›-protocols›
theory Sigma_Protocols imports
CryptHOL.CryptHOL
Commitment_Schemes
begin
type_synonym ('msg', 'challenge', 'response') conv_tuple = "('msg' × 'challenge' × 'response')"
type_synonym ('msg','response') sim_out = "('msg' × 'response')"
type_synonym ('pub_input', 'msg', 'challenge', 'response', 'witness') prover_adversary
= "'pub_input' ⇒ ('msg', 'challenge', 'response') conv_tuple
⇒ ('msg', 'challenge', 'response') conv_tuple ⇒ 'witness' spmf"
locale Σ_protocols_base =
fixes init :: "'pub_input ⇒ 'witness ⇒ ('rand × 'msg) spmf"
and response :: "'rand ⇒ 'witness ⇒ 'challenge ⇒ 'response spmf"
and check :: "'pub_input ⇒ 'msg ⇒ 'challenge ⇒ 'response ⇒ bool"
and Rel :: "('pub_input × 'witness) set"
and S_raw :: "'pub_input ⇒ 'challenge ⇒ ('msg, 'response) sim_out spmf"
and 𝒜ss :: "('pub_input, 'msg, 'challenge, 'response, 'witness) prover_adversary"
and challenge_space :: "'challenge set"
and valid_pub :: "'pub_input set"
assumes domain_subset_valid_pub: "Domain Rel ⊆ valid_pub"
begin
lemma assumes "x ∈ Domain Rel" shows "∃ w. (x,w) ∈ Rel"
using assms by auto
text‹The language defined by the relation is the set of all public inputs such that there exists a witness that satisfies the relation.›
definition "L ≡ {x. ∃ w. (x, w) ∈ Rel}"
text‹The first property of ‹Σ›-protocols we consider is completeness, we define a probabilistic programme
that runs the components of the protocol and outputs the boolean defined by the check algorithm.›
definition completeness_game :: "'pub_input ⇒ 'witness ⇒ 'challenge ⇒ bool spmf"
where "completeness_game h w e = do {
(r, a) ← init h w;
z ← response r w e;
return_spmf (check h a e z)}"
text‹We define completeness as the probability that the completeness-game returns true for all challenges assuming the relation holds on ‹h› and ‹w›.›
definition "completeness ≡ (∀ h w e . (h,w) ∈ Rel ⟶ e ∈ challenge_space ⟶ spmf (completeness_game h w e) True = 1)"
text‹Second we consider the honest verifier zero knowledge property (HVZK). To reason about this we construct the real view of the
‹Σ›-protocol given a challenge ‹e› as input.›
definition R :: "'pub_input ⇒ 'witness ⇒ 'challenge ⇒ ('msg, 'challenge, 'response) conv_tuple spmf"
where "R h w e = do {
(r,a) ← init h w;
z ← response r w e;
return_spmf (a,e,z)}"
definition S where "S h e = map_spmf (λ (a, z). (a, e, z)) (S_raw h e)"
lemma lossless_S_raw_imp_lossless_S: "lossless_spmf (S_raw h e) ⟶ lossless_spmf (S h e)"
by(simp add: S_def)
text‹The HVZK property requires that the simulator's output distribution is equal to the real views output distribution.›
definition "HVZK ≡ (∀e ∈ challenge_space.
(∀(h, w)∈Rel. R h w e = S h e)
∧ (∀h ∈ valid_pub. ∀(a, z) ∈ set_spmf (S_raw h e). check h a e z))"
text‹The final property to consider is that of special soundness. This says that given two valid transcripts such that the challenges
are not equal there exists an adversary ‹𝒜ss› that can output the witness.›
definition "special_soundness ≡ (∀ h e e' a z z'. h ∈ valid_pub ⟶ e ∈ challenge_space ⟶ e' ∈ challenge_space ⟶ e ≠ e'
⟶ check h a e z ⟶ check h a e' z' ⟶ (lossless_spmf (𝒜ss h (a,e,z) (a, e', z')) ∧
(∀w'∈set_spmf (𝒜ss h (a,e,z) (a,e',z')). (h,w') ∈ Rel)))"
lemma special_soundness_alt:
"special_soundness ⟷
(∀ h a e z e' z'. e ∈ challenge_space ⟶ e' ∈ challenge_space ⟶ h ∈ valid_pub
⟶ e ≠ e' ⟶ check h a e z ∧ check h a e' z'
⟶ bind_spmf (𝒜ss h (a,e,z) (a,e',z')) (λ w'. return_spmf ((h,w') ∈ Rel)) = return_spmf True)"
apply(auto simp add: special_soundness_def map_spmf_conv_bind_spmf[symmetric] map_pmf_eq_return_pmf_iff in_set_spmf lossless_iff_set_pmf_None)
apply(metis Domain.DomainI in_set_spmf not_Some_eq)
using Domain.intros by blast +
definition "Σ_protocol ≡ completeness ∧ special_soundness ∧ HVZK"
text‹General lemmas›
lemma lossless_complete_game:
assumes lossless_init: "∀ h w. lossless_spmf (init h w)"
and lossless_response: "∀ r w e. lossless_spmf (response r w e)"
shows "lossless_spmf (completeness_game h w e)"
by(simp add: completeness_game_def lossless_init lossless_response split_def)
lemma complete_game_return_true:
assumes "(h,w) ∈ Rel"
and "completeness"
and lossless_init: "∀ h w. lossless_spmf (init h w)"
and lossless_response: "∀ r w e. lossless_spmf (response r w e)"
and "e ∈ challenge_space"
shows "completeness_game h w e = return_spmf True"
proof -
have "spmf (completeness_game h w e) True = spmf (return_spmf True) True"
using assms Σ_protocol_def completeness_def by fastforce
then have "completeness_game h w e = return_spmf True"
by (metis (full_types) lossless_complete_game lossless_init lossless_response lossless_return_spmf spmf_False_conv_True spmf_eqI)
then show ?thesis
by (simp add: completeness_game_def)
qed
lemma HVZK_unfold1:
assumes "Σ_protocol"
shows "∀ h w e. (h,w) ∈ Rel ⟶ e ∈ challenge_space ⟶ R h w e = S h e"
using assms by(auto simp add: Σ_protocol_def HVZK_def)
lemma HVZK_unfold2:
assumes "Σ_protocol"
shows "∀ h e out. e ∈ challenge_space ⟶ h ∈ valid_pub ⟶ out ∈ set_spmf (S_raw h e) ⟶ check h (fst out) e (snd out)"
using assms by(auto simp add: Σ_protocol_def HVZK_def split_def)
lemma HVZK_unfold2_alt:
assumes "Σ_protocol"
shows "∀ h a e z. e ∈ challenge_space ⟶ h ∈ valid_pub ⟶ (a,z) ∈ set_spmf (S_raw h e) ⟶ check h a e z"
using assms by(fastforce simp add: Σ_protocol_def HVZK_def)
end
subsection‹Commitments from ‹Σ›-protocols›
text‹In this section we provide a general proof that ‹Σ›-protocols can be used to construct commitment schemes.
We follow the construction given by Damgard in \<^cite>‹"sigma_protocols"›.›
locale Σ_protocols_to_commitments = Σ_protocols_base init response check Rel S_raw 𝒜ss challenge_space valid_pub
for init :: "'pub_input ⇒ 'witness ⇒ ('rand × 'msg) spmf"
and response :: "'rand ⇒ 'witness ⇒ 'challenge ⇒ 'response spmf"
and check :: "'pub_input ⇒ 'msg ⇒ 'challenge ⇒ 'response ⇒ bool"
and Rel :: "('pub_input × 'witness) set"
and S_raw :: "'pub_input ⇒ 'challenge ⇒ ('msg, 'response) sim_out spmf"
and 𝒜ss :: "('pub_input, 'msg, 'challenge, 'response, 'witness) prover_adversary"
and challenge_space :: "'challenge set"
and valid_pub :: "'pub_input set"
and G :: "('pub_input × 'witness) spmf"
+
assumes Σ_prot: "Σ_protocol"
and set_spmf_G_rel [simp]: "(h,w) ∈ set_spmf G ⟹ (h,w) ∈ Rel"
and lossless_G: "lossless_spmf G"
and lossless_init: "lossless_spmf (init h w)"
and lossless_response: "lossless_spmf (response r w e)"
begin
lemma set_spmf_G_domain_rel [simp]: "(h,w) ∈ set_spmf G ⟹ h ∈ Domain Rel"
using set_spmf_G_rel by fast
lemma set_spmf_G_L [simp]: "(h,w) ∈ set_spmf G ⟹ h ∈ L"
by (metis mem_Collect_eq set_spmf_G_rel L_def)
text‹We define the advantage associated with the hard relation, this is used in the proof of the binding property where
we reduce the binding advantage to the relation advantage.›
definition rel_game :: "('pub_input ⇒ 'witness spmf) ⇒ bool spmf"
where "rel_game 𝒜 = TRY do {
(h,w) ← G;
w' ← 𝒜 h;
return_spmf ((h,w') ∈ Rel)} ELSE return_spmf False"
definition rel_advantage :: "('pub_input ⇒ 'witness spmf) ⇒ real"
where "rel_advantage 𝒜 ≡ spmf (rel_game 𝒜) True"
text‹We now define the algorithms that define the commitment scheme constructed from a ‹Σ›-protocol.›
definition key_gen :: "('pub_input × ('pub_input × 'witness)) spmf"
where
"key_gen = do {
(x,w) ← G;
return_spmf (x, (x,w))}"
definition commit :: "'pub_input ⇒ 'challenge ⇒ ('msg × 'response) spmf"
where
"commit x e = do {
(a,e,z) ← S x e;
return_spmf (a, z)}"
definition verify :: "('pub_input × 'witness) ⇒ 'challenge ⇒ 'msg ⇒ 'response ⇒ bool"
where "verify x e a z = (check (fst x) a e z)"
text‹We allow the adversary to output any message, so this means the type constraint is enough›
definition "valid_msg m = (m ∈ challenge_space)"
text‹Showing the construction of a commitment scheme from a ‹Σ›-protocol is a valid commitment scheme is trivial.›
sublocale abstract_com: abstract_commitment key_gen commit verify valid_msg .
paragraph‹Correctness›
lemma commit_correct:
shows "abstract_com.correct"
including monad_normalisation
proof-
have "∀ m ∈ challenge_space. abstract_com.correct_game m = return_spmf True"
proof
fix m
assume m: "m ∈ challenge_space"
show "abstract_com.correct_game m = return_spmf True"
proof-
have "abstract_com.correct_game m = do {
(ck, (vk1,vk2)) ← key_gen;
(a,e,z) ← S ck m;
return_spmf (check vk1 a m z)}"
unfolding abstract_com.correct_game_def
by(simp add: commit_def verify_def split_def)
also have "... = do {
(x,w) ← G;
let (ck, (vk1,vk2)) = (x,(x,w));
(a,e,z) ← S ck m;
return_spmf (check vk1 a m z)}"
by(simp add: key_gen_def split_def)
also have "... = do {
(x,w) ← G;
(a,e,z) ← S x m;
return_spmf (check x a m z)}"
by(simp add: Let_def)
also have "... = do {
(x,w) ← G;
(a, e,z) ← R x w m;
return_spmf (check x a m z)}"
using Σ_prot HVZK_unfold1 m
by(intro bind_spmf_cong bind_spmf_cong[OF refl]; clarsimp?)
also have "... = do {
(x,w) ← G;
(r, a) ← init x w;
z ← response r w m;
return_spmf (check x a m z)}"
by(simp add: R_def split_def)
also have "... = do {
(x,w) ← G;
return_spmf True}"
apply(intro bind_spmf_cong bind_spmf_cong[OF refl]; clarsimp?)
using complete_game_return_true lossless_init lossless_response Σ_prot Σ_protocol_def
by(simp add: split_def completeness_game_def Σ_protocols_base.Σ_protocol_def m cong: bind_spmf_cong_simp)
ultimately show "abstract_com.correct_game m = return_spmf True"
by(simp add: bind_spmf_const lossless_G lossless_weight_spmfD split_def)
qed
qed
thus ?thesis
using abstract_com.correct_def abstract_com.valid_msg_set_def valid_msg_def by simp
qed
paragraph‹The hiding property›
text‹We first show we have perfect hiding with respect to the hiding game that allows the adversary to choose
the messages that are committed to, this is akin to the ind-cpa game for encryption schemes.›
lemma perfect_hiding:
shows "abstract_com.perfect_hiding_ind_cpa 𝒜"
including monad_normalisation
proof-
obtain 𝒜1 𝒜2 where [simp]: "𝒜 = (𝒜1, 𝒜2)" by(cases 𝒜)
have "abstract_com.hiding_game_ind_cpa (𝒜1, 𝒜2) = TRY do {
(x,w) ← G;
((m0, m1), σ) ← 𝒜1 (x,w);
_ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
b ← coin_spmf;
(a,e,z) ← S x (if b then m0 else m1);
b' ← 𝒜2 a σ;
return_spmf (b' = b)} ELSE coin_spmf"
by(simp add: abstract_com.hiding_game_ind_cpa_def commit_def; simp add: key_gen_def split_def)
also have "... = TRY do {
(x,w) ← G;
((m0, m1), σ) ← 𝒜1 (x,w);
_ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
b :: bool ← coin_spmf;
(a,e,z) ← R x w (if b then m0 else m1);
b' :: bool ← 𝒜2 a σ;
return_spmf (b' = b)} ELSE coin_spmf"
apply(intro try_spmf_cong bind_spmf_cong[OF refl]; clarsimp?)+
by(simp add: Σ_prot HVZK_unfold1 valid_msg_def)
also have "... = TRY do {
(x,w) ← G;
((m0, m1), σ) ← 𝒜1 (x,w);
_ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
b ← coin_spmf;
(r,a) ← init x w;
z :: 'response ← response r w (if b then m0 else m1);
guess :: bool ← 𝒜2 a σ;
return_spmf(guess = b)} ELSE coin_spmf"
using Σ_protocols_base.R_def
by(simp add: bind_map_spmf o_def R_def split_def)
also have "... = TRY do {
(x,w) ← G;
((m0, m1), σ) ← 𝒜1 (x,w);
_ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
b ← coin_spmf;
(r,a) ← init x w;
guess :: bool ← 𝒜2 a σ;
return_spmf(guess = b)} ELSE coin_spmf"
by(simp add: bind_spmf_const lossless_response lossless_weight_spmfD)
also have "... = TRY do {
(x,w) ← G;
((m0, m1), σ) ← 𝒜1 (x,w);
_ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
(r,a) ← init x w;
guess :: bool ← 𝒜2 a σ;
map_spmf( (=) guess) coin_spmf} ELSE coin_spmf"
apply(simp add: map_spmf_conv_bind_spmf)
by(simp add: split_def)
also have "... = coin_spmf"
by(auto simp add: map_eq_const_coin_spmf try_bind_spmf_lossless2' Let_def split_def bind_spmf_const scale_bind_spmf weight_spmf_le_1 scale_scale_spmf)
ultimately have "spmf (abstract_com.hiding_game_ind_cpa 𝒜) True = 1/2"
by(simp add: spmf_of_set)
thus ?thesis
by (simp add: abstract_com.perfect_hiding_ind_cpa_def abstract_com.hiding_advantage_ind_cpa_def)
qed
text‹We reduce the security of the binding property to the relation advantage. To do this we first construct
an adversary that interacts with the relation game. This adversary succeeds if the binding adversary succeeds.›
definition adversary :: "('pub_input ⇒ ('msg × 'challenge × 'response × 'challenge × 'response) spmf) ⇒ 'pub_input ⇒ 'witness spmf"
where "adversary 𝒜 x = do {
(c, e, ez, e', ez') ← 𝒜 x;
𝒜ss x (c,e,ez) (c,e',ez')}"
lemma bind_advantage:
shows "abstract_com.bind_advantage 𝒜 ≤ rel_advantage (adversary 𝒜)"
proof-
have "abstract_com.bind_game 𝒜 = TRY do {
(x,w) ← G;
(c, m, d, m', d') ← 𝒜 x;
_ :: unit ← assert_spmf (m ≠ m' ∧ m ∈ challenge_space ∧ m' ∈ challenge_space);
let b = check x c m d;
let b' = check x c m' d';
_ :: unit ← assert_spmf (b ∧ b');
w' ← 𝒜ss x (c,m, d) (c,m', d');
return_spmf ((x,w') ∈ Rel)} ELSE return_spmf False"
unfolding abstract_com.bind_game_alt_def
apply(simp add: key_gen_def verify_def Let_def split_def valid_msg_def)
apply(intro try_spmf_cong bind_spmf_cong[OF refl]; clarsimp?)+
using special_soundness_def Σ_prot Σ_protocol_def special_soundness_alt special_soundness_def set_spmf_G_rel set_spmf_G_domain_rel
by (smt basic_trans_rules(31) bind_spmf_cong domain_subset_valid_pub)
hence "abstract_com.bind_advantage 𝒜 ≤ spmf (TRY do {
(x,w) ← G;
(c, m, d, m', d') ← 𝒜 x;
w' ← 𝒜ss x (c,m, d) (c,m', d');
return_spmf ((x,w') ∈ Rel)} ELSE return_spmf False) True"
unfolding abstract_com.bind_advantage_def
apply(simp add: spmf_try_spmf)
apply(rule ord_spmf_eq_leD)
apply(rule ord_spmf_bind_reflI;clarsimp)+
by(simp add: assert_spmf_def)
thus ?thesis
by(simp add: rel_game_def adversary_def split_def rel_advantage_def)
qed
end
end