Theory Commitment_Schemes
section‹Commitment Schemes›
text‹A commitment scheme is a two party Cryptographic protocol run between a committer and a verifier.
They allow the committer to commit to a chosen value while at a later time reveal the value. A commitment
scheme is composed of three algorithms, the key generation, the commitment and the verification algorithms.
The two main properties of commitment schemes are hiding and binding.›
text‹Hiding is the property that the commitment leaks no information about the committed value, and
binding is the property that the committer cannot reveal their a different message to the one they
committed to; that is they are bound to their commitment. We follow the game based approach \<^cite>‹"DBLP:journals/iacr/Shoup04"› to
define security. A game is played between an adversary and a challenger.›
theory Commitment_Schemes imports
CryptHOL.CryptHOL
begin
subsection‹Defining security›
text‹Here we define the hiding, binding and correctness properties of commitment schemes.›
text‹We provide the types of the adversaries that take part in the hiding and binding games. We consider
two variants of the hiding property, one stronger than the other --- thus we provide two hiding adversaries.
The first hiding property we consider is analogous to the IND-CPA property for encryption schemes, the second,
weaker notion, does not allow the adversary to choose the messages used in the game, instead they are sampled
from a set distribution.›
type_synonym ('vk', 'plain', 'commit', 'state) hid_adv =
"('vk' ⇒ (('plain' × 'plain') × 'state) spmf)
× ('commit' ⇒ 'state ⇒ bool spmf)"
type_synonym 'commit' hid = "'commit' ⇒ bool spmf"
type_synonym ('ck', 'plain', 'commit', 'opening') bind_adversary =
"'ck' ⇒ ('commit' × 'plain' × 'opening' × 'plain' × 'opening') spmf"
text‹We fix the algorithms that make up a commitment scheme in the locale.›
locale abstract_commitment =
fixes key_gen :: "('ck × 'vk) spmf"
and commit :: "'ck ⇒ 'plain ⇒ ('commit × 'opening) spmf"
and verify :: "'vk ⇒ 'plain ⇒ 'commit ⇒ 'opening ⇒ bool"
and valid_msg :: "'plain ⇒ bool"
begin
definition "valid_msg_set = {m. valid_msg m}"
definition lossless :: "('pub_key, 'plain, 'commit, 'state) hid_adv ⇒ bool"
where "lossless 𝒜 ⟷
((∀pk. lossless_spmf (fst 𝒜 pk)) ∧
(∀commit σ. lossless_spmf (snd 𝒜 commit σ)))"
text‹The correct game runs the three algorithms that make up commitment schemes and outputs the output
of the verification algorithm.›
definition correct_game :: "'plain ⇒ bool spmf"
where "correct_game m = do {
(ck, vk) ← key_gen;
(c,d) ← commit ck m;
return_spmf (verify vk m c d)}"
lemma "⟦ lossless_spmf key_gen; lossless_spmf TI;
⋀pk m. valid_msg m ⟹ lossless_spmf (commit pk m) ⟧
⟹ valid_msg m ⟹ lossless_spmf (correct_game m)"
by(simp add: lossless_def correct_game_def split_def Let_def)
definition correct where "correct ≡ (∀m. valid_msg m ⟶ spmf (correct_game m) True = 1)"
text‹The hiding property is defined using the hiding game. Here the adversary is asked to output two
messages, the challenger flips a coin to decide which message to commit and hand to the adversary.
The adversary's challenge is to guess which commitment it was handed. Note we must check the two
messages outputted by the adversary are valid.›
primrec hiding_game_ind_cpa :: "('vk, 'plain, 'commit, 'state) hid_adv ⇒ bool spmf"
where "hiding_game_ind_cpa (𝒜1, 𝒜2) = TRY do {
(ck, vk) ← key_gen;
((m0, m1), σ) ← 𝒜1 vk;
_ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
b ← coin_spmf;
(c,d) ← commit ck (if b then m0 else m1);
b' :: bool ← 𝒜2 c σ;
return_spmf (b' = b)} ELSE coin_spmf"
text‹The adversary wins the game if ‹b = b'›.›
lemma lossless_hiding_game:
"⟦ lossless 𝒜; lossless_spmf key_gen;
⋀pk plain. valid_msg plain ⟹ lossless_spmf (commit pk plain) ⟧
⟹ lossless_spmf (hiding_game_ind_cpa 𝒜)"
by(auto simp add: lossless_def hiding_game_ind_cpa_def split_def Let_def)
text‹To define security we consider the advantage an adversary has of winning the game over a tossing
a coin to determine their output.›
definition hiding_advantage_ind_cpa :: "('vk, 'plain, 'commit, 'state) hid_adv ⇒ real"
where "hiding_advantage_ind_cpa 𝒜 ≡ ¦spmf (hiding_game_ind_cpa 𝒜) True - 1/2¦"
definition perfect_hiding_ind_cpa :: "('vk, 'plain, 'commit, 'state) hid_adv ⇒ bool"
where "perfect_hiding_ind_cpa 𝒜 ≡ (hiding_advantage_ind_cpa 𝒜 = 0)"
text‹The binding game challenges an adversary to bind two messages to the same committed value. Both
opening values and messages are verified with respect to the same committed value, the adversary wins
if the game outputs true. We must check some conditions of the adversaries output are met;
we will always require that ‹m ≠ m'›, other conditions will be dependent on the protocol for example
we may require group or field membership.›
definition bind_game :: "('ck, 'plain, 'commit, 'opening) bind_adversary ⇒ bool spmf"
where "bind_game 𝒜 = TRY do {
(ck, vk) ← key_gen;
(c, m, d, m', d') ← 𝒜 ck;
_ :: unit ← assert_spmf (m ≠ m' ∧ valid_msg m ∧ valid_msg m');
let b = verify vk m c d;
let b' = verify vk m' c d';
return_spmf (b ∧ b')} ELSE return_spmf False"
text‹We proof the binding game is equivalent to the following game which is easier to work with. In particular
we assert b and b' in the game and return True.›
lemma bind_game_alt_def:
"bind_game 𝒜 = TRY do {
(ck, vk) ← key_gen;
(c, m, d, m', d') ← 𝒜 ck;
_ :: unit ← assert_spmf (m ≠ m' ∧ valid_msg m ∧ valid_msg m');
let b = verify vk m c d;
let b' = verify vk m' c d';
_ :: 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, m, d, m', d') ← 𝒜 ck;
TRY do {
_ :: unit ← assert_spmf (m ≠ m' ∧ valid_msg m ∧ valid_msg m');
TRY return_spmf (verify vk m c d ∧ verify vk m' c d') 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, m, d, m', d') ← 𝒜 ck;
TRY do {
_ :: unit ← assert_spmf (m ≠ m' ∧ valid_msg m ∧ valid_msg m');
TRY do {
_ :: unit ← assert_spmf (verify vk m c d ∧ verify vk m' c d');
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
lemma lossless_binding_game: "lossless_spmf (bind_game 𝒜)"
by (simp add: bind_game_def)
definition bind_advantage :: "('ck, 'plain, 'commit, 'opening) bind_adversary ⇒ real"
where "bind_advantage 𝒜 ≡ spmf (bind_game 𝒜) True"
end
end