Skip to content

Commit 6fe9aad

Browse files
ashandoakashandoak
authored
Merge branch 'thesis-edits' into elgamal-binding
2 parents d46a3d8 + 5e564eb commit 6fe9aad

3 files changed

Lines changed: 244 additions & 189 deletions

File tree

‎VerifiedCommitments/CommitmentScheme.lean‎

Lines changed: 66 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -4,76 +4,98 @@ import Mathlib.Probability.ProbabilityMassFunction.Constructions
44
import Mathlib.Probability.Distributions.Uniform
55
import Mathlib.Data.ZMod.Defs
66

7+
/-- A CommitmentScheme is a structure over four spaces:
8+
M: Message space
9+
C: Commitment space
10+
O: Opening value space
11+
K: Key space
12+
13+
And that contains three algorithms:
14+
setup: returns a public parameter and associated randomness
15+
commit: given the public parameter and a message produces a commitment and an opening value
16+
verify: given the public parameter, message and associated commit and opening value returns 1 when the commit opens to the given message and 0 otherwise.-/
717
structure CommitmentScheme (M C O K : Type) where
818
setup : PMF (K × O)
919
commit : K → M → PMF (C × O)
1020
verify : K → M → C → O → ZMod 2
1121

22+
23+
/-- The structure of binding adversary guesses for use in the computational binding game.-/
1224
structure BindingGuess (M C O : Type) where
1325
c : C
1426
m : M
1527
m' : M
1628
o : O
17-
o': O
29+
o' : O
1830

31+
/-- The structure of the hiding adversary for use in the computational hiding game.-/
1932
structure TwoStageAdversary (K M C : Type) where
20-
State : Type
21-
stage1 : K → PMF ((M × M) × State)
22-
stage2 : C → State → PMF (ZMod 2)
33+
state : Type
34+
stage1 : K → PMF ((M × M) × state)
35+
stage2 : C → state → PMF (ZMod 2)
2336

2437
namespace Commitment
2538

26-
noncomputable section
2739
variable {M C O K : Type}
28-
variable (scheme : CommitmentScheme M C O K)
2940

41+
/-- For any public parameters `h` and any message `m` if `commit` outputs a commitment `c` and opening value `o`, then `verify h m c o` accepts with probability 1.-/
3042
def correctness (scheme : CommitmentScheme M C O K) : Prop :=
31-
∀ (h : K) (m : M),
32-
PMF.bind (scheme.commit h m) (fun (commit, opening_val) => pure $ scheme.verify h m commit opening_val) = pure 1
43+
∀ (h : K) (m : M), (scheme.commit h m |>.bind fun (c, o) =>
44+
pure <| scheme.verify h m c o) = pure 1
3345

