Port to Lean 4

src/commitments.lean → Cryptolib/Commitments.lean

@@ -1,16 +1,19 @@
 /-
- -----------------------------------------------------------
-  Generic commitments
- -----------------------------------------------------------
+Copyright (c) 2023 Ashley Blacquiere
+Released under either MIT or Apache 2.0 as described in the file README.md.
+Authors: Ashley Blacquiere
+-/
+import Cryptolib.Tactic
+import Cryptolib.ToMathlib
+import Cryptolib.Uniform
+import Mathlib.Data.ZMod.Basic
+import Mathlib.Probability.Distributions.Uniform
+
+/-!
+# Generic commitments
 -/
 
-import data.zmod.basic
-import measure_theory.probability_mass_function
-import to_mathlib
-import uniform
-import tactics
-
-noncomputable theory 
+noncomputable section
 
 /-
   G = The agreed upon group (order q and generator g)
@@ -31,16 +34,16 @@ Verification phase:
 
 /-
 From Boneh & Shoup:
-A security parameter (λ) and system parameter (Λ) are used to index families of key spaces, message spaces and ciphertext spaces. 
+A security parameter (λ) and system parameter (Λ) are used to index families of key spaces, message spaces and ciphertext spaces.
 -/
 
-variables {G M D C A_state : Type} [decidable_eq M]
-          (gen : pmf (G × G) ) -- generates the public parameter, h ∈ G, and secret key a ∈ G
-          (commit : G → M → pmf (C × D) )
-          (verify : G → C → D → M → zmod 2)
-          (BindingAdversary : G → pmf (C × D × D × M × M)) -- how to ensure these are two different Ms?
-          (HidingAdversary1 : G → pmf (M × M × A_state)) -- double check how Lupo handles state
-          (HidingAdversary2 : G → C → A_state → pmf (zmod 2) )
+variable {G M D C A_state : Type} [DecidableEq M]
+         (gen : PMF (G × G) ) -- generates the public parameter, h ∈ G, and secret key a ∈ G
+         (commit : G → M → PMF (C × D) )
+         (verify : G → C → D → M → ZMod 2)
+         (BindingAdversary : G → PMF (C × D × D × M × M)) -- how to ensure these are two different Ms?
+         (HidingAdversary1 : G → PMF (M × M × A_state)) -- double check how Lupo handles state
+         (HidingAdversary2 : G → C → A_state → PMF (ZMod 2) )
 
 /-
 Simulates running the program and returns 1 with prob 1 if verify holds
@@ -50,48 +53,48 @@ Simulates running the program and returns 1 with prob 1 if verify holds
 -/
 
 -- def gen : pmf (G × G) :=
--- do  
+-- do
 
 
-def commit_verify (m : M) : pmf (zmod 2) := -- formerly included a (d : D) parameter
-do 
-  h ← gen, 
-  c ← commit h.1 m, 
+def commit_verify (m : M) : PMF (ZMod 2) := -- formerly included a (d : D) parameter
+do
+  let h ← gen
+  let c ← commit h.1 m
   pure (if verify h.1 c.1 c.2 m = 1 then 1 else 0) --c.2 is the opening value
 
-/- 
-  A commitment protocol is correct if verification undoes 
+/-
+  A commitment protocol is correct if verification undoes
   commitment with probability 1
 
   This was formerly:
-    Prop := ∀ (m : M) (d : D), commit_verify gen commit verify m d = pure 1 
+    Prop := ∀ (m : M) (d : D), commit_verify gen commit verify m d = pure 1
 
   But this should this be ∀m, not ∀m,d? - removed the (d : D) parameter (below) as the opening value is generated by commit and the result is passed to verify
 -/
-def commitment_correctness : Prop := ∀ (m : M), commit_verify gen commit verify m = pure 1 
+def commitment_correctness : Prop := ∀ (m : M), commit_verify gen commit verify m = pure 1
 
 #check commitment_correctness
 
 
 /-
   Binding: "no adversary (either powerful or computationally bounded) can generate c, m = m' and d, d' such that both Verify(c, m, d) and Verify(c, m', d') accept"
 -/