34-
-- Perfect binding
46+
/-- A commitment scheme with public parameter `h` is perfectly binding if no commitment `c` can be opened to two different messages. For two purported openings `(m,o)` and `(m',o')` both verifying for the same `c`, the messages must be equal (`m = m'`). -/
3547
def perfect_binding (scheme : CommitmentScheme M C O K) : Prop :=
3648
∀ (h : K) (c : C) (m m' : M) (o o' : O),
3749
scheme.verify h m c o = 1 →
38-
scheme.verify h m' c o' = 1 →
39-
m = m'
40-
-- Equivalent to:
41-
--if scheme.verify h m c o = scheme.verify h m' c o' then true else false
42-
43-
-- Computational binding game
44-
-- Security depends on generating the parameters correctly, but at this level probably alright to have the group and generator fixed
45-
-- h should be inside the game, because its unique to a specific run
46-
def comp_binding_game (scheme : CommitmentScheme M C O K)
47-
(A' : K → PMF (BindingGuess M C O)) : PMF $ ZMod 2 :=
48-
open scoped Classical in
49-
PMF.bind scheme.setup (fun (h, _) =>
50-
PMF.bind (A' h) (fun guess =>
51-
if scheme.verify h guess.m guess.c guess.o = 1 ∧ scheme.verify h guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m' then pure 1 else pure 0 ))
52-
53-
def computational_binding [DecidableEq M] (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop :=
54-
∀ (A' : K → PMF (BindingGuess M C O )), comp_binding_game scheme A' 1 ≤ ε
55-
56-
57-
-- Perfect hiding
58-
def do_commit (scheme: CommitmentScheme M C O K) (m : M) : PMF C :=
59-
PMF.bind scheme.setup (fun (h, _) =>
60-
PMF.bind (scheme.commit h m) (fun (c, _) => pure c))
50+
scheme.verify h m' c o' = 1 →
51+
m = m'
6152

53+
/-- A commitment scheme is perfectly hiding if for any messages `m` and `m'`, the induced distribution on commitments is the same. Sampling `h ← setup` and then committing to `m` or `m'` under `h` yields identical commitment distributions. -/
6254
def perfect_hiding (scheme: CommitmentScheme M C O K) : Prop :=
63-
∀ (m m' : M) (c : C), (do_commit scheme m) c = (do_commit scheme m') c
64-
65-
-- Computational hiding game
66-
def comp_hiding_game (scheme : CommitmentScheme M C O K) (A : TwoStageAdversary K M C) :=
67-
PMF.bind scheme.setup (fun (h, _) =>
68-
PMF.bind (A.stage1 h) (fun ((m₀, m₁), state) =>
69-
PMF.bind (PMF.uniformOfFintype (ZMod 2)) (fun b =>
70-
PMF.bind (scheme.commit h (if b = 0 then m₀ else m₁)) (fun (c, _) =>
71-
PMF.bind (A.stage2 c state) (fun b' =>
72-
pure (1 + b + b'))))))
55+
∀ (m m' : M) (c : C),
56+
PMF.bind scheme.setup (fun (h, _) =>
57+
PMF.bind (scheme.commit h m) (fun (c, _) =>
58+
pure c)) c
59+
=
60+
PMF.bind scheme.setup (fun (h, _) =>
61+
PMF.bind (scheme.commit h m') (fun (c, _) =>
62+
pure c)) c
63+
64+
/- Computational Binding -/
65+
66+
/-- For any adversary `A` that accepts `h ← setup` and outputs a single commitment `c` together with two purported openings `(m,o)` and `(m',o')`, the computational binding game outputs `1` if `c` opens to both `(m,o)` and `(m',o') and the messages differ (`m ≠ m'`). -/
67+
noncomputable def comp_binding_game
68+
[DecidableEq M] (scheme : CommitmentScheme M C O K)
69+
(A : K → PMF (BindingGuess M C O)) : PMF (ZMod 2) := do
70+
let (h, _) ← scheme.setup
71+
let guess ← A h
72+
pure (
73+
if scheme.verify h guess.m guess.c guess.o = 1 ∧
74+
scheme.verify h guess.m' guess.c guess.o' = 1 ∧
75+
guess.m ≠ guess.m'
76+
then 1 else 0 )
77+
78+
/-- A commitment scheme is computationally binding if every adversary’s probability of winning the computational binding game is at most `ε`. -/
79+
def computational_binding [DecidableEq M] (scheme : CommitmentScheme M C O K)
80+
(ε : ENNReal) : Prop :=
81+
∀ (A' : K → PMF (BindingGuess M C O )), comp_binding_game scheme A' 1 ≤ ε
7382

83+
/- Computational Hiding -/
84+
85+
/-- For any `TwoStageAdversary` `A`, sample `h ← setup` and give `h` to the adversary’s first stage to produce two challenge messages `m₀, m₁. The computational hiding game samples a uniform bit `b`, computes a commitment to `m_b`, and gives the commitment `c` to the adversary’s second stage. The game outputs a bit indicating whether the adversary’s guess matches `b`. -/
86+
noncomputable def comp_hiding_game
87+
(scheme : CommitmentScheme M C O K)
88+
(A : TwoStageAdversary K M C) := do
89+
let (h, _) ← scheme.setup
90+
let ((m₀, m₁), state) ← A.stage1 h
91+
let b ← PMF.uniformOfFintype (ZMod 2)
92+
let (c, _) ← scheme.commit h (if b = 0 then m₀ else m₁)
93+
let b' ← A.stage2 c state
94+
pure (1 + b + b')
95+
96+
/-- A commitment scheme is computationally hiding if every adversary’s advantage
97+
over random guessing in the hiding game is at most `ε`. -/
7498
def computational_hiding (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop :=
7599
∀ (A : TwoStageAdversary K M C), comp_hiding_game scheme A 1 - 1/2 ≤ ε
76100

77-
end
78-
79101
end Commitment

‎VerifiedCommitments/ElgamalCommitments.lean‎

Lines changed: 42 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -1,52 +1,12 @@
11
-- From cryptolib licensed under Apache 2.0
22
-- https://github.com/joeylupo/cryptolib
33

4-
/-
5-
-----------------------------------------------------------
6-
Correctness and semantic security of ElGamal public-key
7-
encryption scheme
8-
-----------------------------------------------------------
9-
-/
10-
11-
import Mathlib
124
import VerifiedCommitments.cryptolib
135
import VerifiedCommitments.CommitmentScheme
146

15-
namespace DDH
16-
17-
variable (G : Type) [Fintype G] [Group G]
18-
(g : G) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g)
19-
(q : ℕ) [NeZero q] [Fact (0 < q)] (G_card_q : Fintype.card G = q)
20-
(D : G → G → G → PMF (ZMod 2))
21-
22-
include g_gen_G G_card_q
23-
24-
instance : Fintype (ZMod q) := ZMod.fintype q
25-
26-
noncomputable def Game0 : PMF (ZMod 2) :=
27-
do
28-
let x ← PMF.uniformOfFintype (ZMod q)
29-
let y ← PMF.uniformOfFintype (ZMod q)
30-
let b ← D (g^x.val) (g^y.val) (g^(x.val * y.val))
31-
pure b
32-
33-
noncomputable def Game1 : PMF (ZMod 2) :=
34-
do
35-
let x ← PMF.uniformOfFintype (ZMod q)
36-
let y ← PMF.uniformOfFintype (ZMod q)
37-
let z ← PMF.uniformOfFintype (ZMod q)
38-
let b ← D (g^x.val) (g^y.val) (g^z.val)
39-
pure b
40-
41-
-- DDH0(D) is the event that D outputs 1 upon receiving (g^x, g^y, g^(xy))
42-
-- local notation `Pr[DDH0(D)]` := (DDH0 G g g_gen_G q G_card_q D 1 : ℝ)
43-
44-
-- DDH1(D) is the event that D outputs 1 upon receiving (g^x, g^y, g^z)
45-
-- local notation `Pr[DDH1(D)]` := (DDH1 G g g_gen_G q G_card_q D 1 : ℝ)
46-
47-
def Assumption (ε : ENNReal) : Prop := (Game0 G g q D 1) - (Game1 G g q D 1) ≤ ε
48-
49-
end DDH
7+
/- ========================================
8+
PUBLIC PARAMETERS
9+
======================================== -/
5010

5111
namespace Elgamal
5212

@@ -67,7 +27,11 @@ variable {G : Type} [params : PublicParameters G]
6727
instance : DecidableEq G := params.decidable_G
6828
instance : Fact (Nat.Prime params.q) := ⟨params.prime_q⟩
6929

70-
noncomputable def setup : PMF (G × ZMod params.q) := -- Need to include x to match CommitmentScheme spec
30+
/- ========================================
31+
SCHEME DEFINITION
32+
======================================== -/
33+
34+
noncomputable def setup : PMF (G × ZMod params.q) :=
7135
do
7236
let x ← PMF.uniformOfFintype (ZMod params.q)
7337
return (params.g^x.val, x)
@@ -85,11 +49,9 @@ noncomputable def scheme : CommitmentScheme G (G × G) (ZMod params.q) G where
8549
commit := commit
8650
verify := verify
8751

88-
/-
89-
-----------------------------------------------------------
90-
Proof of correctness of ElGamal
91-
-----------------------------------------------------------
92-
-/
52+
/- ========================================
53+
CORRECTNESS
54+
======================================== -/
9355

9456
theorem elgamal_commitment_correctness : Commitment.correctness (@scheme G params) := by
9557
intro h m
@@ -98,6 +60,37 @@ theorem elgamal_commitment_correctness : Commitment.correctness (@scheme G param
9860
unfold commit verify
9961
simp only [bind_pure_comp, Functor.map, PMF.bind_bind, Function.comp_apply, PMF.pure_bind, ↓reduceIte, PMF.bind_const]
10062

63+
/- ========================================
64+
DDH EXPERIMENT
65+
======================================== -/
66+
67+
namespace DDH
68+
69+
variable (G : Type) [Fintype G] [Group G]
70+
(g : G) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g)
71+
(q : ℕ) [NeZero q] [Fact (0 < q)] (G_card_q : Fintype.card G = q)
72+
(D : G → G → G → PMF (ZMod 2))
73+
74+
include g_gen_G G_card_q
75+
76+
noncomputable def Game0 : PMF (ZMod 2) :=
77+
do
78+
let x ← PMF.uniformOfFintype (ZMod q)
79+
let y ← PMF.uniformOfFintype (ZMod q)
80+
let b ← D (g^x.val) (g^y.val) (g^(x.val * y.val))
81+
pure b
82+
83+
noncomputable def Game1 : PMF (ZMod 2) :=
84+
do
85+
let x ← PMF.uniformOfFintype (ZMod q)
86+
let y ← PMF.uniformOfFintype (ZMod q)
87+
let z ← PMF.uniformOfFintype (ZMod q)
88+
let b ← D (g^x.val) (g^y.val) (g^z.val)
89+
pure b
90+
91+
def Assumption (ε : ENNReal) : Prop := (Game0 G g q D 1) - (Game1 G g q D 1) ≤ ε
92+
93+
end DDH
10194

10295
/-
10396
-----------------------------------------------------------

0 commit comments

Comments
 (0)