-def BG : pmf (zmod 2) :=
-do 
-  h ← gen, 
-  bc ← BindingAdversary h.1, --pmf (C × D × D × M × M)
+def BG : PMF (ZMod 2) :=
+do
+  let h ← gen
+  let bc ← BindingAdversary h.1 --PMF (C × D × D × M × M)
   -- Def. of binding in B&S pg. 337
   -- As per comment above - how to ensure the Ms are unique?
   -- Verify that both return 1
   -- Commitments are valid commitments to a message
-  let b := verify h.1 bc.1 bc.2.1 bc.2.2.2.1,
-  let b' := verify h.1 bc.1 bc.2.2.1 bc.2.2.2.2,
-  -- let b'' := (if bc.2.2.2.1 = bc.2.2.2.2 
+  let b := verify h.1 bc.1 bc.2.1 bc.2.2.2.1
+  let b' := verify h.1 bc.1 bc.2.2.1 bc.2.2.2.2
+  -- let b'' := (if bc.2.2.2.1 = bc.2.2.2.2
   pure (if bc.2.2.2.1 = bc.2.2.2.2 then 0 else b * b')
-
-local notation `Pr[BG(A)]` := (BG gen verify BindingAdversary 1 : ℝ)
 
-def computational_binding_property (ε : nnreal) : Prop := abs (Pr[BG(A)] - 1/2) ≤ ε 
+local notation "Pr[BG(A)]" => (BG gen verify BindingAdversary 1)
+
+def computational_binding_property (ε : NNReal) : Prop := abs (Pr[BG(A)].toReal - 1/2) ≤ ε
 
 #check computational_binding_property
 
@@ -100,79 +103,73 @@ def computational_binding_property (ε : nnreal) : Prop := abs (Pr[BG(A)] - 1/2)
 
 -- Computational hiding
 
-/- 
+/-
   Hiding: "commitment c does not leak information about m (either perfect secrecy, or computational indistinguishability)"
 -/
 -- Split into two phases: 1. return two M; 2. return bit
 
-def docommit (h : G) (m : M) : pmf C :=
+def docommit (h : G) (m : M) : PMF C :=
 do
-  c ← commit h m, 
+  let c ← commit h m
   pure c.1 -- return just the commit, not the opening value
 
-def docommit' (m : M) : pmf C :=
+def docommit' (m : M) : PMF C :=
 do
-  keypair ← gen,
-  let h := keypair.1,  
-  c ← commit h m, 
+  let keypair ← gen
+  let h := keypair.1
+  let c ← commit h m
   pure c.1
 
 -- Perfect hiding strategy: Use uniformity prop. of group to replace the commit with something completely random
 -- Adv with no knowledge of the message can't guess the message with greater prob than 1/|M|
 -- Any adv that wins the perf. hiding game also wins the message guessing game - contradiction
 -- Breaking the perfect hiding game breaks the impossible message game
--- Perf. hiding as equality between pmfs ∀m1,m2 
--- Pedersen commitments are uniform so equivalence shows 
+-- Perf. hiding as equality between PMFs ∀m1,m2
+-- Pedersen commitments are uniform so equivalence shows
 
 
 -- This is an equality between distributions - how is this proved?
 -- Need probablistic statement to compare two commits
 
 
--- def perfect_hiding_property : Prop := ∀ (h : G) (m1 m2 : M), docommit' gen commit m1 = docommit' gen commit m2 := 
+-- def perfect_hiding_property : Prop := ∀ (h : G) (m1 m2 : M), docommit' gen commit m1 = docommit' gen commit m2 :=
 
-theorem perfect_hiding_property : ∀ (h : G) (m1 m2 : M), docommit' gen commit m1 = docommit' gen commit m2 := 
-begin
-  intros,
-  simp [docommit', bind],
-  bind_skip,
-  sorry,
-end
+theorem perfect_hiding_property : ∀ (h : G) (m1 m2 : M), docommit' gen commit m1 = docommit' gen commit m2 := by
+  intros
+  simp [docommit', bind]
+  bind_skip
+  sorry
 
 
-theorem perfect_hiding_property' : ∀ (h : G) (m1 m2 : M), docommit commit h m1 = docommit commit h m2 :=
-begin
-  intros,
-  simp [docommit, bind, pure],
-  sorry,
-end
+theorem perfect_hiding_property' : ∀ (h : G) (m1 m2 : M), docommit commit h m1 = docommit commit h m2 := by
+  intros
+  simp [docommit, bind, pure]
+  sorry
 
-variables (m : M) (c : C)
+variable (m : M) (c : C)
 #check docommit' gen commit m c
 
-theorem perfect_hiding_property'' : ∀ (h : G) (m1 m2 : M) (c : C), docommit' gen commit m1 c = docommit' gen commit m2 c := 
-begin
-  sorry,
-end
+theorem perfect_hiding_property'' : ∀ (h : G) (m1 m2 : M) (c : C), docommit' gen commit m1 c = docommit' gen commit m2 c := by
+  sorry
 
 #check docommit
-def HG : pmf (zmod 2) := 
-do 
-  hc ← HidingAdversary1,
-  b ← uniform_2,
-  c ← commit hc.b,
-  let b' := A c,
-  pure (if b = b' 1 else 0)
+def HG : PMF (ZMod 2) :=
+do
+  let hc ← HidingAdversary1
+  let b ← uniform_2
+  let c ← commit hc.b
+  let b' := A c
+  pure (if b = b' then 1 else 0)
 
-local `Pr[HG(A)]` := (HG verify HidingAdversary 1 : ℝ) 
+local notation "Pr[HG(A)]" => (HG verify HidingAdversary 1)
 
-#check HG commit HidingAdversary A 
+#check HG commit HidingAdversary A
 
-def computational_hiding_property (ε : nnreal) : Prop := abs (Pr[HG(A)] - 1/2) ≤ ε
+def computational_hiding_property (ε : NNReal) : Prop := abs (Pr[HG(A)].toReal - 1/2) ≤ ε
 
 -- game where adv. generates two messages
 -- commiter commits to one chosen at random
--- opening value has to be an input to commit, but we don't really care what it is (could be a series of coin flips in the process or, could be a random string provided as input) 
+-- opening value has to be an input to commit, but we don't really care what it is (could be a series of coin flips in the process or, could be a random string provided as input)
 
 
 -- Also need perfect hiding

Cryptolib/ComputationalDiffieHellman.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2023 Ashley Blacquiere
+Released under either MIT or Apache 2.0 as described in the file README.md.
+Authors: Ashley Blacquiere
+-/
+import Cryptolib.ToMathlib
+import Cryptolib.Uniform
+import Mathlib.Probability.Distributions.Uniform
+
+/-!
+# The computational Diffie-Hellman assumption as a security game
+-/
+
+noncomputable section
+
+section CDH
+
+variable (G : Type) [Fintype G] [Group G]
+         (g : G) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g)
+         (q : ℕ) [NeZero q] (G_card_q : Fintype.card G = q)
+         (A : G → G → PMF G)
+
+include g_gen_G G_card_q -- assumptions used in the game reduction
+
+def CDH : PMF (ZMod 2) :=
+do
+  let α ← uniform_zmod q
+  let β ← uniform_zmod q
+  let ω := g^(α.val * β.val)
+  let ω' ← A (g^α.val) (g^β.val)
+  pure (if ω = ω' then 1 else 0) -- ??
+
+-- CDHadv[A] is the probability that ω = ω'
+-- Should CDH be a Prop? Not sure how to get both ω and ω' out to compare outside of the def
+local notation "CDHadv[A]" => (CDH G g g_gen_G q G_card_q A)
+
+#check CDH G g /- g_gen_G -/ q /- G_card_q -/ A
+
+end CDH

Cryptolib/DecisionalDiffieHellman.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2021 Joey Lupo
+Released under Apache 2.0 license as described in the file LICENSE-APACHE.
+Authors: Joey Lupo
+-/
+import Cryptolib.ToMathlib
+import Cryptolib.Uniform
+import Mathlib.Probability.Distributions.Uniform
+
+/-!
+# The decisional Diffie-Hellman assumption as a security game
+
+This file provides a formal specification of the decisional Diffie-Hellman assumption on a
+finite cyclic group.
+-/
+
+noncomputable section
+
+section DDH
+
+variable (G : Type) [Fintype G] [Group G]
+         (g : G) --(g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g)
+         (q : ℕ) [NeZero q] --(G_card_q : Fintype.card G = q)
+         -- check Mario, 0 < q necessary for Fintype.card?
+         (D : G → G → G → PMF (ZMod 2))
+
+-- include g_gen_G G_card_q
+
+def DDH0 : PMF (ZMod 2) :=
+do
+  let x ← uniform_zmod q
+  let y ← uniform_zmod q
+  let b ← D (g^x.val) (g^y.val) (g^(x.val * y.val))
+  pure b
+
+def DDH1 : PMF (ZMod 2) :=
+do
+  let x ← uniform_zmod q
+  let y ← uniform_zmod q
+  let z ← uniform_zmod q
+  let b ← D (g^x.val) (g^y.val) (g^z.val)
+  pure b
+
+-- DDH0(D) is the event that D outputs 1 upon receiving (g^x, g^y, g^(xy))
+local notation "Pr[DDH0(D)]" => (DDH0 G g q D 1)
+
+-- DDH1(D) is the event that D outputs 1 upon receiving (g^x, g^y, g^z)
+local notation "Pr[DDH1(D)]" => (DDH1 G g q D 1)
+
+def DDH (ε : NNReal) : Prop := abs (Pr[DDH0(D)].toReal - Pr[DDH1(D)].toReal) ≤ ε
+
+end DDH

Cryptolib/DiscreteLog.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2023 Ashley Blacquiere
+Released under either MIT or Apache 2.0 as described in the file README.md.
+Authors: Ashley Blacquiere
+-/
+import Cryptolib.ToMathlib
+import Cryptolib.Uniform
+import Mathlib.Data.ZMod.Basic
+import Mathlib.Probability.Distributions.Uniform
+
+noncomputable section
+
+section DL
+
+variable (G : Type) [Fintype G] [Group G] [DecidableEq G]
+         (g : G) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g)
+         (q : ℕ) [NeZero q] (G_card_q : Fintype.card G = q)
+         (A : G → PMF (ZMod q))
+
+include g_gen_G G_card_q -- assumptions used in the game reduction
+
+  -- let α ← uniform_zmod q
+  -- let u := g^α.val
+  -- let α' ←  A u
+
+def DL /- (h : G) -/ : PMF (ZMod 2) :=
+do
+  let α ← uniform_zmod q
+  let u := g^α.val
+  let α' ←  A u
+  pure (if α = α' then 1 else 0)
+
+-- -- From DDH:
+-- -- DDH0(D) is the event that D outputs 1 upon receiving (g^x, g^y, g^(xy))
+-- local notation "Pr[DDH0(D)]" => (DDH0 G g g_gen_G q G_card_q D 1)
+
+-- -- DDH1(D) is the event that D outputs 1 upon receiving (g^x, g^y, g^z)
+-- local notation "Pr[DDH1(D)]" => (DDH1 G g g_gen_G q G_card_q D 1)
+
+local notation "Pr[DL(A)]" => (DL G g /- g_gen_G -/ q /- G_card_q -/ A 1)
+
+def DLadv (ε: NNReal) : Prop := abs (Pr[DL(A)].toReal - 1/2) ≤ ε
+
+
+#check DL G g /- g_gen_G -/ q /- G_card_q -/ A
+
+end DL