diff --git a/Cryptolib/Block.lean b/Cryptolib/Block.lean new file mode 100644 index 0000000..fa0b5e1 --- /dev/null +++ b/Cryptolib/Block.lean @@ -0,0 +1,50 @@ +/- + ----------------------------------------------------------- + Formalization and correctness of block ciphers + ----------------------------------------------------------- +-/ + +import Mathlib.Data.Matrix.Basic +import Mathlib.Data.ZMod.Basic +import Mathlib.LinearAlgebra.Matrix.NonsingularInverse + +open scoped Matrix + +namespace Hill + +/-! +# Hill cipher: A generalization of the affine cipher + +If block = 2 then this is a digraphic cipher. +If block > 2 then this is a poligraphic cipher. +If block = 1 then this is a reduction to the affine cipher. +-/ + +-- All operations will be mod 26 (English language character set). +def m : ℕ := 26 + +-- The size of the block +variable (block : ℕ) + +-- The key matrix +variable (A : Matrix (Fin block) (Fin block) (ZMod m)) + +-- The plaintext vector +variable (P : Matrix (Fin block) (Fin 1) (ZMod m)) + +-- The ciphertext vector +variable (C : Matrix (Fin block) (Fin 1) (ZMod m)) + +-- Encryption +def encrypt : (Matrix (Fin block) (Fin 1) (ZMod m)) := A * P + +-- Decryption +noncomputable def decrypt : (Matrix (Fin block) (Fin 1) (ZMod m)) := A⁻¹ * P + +-- Proof of correctness +lemma dec_undoes_enc (h : A.det = 1): P = decrypt block A (encrypt block A P) := by + unfold encrypt + unfold decrypt + simp_all only [isUnit_one, Matrix.nonsing_inv_mul_cancel_left] + +end Hill diff --git a/src/commitments.lean b/Cryptolib/Commitments.lean similarity index 59% rename from src/commitments.lean rename to Cryptolib/Commitments.lean index 962b4be..21825ed 100644 --- a/src/commitments.lean +++ b/Cryptolib/Commitments.lean @@ -1,16 +1,19 @@ /- - ----------------------------------------------------------- - Generic commitments - ----------------------------------------------------------- +Copyright (c) 2023 Ashley Blacquiere +Released under Apache 2.0 license as described in the file LICENSE-APACHE. +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,25 +53,25 @@ 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 @@ -76,22 +79,22 @@ def commitment_correctness : Prop := ∀ (m : M), commit_verify gen commit verif /- 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 diff --git a/Cryptolib/ComputationalDiffieHellman.lean b/Cryptolib/ComputationalDiffieHellman.lean new file mode 100644 index 0000000..1cb252b --- /dev/null +++ b/Cryptolib/ComputationalDiffieHellman.lean @@ -0,0 +1,39 @@ +/- +Copyright (c) 2023 Ashley Blacquiere +Released under Apache 2.0 license as described in the file LICENSE-APACHE. +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 diff --git a/Cryptolib/DecisionalDiffieHellman.lean b/Cryptolib/DecisionalDiffieHellman.lean new file mode 100644 index 0000000..4863d44 --- /dev/null +++ b/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 diff --git a/Cryptolib/DiscreteLog.lean b/Cryptolib/DiscreteLog.lean new file mode 100644 index 0000000..d616709 --- /dev/null +++ b/Cryptolib/DiscreteLog.lean @@ -0,0 +1,47 @@ +/- +Copyright (c) 2023 Ashley Blacquiere +Released under Apache 2.0 license as described in the file LICENSE-APACHE. +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 diff --git a/Cryptolib/ElGamal.lean b/Cryptolib/ElGamal.lean new file mode 100644 index 0000000..87e2d50 --- /dev/null +++ b/Cryptolib/ElGamal.lean @@ -0,0 +1,419 @@ +/- +Copyright (c) 2021 Joey Lupo +Released under Apache 2.0 license as described in the file LICENSE-APACHE. +Authors: Joey Lupo +-/ +import Cryptolib.DecisionalDiffieHellman +import Cryptolib.PublicKeyEncryption +import Cryptolib.Tactic +import Cryptolib.ToMathlib +import Cryptolib.Uniform +import Mathlib.Tactic.Cases + +/-! +# Correctness and semantic security of ElGamal public-key encryption scheme + +This file contains the formal specification of the ElGamal public key encryption protocol, +and the formal proofs of correctness. +-/ + +section ElGamal + +noncomputable section + +variable (G : Type) [Fintype G] [CommGroup G] [DecidableEq G] + (g : G) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g) + (q : ℕ) [NeZero q] [Group (ZMod q)] (G_card_q : Fintype.card G = q) + (A_state : Type) + +include g_gen_G G_card_q + +variable (A1 : G → PMF (G × G × A_state)) + (A2 : G → G → A_state → PMF (ZMod 2)) + +def A2' : G × G → A_state → PMF (ZMod 2) := λ (gg : G × G) => A2 gg.1 gg.2 + +-- generates a public key `g^x.val`, and private key `x` +def keygen : PMF (G × (ZMod q)) := +do + let x ← uniform_zmod q + pure (g^x.val, x) + +#check keygen +-- encrypt takes a pair (public key, message) +def encrypt (pk m : G) : PMF (G × G) := +do + let y ← uniform_zmod q + pure (g^y.val, pk^y.val * m) + +-- `x` is the secret key, `c.1` is g^y, the first part of the +-- cipher text returned from encrypt, and `c.2` is the +-- second value returned from encrypt +def decrypt (x : ZMod q)(c : G × G) : G := + (c.2 / (c.1^x.val)) + +/- + ----------------------------------------------------------- + Proof of correctness of ElGamal + ----------------------------------------------------------- +-/ + +lemma decrypt_eq_m (m : G) (x y: ZMod q) : + decrypt G /- g g_gen_G -/ q /- G_card_q -/ x ((g^y.val), ((g^x.val)^y.val * m)) = m := by + simp [decrypt] + rw [(pow_mul g x.val y.val).symm] + rw [(pow_mul g y.val x.val).symm] + rw [mul_comm y.val x.val] + rw [div_eq_mul_inv] + rw [mul_assoc, mul_comm m _, <- mul_assoc, mul_inv_cancel _] + exact one_mul m + +-- set_option trace.ext true +-- set_option trace.simplify true + + +theorem elgamal_correctness : PkeCorrectness (keygen G g /- g_gen_G -/ q /- G_card_q -/) (encrypt G g /- g_gen_G -/ q /- G_card_q -/) (decrypt G /- g g_gen_G -/ q /- G_card_q -/) := by + -- simp_intros [PkeCorrectness] + simp [PkeCorrectness] + -- intro m + -- simp [enc_dec, keygen, encrypt, bind] + -- bind_skip_const with x + -- simp [pure] + -- bind_skip_const with y + simp [enc_dec, keygen, encrypt, bind, pure] + simp_rw [decrypt_eq_m] + simp only [eq_self_iff_true, if_true] + + + +/- + ----------------------------------------------------------- + Proof of semantic security of ElGamal + ----------------------------------------------------------- +-/ + +def D (gx gy gz : G) : PMF (ZMod 2) := +do + let m ← A1 gx -- give G, g, q, h_1 (gx) to A1 and run to get two messages + let b ← uniform_2 -- choose b uniformly + let mb ← pure (if b = 0 then m.1 else m.2.1) + let b' ← A2 gy (gz * mb) m.2.2 -- Katz & Lindell theorem 12.18 (elgamal) + pure (1 + b + b') -- output the same bit - means it was able to break the encryption + +/- + The probability of the attacker (i.e. the composition of A1 and A2) + winning the semantic security game (i.e. guessing the correct bit), + w.r.t. ElGamal is equal to the probability of D winning the game DDH0. +-/ + + +theorem SSG_DDH0 : SSG (keygen G g /- g_gen_G -/ q /- G_card_q -/) (encrypt G g /- g_gen_G -/ q /- G_card_q -/) A1 (A2' G /- g g_gen_G q G_card_q -/ A_state A2) = DDH0 G g /- g_gen_G -/ q /- G_card_q -/ (D G /- g g_gen_G q G_card_q -/ A_state A1 A2) := by + simp only [SSG, DDH0, bind, keygen, encrypt, D] + simp_rw [PMF.bind_bind (uniform_zmod q)] + bind_skip with x + simp [pure] + simp_rw [PMF.bind_comm (uniform_zmod q)] + bind_skip with m + bind_skip with b + bind_skip with y + simp only [A2'] + rw [pow_mul g x.val y.val] + + +def Game1 : PMF (ZMod 2) := +do + let x ← uniform_zmod q + let y ← uniform_zmod q + let m ← A1 (g^x.val) + let b ← uniform_2 + let ζ ← (do let z ← uniform_zmod q; let mb ← pure (if b = 0 then m.1 else m.2.1); pure (g^z.val * mb)) + let b' ← A2 (g^y.val) ζ m.2.2 + pure (1 + b + b') + +def Game2 : PMF (ZMod 2) := +do + let x ← uniform_zmod q + let y ← uniform_zmod q + let m ← A1 (g^x.val) + let b ← uniform_2 + let ζ ← (do let z ← uniform_zmod q; pure (g^z.val)) + let b' ← A2 (g^y.val) ζ m.2.2 + pure (1 + b + b') + +/- + The probability of the attacker (i.e. the composition of A1 and A2) + winning Game1 (i.e. guessing the correct bit) is equal to the + probability of D winning the game DDH1. +-/ + +theorem Game1_DDH1 : (Game1 G g /- g_gen_G -/ q /- G_card_q -/ A_state A1 A2) = DDH1 G g /- g_gen_G -/ q /- G_card_q -/ (D G /- g g_gen_G q G_card_q -/ A_state A1 A2) := by + simp only [DDH1, Game1, bind, D] + bind_skip with x + bind_skip with y + simp_rw [PMF.bind_bind (A1 _)] + -- conv_rhs {rw [PMF.bind_comm (uniform_zmod q)]} + bind_skip with m + simp_rw [PMF.bind_bind (uniform_zmod q)] + -- conv_lhs {rw [PMF.bind_comm (uniform_2)]} + bind_skip with z + -- conv_rhs {rw [PMF.bind_bind (uniform_2)]} + bind_skip with b + simp_rw [PMF.bind_bind] + bind_skip with mb + simp [pure] + +lemma exp_bij : + Function.Bijective (λ (z : ZMod q) => g ^ z.val) := by + apply (Fintype.bijective_iff_surjective_and_card _).mpr + constructor + + { -- (λ (z : ZMod q) => g ^ z.val) surjective + intro gz + have hz := Subgroup.mem_zpowers_iff.mp (g_gen_G gz) + cases' hz with z hz + cases' z + + { -- Case : z = z' for (z : ℕ) + let zq := z % q + use zq + have h1 : (λ (z : ZMod q) => g ^ z.val) ↑zq = g ^ (zq : ZMod q).val := rfl + rw [h1] + rw [ZMod.val_cast_of_lt] + { + have goal : gz = g ^ zq := + calc + gz = g ^ Int.of_nat z := hz.symm + _ = g ^ z := by simp + _ = g ^ (z % q + q * (z / q)) := by rw [Nat.mod_add_div z q] + _ = g ^ (z % q) * g ^ (q * (z / q)) := by rw [pow_add] + _ = g ^ (z % q) * (g ^ q) ^ (z / q) := by rw [pow_mul] + _ = g ^ (z % q) * (g ^ Fintype.card G) ^ (z / q) := by rw [<- G_card_q] + _ = g ^ (z % q) := by simp [pow_card_eq_one] + _ = g ^ zq := rfl + exact goal.symm + } + exact Nat.mod_lt z (Nat.pos_of_ne_zero _inst_4.out) + } + + { -- Case : z = - (1 + z') for (z' : ℕ) + let zq := (q - (z + 1) % q ) % q + use zq + have h1 : (λ (z : ZMod q) => g ^ z.val) ↑zq = g ^ (zq : ZMod q).val := rfl + rw [h1] + rw [ZMod.val_cast_of_lt] + { + have h1 : (z + 1) % q ≤ Fintype.card G := by + rw [G_card_q] + apply le_of_lt + exact Nat.mod_lt _ (Nat.pos_of_ne_zero _inst_4.out) + + have goal : gz = g ^ zq := + calc + gz = g ^ Int.neg_succ_of_nat z := hz.symm + _ = (g ^ z.succ)⁻¹ := by rw [zpow_neg_succ_of_nat] + _ = (g ^ (z + 1))⁻¹ := rfl + _ = (g ^ ((z + 1) % Fintype.card G))⁻¹ := by rw [pow_eq_mod_card (z + 1)] + _ = (g ^ ((z + 1) % q))⁻¹ := by rw [G_card_q] + _ = g ^ (Fintype.card G - (z + 1) % q) := inv_pow_eq_card_sub_pow G g _ h1 + _ = g ^ (q - ((z + 1) % q)) := by rw [G_card_q] + _ = g ^ ((q - (z + 1) % q) % q + + q * ((q - (z + 1) % q) / q)) := by rw [Nat.mod_add_div] + _ = g ^ ((q - (z + 1) % q) % q) + * g ^ (q * ((q - (z + 1) % q) / q)) := by rw [pow_add] + _ = g ^ ((q - (z + 1) % q) % q) + * (g ^ q) ^ ((q - (z + 1) % q) / q) := by rw [pow_mul] + _ = g ^ ((q - (z + 1) % q) % q) + * (g ^ Fintype.card G) ^ ((q - (z + 1) % q) / q) := by rw [<- G_card_q] + _ = g ^ ((q - (z + 1) % q) % q) := by simp [pow_card_eq_one] + _ = g ^ zq := rfl + exact goal.symm + } + + exact Nat.mod_lt _ (Nat.pos_of_ne_zero _inst_4.out) + } + } + + { -- Fintype.card (ZMod q) = Fintype.card G + rw [G_card_q] + exact ZMod.card q + } + +lemma exp_mb_bij (mb : G) : Function.Bijective (λ (z : ZMod q) => g ^ z.val * mb) := by + have h : + (λ (z : ZMod q) => g ^ z.val * mb) = + ((λ (m : G) => (m * mb)) ∘ (λ (z : ZMod q) => g ^ z.val)) := by + simp + rw [h] + apply Function.Bijective.comp + + { -- (λ (m : G), (m * mb)) bijective + refine Finite.injective_iff_bijective.mp _ + intros x a hxa + simp at hxa + exact hxa + } + + { -- (λ (z : ZMod q), g ^ z.val) bijective + exact exp_bij G g g_gen_G q G_card_q + } + +lemma G1_G2_lemma1 (x : G) (exp : ZMod q → G) (exp_bij : Function.Bijective exp) : + ∑' (z : ZMod q), ite (x = exp z) (1 : NNReal) 0 = 1 := by + have inv := Function.bijective_iff_has_inverse.mp exp_bij + cases' inv with exp_inv + have bij_eq : ∀ (z : ZMod q), (x = exp z) = (z = exp_inv x) := by + intro z + simp + constructor + + { -- (x = exp z) → (z = exp_inv x) + intro h + have h1 : exp_inv x = exp_inv (exp z) := congr_arg exp_inv h + rw [inv_h.left z] at h1 + exact h1.symm + } + + { -- (z = exp_inv x) → (x = exp z) + intro h + have h2 : exp z = exp (exp_inv x) := congr_arg exp h + rw [inv_h.right x] at h2 + exact h2.symm + } + simp_rw [bij_eq] + simp + +lemma G1_G2_lemma2 (mb : G) : + (uniform_zmod q).bind (λ (z : ZMod q) => pure (g^z.val * mb)) = + (uniform_zmod q).bind (λ (z : ZMod q) => pure (g^z.val)) := by + simp [PMF.bind] + simp_rw [uniform_zmod_prob] + apply funext + intro + -- ext + simp only [pure] + simp only [PMF.pure] + simp only [coe_fn] + simp only [has_coe_to_fun.coe] + simp only [fun_like.coe] + simp only [ennreal.tsum_mul_left] + -- simp only [pure, PMF.pure, coe_fn, has_coe_to_fun.coe, nnreal.tsum_mul_left] + norm_cast + simp + rw [@mul_eq_mul_left_iff ennreal ↑q _ _] + simp only [one_div, mul_eq_mul_left_iff, inv_eq_zero, nat.cast_eq_zero] + simp only [one_div] + congr 2 + intros + -- simp_rw [mul_eq_mul_left_iff] at * -- Seems that this is not going to the same depth as the same tactic in 3.3? There is an extra simplification step in the 3.3 version that seems to reach the intended target + simp + simp only [inv_eq_zero] + simp only [nat.cast_eq_zero] -- added trace.simplify true - must be something in here... + apply or.intro_left -- tried apply iff.intro here, but that seems like maybe a deadend... + repeat {rw [G1_G2_lemma1 x]} + rw [G1_G2_lemma1 _ _ (exp_mb_bij mb)] + intros + exact exp_mb_bij mb + +#check exp_bij +#check G1_G2_lemma1 _ _ (exp_mb_bij _) +#check G1_G2_lemma1 +#check exp_mb_bij + +lemma G1_G2_lemma3 (m : PMF G) : + m.bind (λ (mb : G) => (uniform_zmod q).bind (λ (z : ZMod q) => pure (g^z.val * mb))) = + (uniform_zmod q).bind (λ (z : ZMod q) => pure (g^z.val)) := by + simp_rw [G1_G2_lemma2 _] + bind_skip_const with m + congr + +/- + The probability of the attacker (i.e. the composition of A1 and A2) + winning Game1 (i.e. guessing the correct bit) is equal to the + probability of the attacker winning Game2. +-/ +theorem Game1_Game2 : Game1 = Game2 := by + simp only [Game1, Game2] + bind_skip with x + bind_skip with y + bind_skip with m + bind_skip with b + simp [bind, -PMF.bind_pure, -PMF.bind_bind] + simp_rw [PMF.bind_comm (uniform_zmod q)] + rw [G1_G2_lemma3] + +lemma G2_uniform_lemma (b' : ZMod 2) : + uniform_2.bind (λ (b : ZMod 2) => pure (1 + b + b')) = uniform_2 := by + fin_cases b' + + . -- b = 0 + ring_nf + ext + simp [uniform_2] + rw [uniform_zmod_prob] -- a + simp_rw [uniform_zmod_prob] + simp [NNReal.tsum_mul_left] + have zmod_eq_comm : ∀ (x : ZMod 2), (a = 1 + x) = (x = 1 + a) := by + intro x + fin_cases a + + . -- a = 0 + fin_cases x with [0,1] + simp + + . -- a = 1 + fin_cases x with [0,1] + simp [if_pos] + have h : ∑' (x : ZMod 2), (pure (1 + x) : PMF (ZMod 2)) a = 1 := by + simp [pure, PMF.pure, coe_fn, has_coe_to_fun.coe] + simp_rw [zmod_eq_comm] + simp + rw [h] + simp + + . -- b = 1 + ring_nf + simp + have h : + uniform_2.bind (λ (b : ZMod 2) => pure (b + 0)) = uniform_2 := by simp [pure] + exact h + +/- + The probability of the attacker (i.e. the composition of A1 and A2) + winning Game2 (i.e. guessing the correct bit) is equal to a coin flip. +-/ +theorem Game2_uniform : Game2 = uniform_2 := by + simp [Game2, bind] + bind_skip_const with x + bind_skip_const with m + bind_skip_const with y + rw [PMF.bind_comm uniform_2] + simp_rw [PMF.bind_comm uniform_2] + bind_skip_const with z + bind_skip_const with ζ + bind_skip_const with b' + exact G2_uniform_lemma b' + +variable (ε : NNReal) + +/- + The advantage of the attacker (i.e. the composition of A1 and A2) in + the semantic security game `ε` is exactly equal to the advantage of D in + the Diffie-Hellman game. Therefore, assumining the decisional Diffie-Hellman + assumption holds for the group `G`, we conclude `ε` is negligble, and + therefore ElGamal is, by definition, semantically secure. +-/ +theorem elgamal_semantic_security (DDH_G : DDH G g /- g_gen_G -/ q /- G_card_q -/ D ε) : + PkeSemanticSecurity keygen encrypt A1 A2' ε := by + simp only [PkeSemanticSecurity] + rw [SSG_DDH0] + have h : (((uniform_2) 1) : ennreal) = 1/2 := by + simp only [uniform_2] + rw [uniform_zmod_prob 1] + norm_cast + rw [<- h] + rw [<- Game2_uniform] + rw [<- Game1_Game2] + rw [Game1_DDH1] + exact DDH_G + +end ElGamal diff --git a/Cryptolib/Negligible.lean b/Cryptolib/Negligible.lean new file mode 100644 index 0000000..72fb028 --- /dev/null +++ b/Cryptolib/Negligible.lean @@ -0,0 +1,243 @@ +/- +Copyright (c) 2021 Joey Lupo +Released under Apache 2.0 license as described in the file LICENSE-APACHE. +Authors: Joey Lupo +-/ +import Mathlib.Analysis.SpecialFunctions.Log.Basic +import Mathlib.Analysis.SpecialFunctions.Pow.NNReal +import Mathlib.Analysis.SpecialFunctions.Pow.Real +import Mathlib.Data.Nat.Basic +import Mathlib.Data.Real.Basic +import Mathlib.Tactic.Cases +import Mathlib.Tactic.Monotonicity + +/-! +# Negligible functions. + +This file defines negligible functions and provides several useful lemmas regarding +negligible functions. + + TO-DO connect with security parameter, (or not, as in Nowak), + and refactor proofs/improve variable naming +-/ + +/- + A function f : ℤ≥1 → ℝ is called negligible if + for all c ∈ ℝ>0 there exists n₀ ∈ ℤ≥1 such that + n₀ ≤ n → |f(n)| < 1/n^c +-/ +def negligible (f : ℕ → ℝ) := + ∀ c > 0, ∃ n₀, ∀ n, + n₀ ≤ n → abs (f n) < 1 / (n : ℝ)^c + +def negligible' (f : ℕ → ℝ) := + ∀ (c : ℝ), ∃ (n₀ : ℕ), ∀ (n : ℕ), + 0 < c → n₀ ≤ n → abs (f n) < 1 / n^c + +lemma negl_equiv (f : ℕ → ℝ) : negligible f ↔ negligible' f := by + constructor + {-- Forward direction + intros h c + have arch := exists_nat_gt c + cases' arch with k hk + let k₀ := max k 1 + have k_leq_k₀ : k ≤ k₀ := le_max_left k 1 + have kr_leq_k₀r : (k:ℝ) ≤ k₀ := Nat.cast_le.mpr k_leq_k₀ + have k₀_pos : 0 < k₀ := by {apply le_max_right k 1} + have a := h k₀ k₀_pos + + -- use k₀ + -- intros n c_pos hn + -- have hnnn : k ≤ n := by linarith + + cases' a with n' hn₀ + let n₀ := max n' 1 + have n₀_pos : 0 < n₀ := by apply le_max_right n' 1 + have n'_leq_n₀ : n' ≤ n₀ := le_max_left n' 1 + use n₀ + intros n c_pos hn + have hnnn : n' ≤ n := by linarith + + have b : (n : ℝ)^c ≤ (n : ℝ)^(k₀ : ℝ) := by + apply Real.rpow_le_rpow_of_exponent_le + norm_cast + linarith + linarith + have daf : (n : ℝ)^(k₀ : ℝ) = (n : ℝ)^k₀ := (n : ℝ).rpow_natCast k₀ + rw [daf] at b + have d : 1 / (n : ℝ)^k₀ ≤ 1 / n^c := by + apply one_div_le_one_div_of_le + { -- Proving 0 < (n:ℝ) ^ c + apply Real.rpow_pos_of_pos + norm_cast + linarith + } + {exact b} + have goal : abs (f n) < 1 / n^c := + calc + abs (f n) < 1 / (n : ℝ)^k₀ := hn₀ n hnnn + _ ≤ 1 / n^c := d + exact goal + } + + {-- Reverse direction + intros h c hc + cases' h c with n₀ hn₀ + use n₀ + intros n hn + have goal := hn₀ n (Nat.cast_pos.mpr hc) hn + rw [(n : ℝ).rpow_natCast c] at goal + exact goal + } + +lemma zero_negl : negligible (λ_ => 0) := by + intros c hc + use 1 + intros n hn + norm_num + apply pow_pos + have h : 0 < n := by linarith + exact Nat.cast_pos.mpr h + +lemma negl_add_negl_negl {f g : ℕ → ℝ} : negligible f → negligible g → negligible (f + g) := by + intros hf hg + intros c hc + have hc1 : (c+1) > 0 := Nat.lt.step hc + have hf2 := hf (c+1) hc1 + have hg2 := hg (c+1) hc1 + cases' hf2 with nf hnf + cases' hg2 with ng hng + let n₀ := max (max nf ng) 2 + use n₀ + intros n hn + let nr := (n:ℝ) + have n_eq_nr : (n:ℝ) = nr := by rfl + + have tn : max nf ng ≤ n₀ := le_max_left (max nf ng) 2 + have t2n₀ : 2 ≤ n₀ := le_max_right (max nf ng) 2 + have t2n : 2 ≤ n := by linarith + have t2nr : 2 ≤ nr := by + have j := Nat.cast_le.mpr t2n + rw [n_eq_nr] at j + norm_num at j + exact j + exact is_R_or_C.char_zero_R_or_C + have tnr_pos : 0 < nr := by linarith + + have t2na : (1 / nr) * (1/nr^c) ≤ (1 / (2 : ℝ)) * (1 / nr^c) := by + have ht2 : 0 < (1 / nr^c) := by {apply one_div_pos.mpr; exact pow_pos tnr_pos c} + apply (mul_le_mul_right ht2).mpr + apply one_div_le_one_div_of_le + exact zero_lt_two + exact t2nr + + have tnr2 : 1 / nr^(c + 1) ≤ (1 / (2 : ℝ)) * (1 / nr^c) := + calc + 1 / nr ^ (c + 1) = (1 / nr)^(c + 1) := by rw [one_div_pow] + _ = (1 / nr)^c * (1 / nr) := pow_succ (1 / nr) c + _ = (1 / nr) * (1 / nr)^c := by linarith + _ = (1 / nr) * (1 / nr^c) := by rw [one_div_pow] + _ ≤ (1 / (2 : ℝ)) * (1 / nr^c) := t2na + + have tnf : nf ≤ n := + calc + nf ≤ n₀ := le_of_max_le_left tn + _ ≤ n := hn + have tfn := hnf n tnf + have tf : abs (f n) < (1 / (2 : ℝ)) * (1 / nr^c) := by linarith + + have tng : ng ≤ n := + calc ng ≤ n₀ := le_of_max_le_right tn + _ ≤ n := hn + have tgn := hng n tng + have tg : abs (g n) < (1/(2:ℝ)) * (1/nr^c) := by linarith + + have goal : abs ((f + g) n) < 1 / nr ^ c := + calc + abs ((f + g) n) = abs (f n + g n) := by rw [Pi.add_apply f g n] + _ ≤ abs (f n) + abs (g n) := abs_add (f n) (g n) + _ < (1/(2:ℝ)) * (1/nr^c) + abs (g n) := by linarith + _ < (1/(2:ℝ)) * (1/nr^c) + (1/(2:ℝ)) * (1/nr^c) := by linarith + _ = 1/nr^c := by ring_nf + exact goal + +lemma bounded_negl_negl {f g : ℕ → ℝ} (hg : negligible g): + (∀ n, abs (f n) ≤ abs (g n)) → negligible f := by + intro h + intros c hc + have hh := hg c hc + cases' hh with n₀ hn₀ + use n₀ + intros n hn + have goal : abs (f n) < 1 / (n : ℝ) ^ c := + calc + abs (f n) ≤ abs (g n) := h n + _ < 1 / (n : ℝ)^c := hn₀ n hn + exact goal + +lemma nat_mul_negl_negl {f : ℕ → ℝ} (m : ℕ): + negligible f → negligible (λn => m * (f n)) := by + intros hf + induction' m with k hk + { -- Base case + norm_num + exact zero_negl + } + { -- Inductive step + norm_num + have d : (λn => ((k : ℝ) + 1) * (f n)) = (λn => (k : ℝ) * (f n)) + (λn => f n) := + by sorry --repeat' {ring_nf} + rw [d] + apply negl_add_negl_negl + exact hk + exact hf + } + +lemma const_mul_negl_negl {f : ℕ → ℝ} (m : ℝ) : + negligible f → negligible (λn => m * (f n)) := by + intro hf + -- Use Archimedian property to get arch : ℕ with abs m < arch + have arch := exists_nat_gt (abs m) + cases' arch with k hk + apply bounded_negl_negl + + { -- Demonstrate a negligible function kf + have kf_negl := nat_mul_negl_negl k hf + exact kf_negl + } + + { -- Show kf bounds mf from above + intro n + have h : abs m ≤ abs (k : ℝ) := + calc + abs m ≤ (k : ℝ) := le_of_lt hk + _ = abs (k : ℝ) := (Nat.abs_cast k).symm + + have goal : abs (m * f n) ≤ abs ((k : ℝ) * f n) := + calc + abs (m * f n) = abs m * abs (f n) := by rw [abs_mul] + _ ≤ abs (k : ℝ) * abs (f n) := mul_le_mul_of_nonneg_right h (abs_nonneg (f n)) + _ = abs ((k : ℝ) * f n) := by rw [<- abs_mul] + + exact goal + } + +theorem neg_exp_negl : negligible ((λn => (1 : ℝ) / 2^n) : ℕ → ℝ) := by sorry + +-- Need to prove lim n^c/2^n = 0 by induction on c using L'Hopital's rule to apply inductive +-- hypothesis +/- + let m := 2 + have hm : 0 < 2 := zero_lt_two + have c2_negl := c2_mul_neg_exp_is_negl 2 hm + have r : (λ (n : ℕ) => 16 * (1 / (2 ^ n * 16)): ℕ → ℝ) = ((λn => (1:ℝ)/2^n): ℕ → ℝ) := by + funext + have h : (1:ℝ) / 2^n / 16 = (1:ℝ) / (2^n * 16) := div_div_eq_div_mul 1 (2^n) 16 + rw [<- h] + ring_nf + + have goal := const_mul_negl_is_negl 16 c2_negl + norm_num at goal + rw [<-r] + exact goal +-/ diff --git a/src/pedersen.lean b/Cryptolib/Pedersen.lean similarity index 69% rename from src/pedersen.lean rename to Cryptolib/Pedersen.lean index 0108d79..8280855 100644 --- a/src/pedersen.lean +++ b/Cryptolib/Pedersen.lean @@ -1,15 +1,19 @@ +/- +Copyright (c) 2023 Ashley Blacquiere +Released under Apache 2.0 license as described in the file LICENSE-APACHE. +Authors: Ashley Blacquiere +-/ +import Cryptolib.Commitments +import Cryptolib.DiscreteLog -import dlog -import commitments - -section pedersen +section Pedersen -noncomputable theory +noncomputable theory variables {M : Type} (G : Type) [fintype G] [group G] [decidable_eq G] - (g : G) (g_gen_G : ∀ (x : G), x ∈ subgroup.gpowers g) - (q : ℕ) [fact (0 < q)] (G_card_q : fintype.card G = q) + (g : G) (g_gen_G : ∀ (x : G), x ∈ subgroup.gpowers g) + (q : ℕ) [fact (0 < q)] (G_card_q : fintype.card G = q) (A : G → (pmf (G × zmod q) × zmod q × zmod q × G × G)) include g_gen_G G_card_q -- assumptions used in the game reduction @@ -22,18 +26,18 @@ To implement: (gen : pmf G) -- generates the public parameter, h ∈ G (commit : G → M → pmf (C × D) ) (verify : G → C → D → M → bool) -(BindingAdversary : G → pmf (C × D × D × M × M)) +(BindingAdversary : G → pmf (C × D × D × M × M)) -/ -- (gen : pmf (G x zmod q) -- generates the public parameter, h ∈ G and secret x ∈ zmod q --- Note: Messages in ElGamal come from G not from zmod q -def gen : pmf (G × zmod q) := -do +-- Note: Messages in ElGamal come from G not from zmod q +def gen : pmf (G × zmod q) := +do x ← uniform_zmod q, - pure (g^x.val, x) + pure (g^x.val, x) -- commit : G → M → pmf (C × D) -def commit (h : G) (m : zmod q) : pmf (G × zmod q) := +def commit (h : G) (m : zmod q) : pmf (G × zmod q) := do y ← uniform_zmod q, pure (g^m.val * h^y.val, y) @@ -42,11 +46,11 @@ do def verify (h : G) (c : G) (d : zmod q) (m : zmod q) : zmod 2 := let c' := g^m.val * h^d.val in if c' = c then 1 else 0 --- Previously had as follows, but problems with the use of ite +-- Previously had as follows, but problems with the use of ite -- def verify' (h : G) (c : G) (d : zmod q) (m : zmod q) : zmod 2 := --- do +-- do -- let c' := g^m.val * h^d.val, --- pure (if c' = c then 1 else 0) +-- pure (if c' = c then 1 else 0) -- BindingAdversary : G → pmf (C × D × D × M × M) @@ -59,16 +63,14 @@ do let c := (A h).1, pure (if (g^x.val * h^r.val) = c.1 then 1 else 0) -/- - The probability of the binding adversary winning the security game (i.e. finding messages, m and m', and opening values, o and o', such that they both resolve to the same commitment c), is equal to the probability of A winning the game DL. +/- + The probability of the binding adversary winning the security game (i.e. finding messages, m and m', and opening values, o and o', such that they both resolve to the same commitment c), is equal to the probability of A winning the game DL. -/ #check BG -theorem BG_DL : BG gen A verify = DL ?? := -begin - sorry, -end +theorem BG_DL : BG gen A verify = DL ?? := by + sorry -end pedersen \ No newline at end of file +end Pedersen diff --git a/Cryptolib/PublicKeyEncryption.lean b/Cryptolib/PublicKeyEncryption.lean new file mode 100644 index 0000000..b3661dd --- /dev/null +++ b/Cryptolib/PublicKeyEncryption.lean @@ -0,0 +1,70 @@ +/- +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.Data.ZMod.Basic +import Mathlib.Probability.Distributions.Uniform + +/-! +# Security games as PMFs + +This file provides formal definitions for correctness and semantic security of a public +key encryption scheme. +-/ + +noncomputable section + +/- +G1 = public key space, G2 = private key space, +M = message space, C = ciphertext space +A_state = type for state A1 passes to A2 +-/ +variable {G1 G2 M C A_state: Type} [DecidableEq M] + (keygen : PMF (G1 × G2)) + (encrypt : G1 → M → PMF C) + (decrypt : G2 → C → M) + (A1 : G1 → PMF (M × M × A_state)) + (A2 : C → A_state → PMF (ZMod 2)) -- Should have G1 else how can A2 do further encryptions? Any general result about encryptions before getting challenge ciphertext...? + +/- +Executes a public-key protocol defined by keygen, +encrypt, and decrypt +-/ +-- Simulates running the program and returns 1 with prob 1 if: +-- `Pr[D(sk, E(pk, m)) = m] = 1` holds +def enc_dec (m : M) : PMF (ZMod 2) := -- given a message m +do + let k ← keygen -- produces a public / secret key pair + let c ← encrypt k.1 m -- encrypts m using pk + pure (if decrypt k.2 c = m then 1 else 0) -- decrypts using sk and checks for equality with m + +/- +A public-key encryption protocol is correct if decryption undoes +encryption with probability 1 +-/ + +/- +This chain of encryption/decryption matches the monadic actions in the `enc_dec` function +-/ +def PkeCorrectness : Prop := ∀ (m : M), enc_dec keygen encrypt decrypt m = pure 1 + +/- +The semantic security game. +Returns 1 if the attacker A2 guesses the correct bit +-/ +def SSG : PMF (ZMod 2) := +do + let k ← keygen + let m ← A1 k.1 + let b ← uniform_2 + let c ← encrypt k.1 (if b = 0 then m.1 else m.2.1) + let b' ← A2 c m.2.2 + pure (1 + b + b') + +-- SSG(A) denotes the event that A wins the semantic security game +local notation "Pr[SSG(A)]" => (SSG keygen encrypt A1 A2 1) + +def PkeSemanticSecurity (ε : NNReal) : Prop := abs (Pr[SSG(A)].toReal - 1/2) ≤ ε diff --git a/Cryptolib/Tactic.lean b/Cryptolib/Tactic.lean new file mode 100644 index 0000000..704429c --- /dev/null +++ b/Cryptolib/Tactic.lean @@ -0,0 +1,48 @@ +/- +Copyright (c) 2021 Joey Lupo +Released under Apache 2.0 license as described in the file LICENSE-APACHE. +Authors: Joey Lupo +-/ +import Mathlib.Probability.Distributions.Uniform +/-! +# Cryptolib tactics +This file provides the `bindskip` and `bindconst` tactics to help prove equivalences +between PMFs. +-/ + +variable {α β : Type} + +lemma bind_skip' (p : PMF α) (f g : α → PMF β) : + (∀ (a : α), f a = g a) → p.bind f = p.bind g := by + intro ha + ext + simp + simp_rw [ha] + +lemma bind_skip_const' (pa : PMF α) (pb : PMF β) (f : α → PMF β) : + (∀ (a : α), f a = pb) → pa.bind f = pb := by + intro ha + ext + simp + simp_rw [ha] + simp [ENNReal.tsum_mul_right] + +-- setup_tactic_parser +-- meta def tactic.interactive.bind_skip (x : parse (tk "with" *> ident)?) : tactic unit := +-- do `[apply bind_skip'], +-- let a := x.get_or_else `_, +-- tactic.interactive.intro a +syntax "bind_skip" : tactic +macro_rules + | `(tactic|bind_skip) => `(tactic|apply bind_skip') +syntax "bind_skip" "with" ident : tactic +macro_rules + | `(tactic|bind_skip with x) => `(tactic|apply bind_skip') + +-- meta def tactic.interactive.bind_skip_const (x : parse (tk "with" *> ident)?) : tactic unit := +-- do `[apply bind_skip_const'], +-- let a := x.get_or_else `_, +-- tactic.interactive.intro a +syntax "bind_skip_const" "with" ident : tactic +macro_rules + | `(tactic|bind_skip_const with x) => `(tactic|apply bind_skip_const') diff --git a/Cryptolib/ToMathlib.lean b/Cryptolib/ToMathlib.lean new file mode 100644 index 0000000..e89cd70 --- /dev/null +++ b/Cryptolib/ToMathlib.lean @@ -0,0 +1,216 @@ +/- +Copyright (c) 2021 Joey Lupo +Released under Apache 2.0 license as described in the file LICENSE-APACHE. +Authors: Joey Lupo, Alfredo Garcia +-/ +import Mathlib.Data.BitVec +import Mathlib.Data.Fintype.BigOperators +import Mathlib.Data.ZMod.Basic +import Mathlib.GroupTheory.SpecificGroups.Cyclic +import Mathlib.GroupTheory.Subgroup.Simple +-- import Mathlib.GroupTheory.Subgroup.Pointwise +import Mathlib.GroupTheory.OrderOfElement +import Mathlib.Probability.Distributions.Uniform +import Mathlib.Probability.ProbabilityMassFunction.Basic +import Mathlib.Probability.ProbabilityMassFunction.Constructions +import Mathlib.Probability.ProbabilityMassFunction.Monad + +/-! +# General lemmas for inclusion into mathlib + +These are lemmas necessary for using Mathlib with cryptography, that should be upstreamed +into Mathlib itself. +-/ + +/- + --------------------------------------------------------- + To multiset.range + --------------------------------------------------------- +-/ + +lemma range_pos_ne_zero (n : ℕ) (n_pos : 0 < n) : Multiset.range n ≠ 0 := by + apply (Multiset.card_pos).mp + rw [Multiset.card_range] + exact n_pos + + + +/- + --------------------------------------------------------- + To group_theory.is_cyclic + --------------------------------------------------------- +-/ + +def is_cyclic.generator {G : Type} [Group G] [IsCyclic G] (g : G): Prop := + ∀ (x : G), x ∈ Subgroup.zpowers g + + +/- + --------------------------------------------------------- + To bitvec.basic + --------------------------------------------------------- +-/ + +namespace BitVec + +instance fintype : Π (n : ℕ), Fintype (BitVec n) := by + intro n + sorry + -- exact Vector.fintype + +lemma card (n : ℕ) : Fintype.card (BitVec n) = 2^n := by sorry + -- card_vector n + +lemma multiset_ne_zero (n : ℕ) : (BitVec.fintype n).elems.val ≠ 0 := by + apply (Multiset.card_pos).mp + -- have h : Multiset.card (Fintype.elems (BitVec n)).val = 2^n := BitVec.card n + -- rw [h] + -- simp only [pow_pos, nat.succ_pos'] + sorry + +-- missing bitvec lemmas used in streams ciphers. +-- TODO: they need proof +variable (n : ℕ) +variable (a b c : BitVec n) + +lemma add_self : a + a = BitVec.zero n := by sorry +-- lemma add_assoc : a + b + c = a + (b + c) := by sorry +-- lemma zero_add : a = BitVec.zero n + a := by sorry +lemma add_self_assoc : b = a + (a + b) := by sorry + -- rw [←add_assoc, add_self, ←zero_add] + +-- lemma add_comm : a + b = b + a := by +-- -- idea: convert a and b to ℕ and prove comm there +-- have ha := bitvec.to_nat a +-- have hb := bitvec.to_nat b +-- sorry + +lemma add_assoc_self : b = a + b + a := by + -- rw [add_comm, ←add_assoc, add_self, ←zero_add] + sorry + +lemma add_assoc_self_reduce : c = a + (b + (a + (b + c))) := by + rw [←add_assoc, ←add_assoc, ←add_assoc] + -- rw [←add_assoc_self, add_self, ←zero_add] + sorry + +-- def to_list (length: ℕ) (B : BitVec length) : List Bool := +-- Vector.to_list B + + +end BitVec + + +/- + --------------------------------------------------------- + To data.basic.zmod, TO-DO Ask why this isn't already there + --------------------------------------------------------- +-/ + +namespace ZMod + +-- instance group : Π (n : ℕ) [fact (0 < n)], group (zmod n) := +-- by {intros n h, exact multiplicative.group} + +-- instance group (n : ℕ) : Group (ZMod n) := by +instance group : ∀ (n : ℕ) [NeZero n], Group (ZMod n) := by + intros n h + sorry + -- exact Multiplicative.group + +end ZMod + + + +/- + --------------------------------------------------------- + To nat + --------------------------------------------------------- +-/ + +lemma exists_mod_add_div (a b: ℕ) : ∃ (m : ℕ), a = a % b + b * m := by + use (a/b) + exact (Nat.mod_add_div a b).symm + + + +/- + --------------------------------------------------------- + To group + --------------------------------------------------------- +-/ + +variable (G : Type) [Fintype G] [Group G] + +namespace Group + +-- lemma multiset_ne_zero : (Fintype.elems G).val ≠ 0 := by +-- have e : G := (_inst_2.one) +-- have h1 : e ∈ (Fintype.elems G).val := Finset.mem_univ e +-- have h2 : 0 < multiset.card (fintype.elems G).val := by +-- apply (multiset.card_pos_iff_exists_mem).mpr +-- exact Exists.intro e h1 +-- exact multiset.card_pos.mp h2 + +end Group + +/- + --------------------------------------------------------- + To list + --------------------------------------------------------- +-/ + +namespace List + +-- Given a list `l`, where each element is of type +-- `bitvec` of a given length `len`, convert this to a +-- `vector`, truncating the list at `len_vec` elements. +-- def to_vec_of_bitvec +-- (len_bitvec : ℕ) (len_vec: ℕ) (l : List (BitVec len_bitvec)) : +-- Vector (BitVec len_bitvec ) len_vec := +-- ⟨List.take len_vec l, List.take_length len_vec l⟩ + +end List + +/- + --------------------------------------------------------- + To ascii + --------------------------------------------------------- +-/ + +namespace ascii + +-- https://www.rapidtables.com/code/text/ascii-table.html + +notation "ascii.A" => 0b01000001 -- 65 +notation "ascii.B" => 0b01000010 -- 66 +notation "ascii.C" => 0b01000011 -- 67 +notation "ascii.D" => 0b01000100 -- 68 +notation "ascii.E" => 0b01000101 -- 69 +notation "ascii.F" => 0b01000110 -- 70 +notation "ascii.G" => 0b01000111 -- 71 +notation "ascii.H" => 0b01001000 -- 72 +notation "ascii.I" => 0b01001001 -- 73 +notation "ascii.J" => 0b01001010 -- 74 +notation "ascii.K" => 0b01001011 -- 75 +notation "ascii.L" => 0b01001100 -- 76 +notation "ascii.M" => 0b01001101 -- 77 +notation "ascii.N" => 0b01001110 -- 78 +notation "ascii.O" => 0b01001111 -- 79 +notation "ascii.P" => 0b01010000 -- 80 +notation "ascii.Q" => 0b01010001 -- 81 +notation "ascii.R" => 0b01010010 -- 82 +notation "ascii.S" => 0b01010011 -- 83 +notation "ascii.T" => 0b01010100 -- 84 +notation "ascii.U" => 0b01010101 -- 85 +notation "ascii.V" => 0b01010110 -- 86 +notation "ascii.W" => 0b01010111 -- 87 +notation "ascii.X" => 0b01011000 -- 88 +notation "ascii.Y" => 0b01011001 -- 89 +notation "ascii.Z" => 0b01011010 -- 90 + +notation "ascii.[space]" => 0b00100000 -- 32 +notation "ascii.[period]" => 0b00101110 -- 46 + + +end ascii diff --git a/Cryptolib/Uniform.lean b/Cryptolib/Uniform.lean new file mode 100644 index 0000000..d8dda48 --- /dev/null +++ b/Cryptolib/Uniform.lean @@ -0,0 +1,43 @@ +/- +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 Mathlib.Probability.Distributions.Uniform + +/-! +# Uniform distributions over ZMod q, BitVecs, and finite groups + +This file defines the uniform distribution over a finite group as a PMF, including the +special case of Z_q, the integers modulo q. + +It also provides two useful lemmas regarding uniform probabilities. +-/ + +variable (G : Type) [Fintype G] [Nonempty G] [Group G] [DecidableEq G] + +noncomputable section + +def uniform_bitvec (n : ℕ) : PMF (BitVec n) := + PMF.uniformOfFintype (BitVec n) + +def uniform_grp : PMF G := + PMF.uniformOfFintype G + +#check (uniform_grp G) + +def uniform_zmod (n : ℕ) [NeZero n] : PMF (ZMod n) := uniform_grp (ZMod n) + +def uniform_2 : PMF (ZMod 2) := uniform_zmod 2 + +lemma uniform_grp_prob : + ∀ (g : G), (uniform_grp G) g = 1 / Fintype.card G := by + intro g + rw [uniform_grp, PMF.uniformOfFintype_apply, inv_eq_one_div] + +lemma uniform_zmod_prob {n : ℕ} [NeZero n] : + ∀ (a : ZMod n), (uniform_zmod n) a = 1/n := by + intro a + rw [uniform_zmod, uniform_grp, PMF.uniformOfFintype_apply] + simp diff --git a/README.md b/README.md index df159fd..3923d91 100644 --- a/README.md +++ b/README.md @@ -12,20 +12,6 @@ This library is a work-in-progress merge, port, and refactor of several forks of ## Files in cryptolib -- `ddh.lean` - provides a formal specification of the decisional Diffie-Hellman assumption on a finite cyclic group - -- [elgamal.lean](src/elgamal.lean) - contains the formal specification of the ElGamal public key encryption protocol, and the formal proofs of correctness - -- `negligible.lean` - defines negligible functions and provides several useful lemmas regarding negligible functions - -- [pke.lean](src/pke.lean) - provides formal definitions for correctness and semantic security of a public key encryption scheme - -- [tactics.lean](src/tactics.lean) - provides the `bindskip` and `bindconst` tactics to help prove equivalences between pmfs - -- [to_mathlib.lean](src/to_mathlib.lean) - includes general lemmas for inclusion into mathlib - -- [uniform.lean](src/uniform.lean) - defines the uniform distribution over a finite group as a pmf, including the special case of Z_q, the integers modulo q, and provides two useful lemmas regarding uniform probabilities - - [rsa.lean](src/rsa.lean) - contains proof of correctness of the RSA public key encryption protocol - [substitution.lean](src/substitution.lean) - contains basic formalization and proof of correctness of different substitution ciphers @@ -50,7 +36,20 @@ This library is a work-in-progress merge, port, and refactor of several forks of ## License -All code in the `scratch` and `src` folders is licensed under Apache License, Version 2.0. +All code in the `scratch` and `src` folders is licensed under Apache License, Version 2.0, +along with the following files: + +- `Cryptolib/Commitments.lean` +- `Cryptolib/ComputationalDiffieHellman.lean` +- `Cryptolib/DecisionalDiffieHellman.lean` +- `Cryptolib/DiscreteLog.lean` +- `Cryptolib/ElGamal.lean` +- `Cryptolib/Negligible.lean` +- `Cryptolib/Pedersen.lean` +- `Cryptolib/PublicKeyEncryption.lean` +- `Cryptolib/Tactic.lean` +- `Cryptolib/ToMathlib.lean` +- `Cryptolib/Uniform.lean` All other code in this workspace is licensed under either of diff --git a/src/block.lean b/src/block.lean deleted file mode 100644 index 5925144..0000000 --- a/src/block.lean +++ /dev/null @@ -1,56 +0,0 @@ -/- - ----------------------------------------------------------- - Formalization and correctness of block ciphers - ----------------------------------------------------------- --/ - -import data.matrix.basic -import data.zmod.basic -import linear_algebra.matrix.nonsingular_inverse - -open_locale matrix - -namespace hill - --- Hill cipher: A generalization of the affine cipher --- --- If block = 2 then this is a digraphic cipher. --- If block > 2 then this is a poligraphic cipher. --- If block = 1 then this is a reduction to the affine cipher. - --- All operations will be mod 26. -def m : ℕ := 26 - --- The size of the block -variables block : ℕ - --- The key matrix -variable A : matrix (fin block) (fin block) (zmod m) - --- The plaintext vector -variable P : matrix (fin block) (fin 1) (zmod m) - --- The ciphertext vector -variable C : matrix (fin block) (fin 1) (zmod m) - --- Encryption -def encrypt : - matrix (fin block) (fin 1) (zmod m) := A ⬝ P - --- Decryption -noncomputable def decrypt : - matrix (fin block) (fin 1) (zmod m) := A⁻¹ ⬝ P - --- Proof of correctness -lemma dec_undoes_enc (h : A.det = 1): - P = decrypt block A (encrypt block A P) := -begin - unfold encrypt, - unfold decrypt, - rw ← matrix.mul_assoc, - rw matrix.nonsing_inv_mul, - finish, - finish, -end - -end hill diff --git a/src/cdh.lean b/src/cdh.lean deleted file mode 100644 index 3de94d3..0000000 --- a/src/cdh.lean +++ /dev/null @@ -1,36 +0,0 @@ -/- - --------------------------------------------------------------- - The computational Diffie-Hellman assumption as a security game - --------------------------------------------------------------- --/ - -import measure_theory.probability_mass_function -import to_mathlib -import uniform - -noncomputable theory - -section CDH - -variables (G : Type) [fintype G] [group G] - (g : G) (g_gen_G : ∀ (x : G), x ∈ subgroup.gpowers g) - (q : ℕ) [fact (0 < 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 - α ← uniform_zmod q, - β ← uniform_zmod q, - let ω := g^(α.val * β.val), - ω' ← 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 \ No newline at end of file diff --git a/src/ddh.lean b/src/ddh.lean deleted file mode 100644 index df0f80f..0000000 --- a/src/ddh.lean +++ /dev/null @@ -1,46 +0,0 @@ -/- - ----------------------------------------------------------- - The decisional Diffie-Hellman assumption as a security game - ----------------------------------------------------------- --/ - -import probability.probability_mass_function.basic -import to_mathlib -import uniform - -noncomputable theory - -section DDH - -variables (G : Type) [fintype G] [group G] - (g : G) (g_gen_G : ∀ (x : G), x ∈ subgroup.zpowers g) - (q : ℕ) [ne_zero 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 - x ← uniform_zmod q, - y ← uniform_zmod q, - b ← D (g^x.val) (g^y.val) (g^(x.val * y.val)), - pure b - -def DDH1 : pmf (zmod 2) := -do - x ← uniform_zmod q, - y ← uniform_zmod q, - z ← uniform_zmod q, - 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 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) - -def DDH (ε : nnreal) : Prop := abs (Pr[DDH0(D)] - Pr[DDH1(D)]) ≤ ε - -end DDH diff --git a/src/dlog.lean b/src/dlog.lean deleted file mode 100644 index 8af93df..0000000 --- a/src/dlog.lean +++ /dev/null @@ -1,40 +0,0 @@ -import measure_theory.probability_mass_function -import uniform - -noncomputable theory - -section DL - -variables (G : Type) [fintype G] [group G] [decidable_eq G] - (g : G) (g_gen_G : ∀ (x : G), x ∈ subgroup.gpowers g) - (q : ℕ) [fact (0 < 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 - - -- α ← uniform_zmod q, - -- let u := g^α.val, - -- α' ← A u, - -def DL (h : G) : pmf (zmod 2) := -do - α ← uniform_zmod q, - let u := g^α.val, - α' ← 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)] - 1/2) ≤ ε - - -#check DL G g g_gen_G q G_card_q A - -end DL \ No newline at end of file diff --git a/src/elgamal.lean b/src/elgamal.lean deleted file mode 100644 index 84a12bf..0000000 --- a/src/elgamal.lean +++ /dev/null @@ -1,448 +0,0 @@ -/- - ----------------------------------------------------------- - Correctness and semantic security of ElGamal public-key - encryption scheme - ----------------------------------------------------------- --/ - -import ddh -import pke -import tactics -import to_mathlib -import uniform - -section elgamal - -noncomputable theory - -variables (G : Type) [fintype G] [comm_group G] [decidable_eq G] - (g : G) (g_gen_G : ∀ (x : G), x ∈ subgroup.zpowers g) - (q : ℕ) [ne_zero q] [group (zmod q)] (G_card_q : fintype.card G = q) - (A_state : Type) - -include g_gen_G G_card_q - -variables (A1 : G → pmf (G × G × A_state)) - (A2 : G → G → A_state → pmf (zmod 2)) - -def A2' : G × G → A_state → pmf (zmod 2) := λ (gg : G × G), A2 gg.1 gg.2 - --- generates a public key `g^x.val`, and private key `x` -def keygen : pmf (G × (zmod q)) := -do - x ← uniform_zmod q, - pure (g^x.val, x) - -#check keygen --- encrypt takes a pair (public key, message) -def encrypt (pk m : G) : pmf (G × G) := -do - y ← uniform_zmod q, - pure (g^y.val, pk^y.val * m) - --- `x` is the secret key, `c.1` is g^y, the first part of the --- cipher text returned from encrypt, and `c.2` is the --- second value returned from encrypt -def decrypt (x : zmod q)(c : G × G) : G := - (c.2 / (c.1^x.val)) - -/- - ----------------------------------------------------------- - Proof of correctness of ElGamal - ----------------------------------------------------------- --/ - -lemma decrypt_eq_m (m : G) (x y: zmod q) : decrypt G g g_gen_G q G_card_q x ((g^y.val), ((g^x.val)^y.val * m)) = m := -begin - simp [decrypt], - repeat {rw (pow_mul _ _ _).symm}, - rw mul_comm y.val x.val, - repeat {rw group.div_eq_mul_inv}, - rw [mul_assoc, mul_comm m _, <- mul_assoc, mul_inv_self _], - -- conv_lhs {rw [mul_assoc, mul_comm m _, <- mul_assoc]}, - exact one_mul m, -end - --- set_option trace.ext true --- set_option trace.simplify true - - -theorem elgamal_correctness : pke_correctness (keygen G g g_gen_G q G_card_q) (encrypt G g g_gen_G q G_card_q) (decrypt G g g_gen_G q G_card_q) := -begin - simp_intros [pke_correctness], - -- intro m, - -- simp [enc_dec, keygen, encrypt, bind], - -- bind_skip_const with x, - -- simp [pure], - -- bind_skip_const with y, - simp [enc_dec, keygen, encrypt, bind, pure], - simp_rw decrypt_eq_m, - simp only [eq_self_iff_true, if_true], -end - - - -/- - ----------------------------------------------------------- - Proof of semantic security of ElGamal - ----------------------------------------------------------- --/ - -def D (gx gy gz : G) : pmf (zmod 2) := -do - m ← A1 gx, -- give G, g, q, h_1 (gx) to A1 and run to get two messages - b ← uniform_2, -- choose b uniformly - mb ← pure (if b = 0 then m.1 else m.2.1), - b' ← A2 gy (gz * mb) m.2.2, -- Katz & Lindell theorem 12.18 (elgamal) - pure (1 + b + b') -- output the same bit - means it was able to break the encryption - -/- - The probability of the attacker (i.e. the composition of A1 and A2) - winning the semantic security game (i.e. guessing the correct bit), - w.r.t. ElGamal is equal to the probability of D winning the game DDH0. --/ - - -theorem SSG_DDH0 : SSG (keygen G g g_gen_G q G_card_q) (encrypt G g g_gen_G q G_card_q) A1 (A2' G g g_gen_G q G_card_q A_state A2) = DDH0 G g g_gen_G q G_card_q (D G g g_gen_G q G_card_q A_state A1 A2):= -begin - simp only [SSG, DDH0, bind, keygen, encrypt, D], - simp_rw pmf.bind_bind (uniform_zmod q), - bind_skip with x, - simp [pure], - simp_rw pmf.bind_comm (uniform_zmod q), - bind_skip with m, - bind_skip with b, - bind_skip with y, - simp only [A2'], - rw pow_mul g x.val y.val, -end - - -def Game1 : pmf (zmod 2) := -do - x ← uniform_zmod q, - y ← uniform_zmod q, - m ← A1 (g^x.val), - b ← uniform_2, - ζ ← (do z ← uniform_zmod q, mb ← pure (if b = 0 then m.1 else m.2.1), pure (g^z.val * mb)), - b' ← A2 (g^y.val) ζ m.2.2, - pure (1 + b + b') - -def Game2 : pmf (zmod 2) := -do - x ← uniform_zmod q, - y ← uniform_zmod q, - m ← A1 (g^x.val), - b ← uniform_2, - ζ ← (do z ← uniform_zmod q, pure (g^z.val)), - b' ← A2 (g^y.val) ζ m.2.2, - pure (1 + b + b') - -/- - The probability of the attacker (i.e. the composition of A1 and A2) - winning Game1 (i.e. guessing the correct bit) is equal to the - probability of D winning the game DDH1. --/ - -theorem Game1_DDH1 : (Game1 G g g_gen_G q G_card_q A_state A1 A2) = DDH1 G g g_gen_G q G_card_q (D G g g_gen_G q G_card_q A_state A1 A2) := -begin - simp only [DDH1, Game1, bind, D], - bind_skip with x, - bind_skip with y, - simp_rw pmf.bind_bind (A1 _), - conv_rhs {rw pmf.bind_comm (uniform_zmod q)}, - bind_skip with m, - simp_rw pmf.bind_bind (uniform_zmod q), - conv_lhs {rw pmf.bind_comm (uniform_2)}, - bind_skip with z, - conv_rhs {rw pmf.bind_bind (uniform_2)}, - bind_skip with b, - simp_rw pmf.bind_bind, - bind_skip with mb, - simp [pure], -end - -lemma exp_bij : - function.bijective (λ (z : zmod q), g ^ z.val) := -begin - apply (fintype.bijective_iff_surjective_and_card _).mpr, - split, - - { -- (λ (z : zmod q), g ^ z.val) surjective - intro gz, - have hz := subgroup.mem_zpowers_iff.mp (g_gen_G gz), - cases hz with z hz, - cases z, - - { -- Case : z = z' for (z : ℕ) - let zq := z % q, - use zq, - have h1 : (λ (z : zmod q), g ^ z.val) ↑zq = g ^ (zq : zmod q).val := rfl, - rw h1, - rw zmod.val_cast_of_lt, - { - have goal : gz = g ^ zq := - calc - gz = g ^ int.of_nat z : hz.symm - ... = g ^ z : by simp - ... = g ^ (z % q + q * (z / q)) : by rw nat.mod_add_div z q - ... = g ^ (z % q) * g ^ (q * (z / q)) : by rw pow_add - ... = g ^ (z % q) * (g ^ q) ^ (z / q) : by rw pow_mul - ... = g ^ (z % q) * (g ^ fintype.card G) ^ (z / q) : by rw <- G_card_q - ... = g ^ (z % q) : by simp [pow_card_eq_one] - ... = g ^ zq : rfl, - exact goal.symm, - }, - exact nat.mod_lt z (nat.pos_of_ne_zero _inst_4.out), - }, - - { -- Case : z = - (1 + z') for (z' : ℕ) - let zq := (q - (z + 1) % q ) % q, - use zq, - have h1 : (λ (z : zmod q), g ^ z.val) ↑zq = g ^ (zq : zmod q).val := rfl, - rw h1, - rw zmod.val_cast_of_lt, - { - have h1 : (z + 1) % q ≤ fintype.card G := - begin - rw G_card_q, - apply le_of_lt, - exact nat.mod_lt _ (nat.pos_of_ne_zero _inst_4.out), - end, - - have goal : gz = g ^ zq := - calc - gz = g ^ int.neg_succ_of_nat z : hz.symm - ... = (g ^ z.succ)⁻¹ : by rw zpow_neg_succ_of_nat - ... = (g ^ (z + 1))⁻¹ : rfl - ... = (g ^ ((z + 1) % fintype.card G))⁻¹ : by rw pow_eq_mod_card (z + 1) - ... = (g ^ ((z + 1) % q))⁻¹ : by rw G_card_q - ... = g ^ (fintype.card G - (z + 1) % q) : inv_pow_eq_card_sub_pow G g _ h1 - ... = g ^ (q - ((z + 1) % q)) : by rw G_card_q - ... = g ^ ((q - (z + 1) % q) % q - + q * ((q - (z + 1) % q) / q)) : by rw nat.mod_add_div - ... = g ^ ((q - (z + 1) % q) % q) - * g ^ (q * ((q - (z + 1) % q) / q)) : by rw pow_add - ... = g ^ ((q - (z + 1) % q) % q) - * (g ^ q) ^ ((q - (z + 1) % q) / q) : by rw pow_mul - ... = g ^ ((q - (z + 1) % q) % q) - * (g ^ fintype.card G) ^ ((q - (z + 1) % q) / q) : by rw <- G_card_q - ... = g ^ ((q - (z + 1) % q) % q) : by simp [pow_card_eq_one] - ... = g ^ zq : rfl, - exact goal.symm, - }, - - exact nat.mod_lt _ (nat.pos_of_ne_zero _inst_4.out), - }, - }, - - { -- fintype.card (zmod q) = fintype.card G - rw G_card_q, - exact zmod.card q, - }, -end - -lemma exp_mb_bij (mb : G) : function.bijective (λ (z : zmod q), g ^ z.val * mb) := -begin - have h : (λ (z : zmod q), g ^ z.val * mb) = - ((λ (m : G), (m * mb)) ∘ (λ (z : zmod q), g ^ z.val)) := by simp, - rw h, - apply function.bijective.comp, - - { -- (λ (m : G), (m * mb)) bijective - refine finite.injective_iff_bijective.mp _, - intros x a hxa, - simp at hxa, - exact hxa, - }, - - { -- (λ (z : zmod q), g ^ z.val) bijective - exact exp_bij G g g_gen_G q G_card_q, - } -end - -lemma G1_G2_lemma1 (x : G) (exp : zmod q → G) (exp_bij : function.bijective exp) : - ∑' (z : zmod q), ite (x = exp z) (1 : nnreal) 0 = 1 := -begin - have inv := function.bijective_iff_has_inverse.mp exp_bij, - cases inv with exp_inv, - have bij_eq : ∀ (z : zmod q), (x = exp z) = (z = exp_inv x) := - begin - intro z, - simp, - split, - - { -- (x = exp z) → (z = exp_inv x) - intro h, - have h1 : exp_inv x = exp_inv (exp z) := congr_arg exp_inv h, - rw inv_h.left z at h1, - exact h1.symm, - }, - - { -- (z = exp_inv x) → (x = exp z) - intro h, - have h2 : exp z = exp (exp_inv x) := congr_arg exp h, - rw inv_h.right x at h2, - exact h2.symm, - }, - end, - simp_rw bij_eq, - simp, -end - -lemma G1_G2_lemma2 (mb : G) : - (uniform_zmod q).bind (λ (z : zmod q), pure (g^z.val * mb)) = - (uniform_zmod q).bind (λ (z : zmod q), pure (g^z.val)) := -begin - simp [pmf.bind], - simp_rw uniform_zmod_prob, - apply funext, - intro, - -- ext, - simp only [pure], - simp only [pmf.pure], - simp only [coe_fn], - simp only [has_coe_to_fun.coe], - simp only [fun_like.coe], - simp only [ennreal.tsum_mul_left], - -- simp only [pure, pmf.pure, coe_fn, has_coe_to_fun.coe, nnreal.tsum_mul_left], - norm_cast, - simp, - rw @mul_eq_mul_left_iff ennreal ↑q _ _, - simp only [one_div, mul_eq_mul_left_iff, inv_eq_zero, nat.cast_eq_zero], - simp only [one_div], - congr' 2, - intros, - -- simp_rw [mul_eq_mul_left_iff] at *, -- Seems that this is not going to the same depth as the same tactic in 3.3? There is an extra simplification step in the 3.3 version that seems to reach the intended target - simp, - simp only [inv_eq_zero], - simp only [nat.cast_eq_zero], -- added trace.simplify true - must be something in here... - apply or.intro_left, -- tried apply iff.intro here, but that seems like maybe a deadend... - repeat {rw G1_G2_lemma1 x}, - rw G1_G2_lemma1 _ _ (exp_mb_bij mb), - intros, - exact exp_mb_bij mb, -end - -#check exp_bij -#check G1_G2_lemma1 _ _ (exp_mb_bij _) -#check G1_G2_lemma1 -#check exp_mb_bij - -lemma G1_G2_lemma3 (m : pmf G) : - m.bind (λ (mb : G), (uniform_zmod q).bind (λ (z : zmod q), pure (g^z.val * mb))) = - (uniform_zmod q).bind (λ (z : zmod q), pure (g^z.val)) := -begin - simp_rw G1_G2_lemma2 _, - bind_skip_const with m, - congr, -end - -/- - The probability of the attacker (i.e. the composition of A1 and A2) - winning Game1 (i.e. guessing the correct bit) is equal to the - probability of the attacker winning Game2. --/ -theorem Game1_Game2 : Game1 = Game2 := -begin - simp only [Game1, Game2], - bind_skip with x, - bind_skip with y, - bind_skip with m, - bind_skip with b, - simp [bind, -pmf.bind_pure, -pmf.bind_bind], - simp_rw pmf.bind_comm (uniform_zmod q), - rw G1_G2_lemma3, -end - -lemma G2_uniform_lemma (b' : zmod 2) : -uniform_2.bind (λ (b : zmod 2), pure (1 + b + b')) = uniform_2 := -begin - fin_cases b' with [0,1], - - { -- b = 0 - ring_nf, - ext, - simp [uniform_2], - rw uniform_zmod_prob a, - simp_rw uniform_zmod_prob, - simp [nnreal.tsum_mul_left], - have zmod_eq_comm : ∀ (x : zmod 2), (a = 1 + x) = (x = 1 + a) := - begin - intro x, - fin_cases a with [0,1], - - { -- a = 0 - fin_cases x with [0,1], - simp, - }, - - { -- a = 1 - fin_cases x with [0,1], - simp [if_pos], - }, - end, - have h : ∑' (x : zmod 2), (pure (1 + x) : pmf (zmod 2)) a = 1 := - begin - simp [pure, pmf.pure, coe_fn, has_coe_to_fun.coe], - simp_rw zmod_eq_comm, - simp, - end, - rw h, - simp, - }, - - { -- b = 1 - ring_nf, - have h : - uniform_2.bind (λ (b : zmod 2), pure (b + 0)) = uniform_2 := by simp [pure], - exact h, - }, -end - -/- - The probability of the attacker (i.e. the composition of A1 and A2) - winning Game2 (i.e. guessing the correct bit) is equal to a coin flip. --/ -theorem Game2_uniform : Game2 = uniform_2 := -begin - simp [Game2, bind], - bind_skip_const with x, - bind_skip_const with m, - bind_skip_const with y, - rw pmf.bind_comm uniform_2, - simp_rw pmf.bind_comm uniform_2, - bind_skip_const with z, - bind_skip_const with ζ, - bind_skip_const with b', - exact G2_uniform_lemma b', -end - -parameters (ε : nnreal) - -/- - The advantage of the attacker (i.e. the composition of A1 and A2) in - the semantic security game `ε` is exactly equal to the advantage of D in - the Diffie-Hellman game. Therefore, assumining the decisional Diffie-Hellman - assumption holds for the group `G`, we conclude `ε` is negligble, and - therefore ElGamal is, by definition, semantically secure. --/ -theorem elgamal_semantic_security (DDH_G : DDH G g g_gen_G q G_card_q D ε) : - pke_semantic_security keygen encrypt A1 A2' ε := -begin - simp only [pke_semantic_security], - rw SSG_DDH0, - have h : (((uniform_2) 1) : ennreal) = 1/2 := - begin - simp only [uniform_2], - rw uniform_zmod_prob 1, - norm_cast, - end, - rw <- h, - rw <- Game2_uniform, - rw <- Game1_Game2, - rw Game1_DDH1, - exact DDH_G, -end - -end elgamal diff --git a/src/negligible.lean b/src/negligible.lean deleted file mode 100644 index fe39d8c..0000000 --- a/src/negligible.lean +++ /dev/null @@ -1,258 +0,0 @@ -/- - ----------------------------------------------------------- - Negligible functions. - - TO-DO connect with security parameter, (or not, as in Nowak), - and refactor proofs/improve variable naming - ----------------------------------------------------------- --/ - -import analysis.special_functions.log.basic -import analysis.special_functions.pow.nnreal -import data.nat.basic -import data.real.basic -import tactic.monotonicity. - -/- - A function f : ℤ≥1 → ℝ is called negligible if - for all c ∈ ℝ>0 there exists n₀ ∈ ℤ≥1 such that - n₀ ≤ n → |f(n)| < 1/n^c --/ -def negligible (f : ℕ → ℝ) := - ∀ c > 0, ∃ n₀, ∀ n, - n₀ ≤ n → abs (f n) < 1 / (n : ℝ)^c - -def negligible' (f : ℕ → ℝ) := - ∀ (c : ℝ), ∃ (n₀ : ℕ), ∀ (n : ℕ), - 0 < c → n₀ ≤ n → abs (f n) < 1 / n^c - -lemma negl_equiv (f : ℕ → ℝ) : negligible f ↔ negligible' f := -begin - split, - {-- Forward direction - intros h c, - have arch := exists_nat_gt c, - cases arch with k hk, - let k₀ := max k 1, - have k_leq_k₀ : k ≤ k₀ := le_max_left k 1, - have kr_leq_k₀r : (k:ℝ) ≤ k₀ := nat.cast_le.mpr k_leq_k₀, - have k₀_pos : 0 < k₀ := by {apply le_max_right k 1}, - have a := h k₀ k₀_pos, - - -- use k₀, - -- intros n c_pos hn, - -- have hnnn : k ≤ n := by linarith - - cases a with n' hn₀, - let n₀ := max n' 1, - have n₀_pos : 0 < n₀ := by apply le_max_right n' 1, - have n'_leq_n₀ : n' ≤ n₀ := le_max_left n' 1, - use n₀, - intros n c_pos hn, - have hnnn : n' ≤ n := by linarith, - - have b : (n : ℝ)^c ≤ (n : ℝ)^(k₀ : ℝ) := - begin - apply real.rpow_le_rpow_of_exponent_le, - norm_cast, - linarith, - linarith, - end, - have daf : (n : ℝ)^(k₀ : ℝ) = (n : ℝ)^k₀ := (n : ℝ).rpow_nat_cast k₀, - rw daf at b, - have d : 1 / (n : ℝ)^k₀ ≤ 1 / n^c := - begin - apply one_div_le_one_div_of_le, - { -- Proving 0 < (n:ℝ) ^ c - apply real.rpow_pos_of_pos, - norm_cast, - linarith, - }, - {exact b}, - end, - have goal : abs (f n) < 1 / n^c := - calc - abs(f n) < 1 / (n : ℝ)^k₀ : hn₀ n hnnn - ... ≤ 1 / n^c : d, - exact goal, - }, - - {-- Reverse direction - intros h c hc, - cases h c with n₀ hn₀, - use n₀, - intros n hn, - have goal := hn₀ n (nat.cast_pos.mpr hc) hn, - rw (n : ℝ).rpow_nat_cast c at goal, - exact goal, - }, -end - -lemma zero_negl : negligible (λn, 0) := -begin - intros c hc, - use 1, - intros n hn, - norm_num, - apply one_div_pos.mpr, - apply pow_pos, - have h : 0 < n := by linarith, - exact nat.cast_pos.mpr h, -end - -lemma negl_add_negl_negl {f g : ℕ → ℝ} : negligible f → negligible g → negligible (f + g) := -begin - intros hf hg, - intros c hc, - have hc1 : (c+1) > 0 := nat.lt.step hc, - have hf2 := hf (c+1) hc1, - have hg2 := hg (c+1) hc1, - cases hf2 with nf hnf, - cases hg2 with ng hng, - let n₀ := max (max nf ng) 2, - use n₀, - intros n hn, - let nr := (n:ℝ), - have n_eq_nr : (n:ℝ) = nr := by refl, - - have tn : max nf ng ≤ n₀ := le_max_left (max nf ng) 2, - have t2n₀ : 2 ≤ n₀ := le_max_right (max nf ng) 2, - have t2n : 2 ≤ n := by linarith, - have t2nr : 2 ≤ nr := - begin - have j := nat.cast_le.mpr t2n, - rw n_eq_nr at j, - norm_num at j, - exact j, - exact is_R_or_C.char_zero_R_or_C, - end, - have tnr_pos : 0 < nr := by linarith, - - have t2na : (1 / nr) * (1/nr^c) ≤ (1 / (2 : ℝ)) * (1 / nr^c) := - begin - have ht2 : 0 < (1 / nr^c) := by {apply one_div_pos.mpr, exact pow_pos tnr_pos c}, - apply (mul_le_mul_right ht2).mpr, - apply one_div_le_one_div_of_le, - exact zero_lt_two, - exact t2nr, - end, - - have tnr2 : 1 / nr^(c + 1) ≤ (1 / (2 : ℝ)) * (1 / nr^c) := - calc - 1 / nr ^ (c + 1) = (1 / nr)^(c + 1) : by rw one_div_pow - ... = (1 / nr) * (1 / nr)^c : pow_succ (1 / nr) c - ... = (1 / nr) * (1 / nr^c) : by rw one_div_pow - ... ≤ (1 / (2 : ℝ)) * (1 / nr^c) : t2na, - - have tnf : nf ≤ n := - calc - nf ≤ n₀ : le_of_max_le_left tn - ... ≤ n : hn, - have tfn := hnf n tnf, - have tf : abs (f n) < (1 / (2 : ℝ)) * (1 / nr^c) := by linarith, - - have tng : ng ≤ n := - calc ng ≤ n₀ : le_of_max_le_right tn - ... ≤ n : hn, - have tgn := hng n tng, - have tg : abs (g n) < (1/(2:ℝ)) * (1/nr^c) := by linarith, - - have goal : abs ((f + g) n) < 1 / nr ^ c := - calc - abs ((f + g) n) = abs (f n + g n) : by rw pi.add_apply f g n - ... ≤ abs (f n) + abs (g n) : abs_add (f n) (g n) - ... < (1/(2:ℝ)) * (1/nr^c) + abs (g n): by linarith - ... < (1/(2:ℝ)) * (1/nr^c) + (1/(2:ℝ)) * (1/nr^c) : by linarith - ... = 1/nr^c : by ring_nf, - exact goal, -end - -lemma bounded_negl_negl {f g : ℕ → ℝ} (hg : negligible g): -(∀ n, abs (f n) ≤ abs (g n)) → negligible f := -begin - intro h, - intros c hc, - have hh := hg c hc, - cases hh with n₀ hn₀, - use n₀, - intros n hn, - have goal : abs (f n) < 1 / (n : ℝ) ^ c := - calc - abs (f n) ≤ abs (g n) : h n - ... < 1 / (n : ℝ)^c: hn₀ n hn, - exact goal, -end - -lemma nat_mul_negl_negl {f : ℕ → ℝ} (m : ℕ): -negligible f → negligible (λn, m * (f n)) := -begin - intros hf, - induction m with k hk, - { -- Base case - norm_num, - exact zero_negl, - }, - { -- Inductive step - norm_num, - have d : (λn, ((k : ℝ) + 1) * (f n)) = (λn, (k : ℝ) * (f n)) + (λn, f n) := - by repeat {ring_nf}, - rw d, - apply negl_add_negl_negl, - exact hk, - exact hf, - }, -end - -lemma const_mul_negl_negl {f : ℕ → ℝ} (m : ℝ) : -negligible f → negligible (λn, m * (f n)) := -begin - intro hf, - -- Use Archimedian property to get arch : ℕ with abs m < arch - have arch := exists_nat_gt (abs m), - cases arch with k hk, - apply bounded_negl_negl, - - { -- Demonstrate a negligible function kf - have kf_negl := nat_mul_negl_negl k hf, - exact kf_negl, - }, - - { -- Show kf bounds mf from above - intro n, - have h : abs m ≤ abs (k : ℝ) := - calc - abs m ≤ (k : ℝ) : le_of_lt hk - ... = abs (k : ℝ) : (nat.abs_cast k).symm, - - have goal : abs (m * f n) ≤ abs ((k : ℝ) * f n) := - calc - abs (m * f n) = abs m * abs (f n) : by rw abs_mul - ... ≤ abs (k : ℝ) * abs (f n) : mul_le_mul_of_nonneg_right h (abs_nonneg (f n)) - ... = abs ((k : ℝ) * f n) : by rw <- abs_mul, - - exact goal, - }, -end - -theorem neg_exp_negl : negligible ((λn, (1 : ℝ) / 2^n) : ℕ → ℝ) := by sorry - --- Need to prove lim n^c/2^n = 0 by induction on c using L'Hopital's rule to apply inductive --- hypothesis -/- -begin - let m := 2, - have hm : 0 < 2 := zero_lt_two, - have c2_negl := c2_mul_neg_exp_is_negl 2 hm, - have r : (λ (n : ℕ), 16 * (1 / (2 ^ n * 16)): ℕ → ℝ) = ((λn, (1:ℝ)/2^n): ℕ → ℝ) := - begin - funext, - have h : (1:ℝ) / 2^n / 16 = (1:ℝ) / (2^n * 16) := div_div_eq_div_mul 1 (2^n) 16, - rw <- h, - ring_nf, - end, - - have goal := const_mul_negl_is_negl 16 c2_negl, - norm_num at goal, - rw <-r, - exact goal, -end -/ diff --git a/src/pke.lean b/src/pke.lean deleted file mode 100644 index e80ea9f..0000000 --- a/src/pke.lean +++ /dev/null @@ -1,61 +0,0 @@ -/- - ----------------------------------------------------------- - Security games as pmfs - ----------------------------------------------------------- --/ - -import data.zmod.basic -import probability.probability_mass_function.basic -import to_mathlib -import uniform - -noncomputable theory - -/- - G1 = public key space, G2 = private key space, - M = message space, C = ciphertext space - A_state = type for state A1 passes to A2 --/ -variables {G1 G2 M C A_state: Type} [decidable_eq M] - (keygen : pmf (G1 × G2)) - (encrypt : G1 → M → pmf C) - (decrypt : G2 → C → M) - (A1 : G1 → pmf (M × M × A_state)) - (A2 : C → A_state → pmf (zmod 2)) -- Should have G1 else how can A2 do further encryptions? Any general result about encryptions before getting challenge ciphertext...? - -/- - Executes the a public-key protocol defined by keygen, - encrypt, and decrypt --/ --- Simulates running the program and returns 1 with prob 1 if: --- `Pr[D(sk, E(pk, m)) = m] = 1` holds -def enc_dec (m : M) : pmf (zmod 2) := -- given a message m -do - k ← keygen, -- produces a public / secret key pair - c ← encrypt k.1 m, -- encrypts m using pk - pure (if decrypt k.2 c = m then 1 else 0) -- decrypts using sk and checks for equality with m - -/- - A public-key encryption protocol is correct if decryption undoes - encryption with probability 1 --/ - -def pke_correctness : Prop := ∀ (m : M), enc_dec keygen encrypt decrypt m = pure 1 -- This chain of encryption/decryption matches the monadic actions in the `enc_dec` function - -/- - The semantic security game. - Returns 1 if the attacker A2 guesses the correct bit --/ -def SSG : pmf (zmod 2):= -do - k ← keygen, - m ← A1 k.1, - b ← uniform_2, - c ← encrypt k.1 (if b = 0 then m.1 else m.2.1), - b' ← A2 c m.2.2, - pure (1 + b + b') - --- SSG(A) denotes the event that A wins the semantic security game -local notation `Pr[SSG(A)]` := (SSG keygen encrypt A1 A2 1) - -def pke_semantic_security (ε : nnreal) : Prop := abs (Pr[SSG(A)] - 1/2) ≤ ε diff --git a/src/tactics.lean b/src/tactics.lean deleted file mode 100644 index 8a24f77..0000000 --- a/src/tactics.lean +++ /dev/null @@ -1,34 +0,0 @@ -import probability.probability_mass_function.basic -import probability.probability_mass_function.monad - -variables {α β : Type} - -lemma bind_skip' (p : pmf α) (f g : α → pmf β) : - (∀ (a : α), f a = g a) → p.bind f = p.bind g := -begin - intro ha, - ext, - simp only [pmf.bind_apply, nnreal.coe_eq], - simp_rw ha, -end - -lemma bind_skip_const' (pa : pmf α) (pb : pmf β) (f : α → pmf β) : - (∀ (a : α), f a = pb) → pa.bind f = pb := -begin - intro ha, - ext, - simp only [pmf.bind_apply, nnreal.coe_eq], - simp_rw ha, - simp [ennreal.tsum_mul_right], -end - -setup_tactic_parser -meta def tactic.interactive.bind_skip (x : parse (tk "with" *> ident)?) : tactic unit := -do `[apply bind_skip'], - let a := x.get_or_else `_, - tactic.interactive.intro a - -meta def tactic.interactive.bind_skip_const (x : parse (tk "with" *> ident)?) : tactic unit := -do `[apply bind_skip_const'], - let a := x.get_or_else `_, - tactic.interactive.intro a diff --git a/src/to_mathlib.lean b/src/to_mathlib.lean deleted file mode 100644 index 5c60d1f..0000000 --- a/src/to_mathlib.lean +++ /dev/null @@ -1,207 +0,0 @@ -import data.bitvec.basic -import data.zmod.basic -import group_theory.specific_groups.cyclic -import group_theory.subgroup.basic -import group_theory.subgroup.pointwise -import group_theory.order_of_element -import probability.probability_mass_function.basic -import probability.probability_mass_function.constructions -import probability.probability_mass_function.monad -import probability.probability_mass_function.uniform - -/- - --------------------------------------------------------- - To multiset.range - --------------------------------------------------------- --/ - -lemma range_pos_ne_zero (n : ℕ) (n_pos : 0 < n): multiset.range n ≠ 0 := -begin - apply (multiset.card_pos).mp, - rw multiset.card_range, - exact n_pos, -end - - - -/- - --------------------------------------------------------- - To group_theory.is_cyclic - --------------------------------------------------------- --/ - -def is_cyclic.generator {G : Type} [group G] [is_cyclic G] (g : G): Prop := - ∀ (x : G), x ∈ subgroup.zpowers g - - -/- - --------------------------------------------------------- - To bitvec.basic - --------------------------------------------------------- --/ - -namespace bitvec - -instance fintype : Π (n : ℕ), fintype (bitvec n) := by {intro n, exact vector.fintype} - -lemma card (n : ℕ) : fintype.card (bitvec n) = 2^n := card_vector n - -lemma multiset_ne_zero (n : ℕ) : (bitvec.fintype n).elems.val ≠ 0 := -begin - apply (multiset.card_pos).mp, - have h : multiset.card (fintype.elems (bitvec n)).val = 2^n := bitvec.card n, - rw h, - simp only [pow_pos, nat.succ_pos'], -end - --- missing bitvec lemmas used in streams ciphers. --- TODO: they need proof -variable n : ℕ -variables a b c : bitvec n - -lemma add_self : a + a = bitvec.zero n := by sorry -lemma add_assoc : a + b + c = a + (b + c) := by sorry -lemma zero_add : a = bitvec.zero n + a := by sorry -lemma add_self_assoc : b = a + (a + b) := - by rw [←add_assoc, add_self, ←zero_add] - -lemma add_comm : a + b = b + a := -begin - -- idea: convert a and b to ℕ and prove comm there - have ha := bitvec.to_nat a, - have hb := bitvec.to_nat b, - sorry, -end - -lemma add_assoc_self : b = a + b + a := - by rw [add_comm, ←add_assoc, add_self, ←zero_add] - -lemma add_assoc_self_reduce : c = a + (b + (a + (b + c))) := -begin - rw [←add_assoc, ←add_assoc, ←add_assoc], - rw [←add_assoc_self, add_self, ←zero_add], -end - -def to_list (length: ℕ) (B : bitvec length) : list bool := - vector.to_list B - - -end bitvec - - -/- - --------------------------------------------------------- - To data.basic.zmod, TO-DO Ask why this isn't already there - --------------------------------------------------------- --/ - -namespace zmod - --- instance group : Π (n : ℕ) [fact (0 < n)], group (zmod n) := --- by {intros n h, exact multiplicative.group} - -instance group (n : ℕ) : group (zmod n) := - by {exact multiplicative.group} - -end zmod - - - -/- - --------------------------------------------------------- - To nat - --------------------------------------------------------- --/ - -lemma exists_mod_add_div (a b: ℕ) : ∃ (m : ℕ), a = a % b + b * m := -begin - use (a/b), - exact (nat.mod_add_div a b).symm, -end - - - -/- - --------------------------------------------------------- - To group - --------------------------------------------------------- --/ - -variables (G : Type) [fintype G] [group G] - -namespace group - -lemma multiset_ne_zero : (fintype.elems G).val ≠ 0 := -begin - have e : G := (_inst_2.one), - have h1 : e ∈ (fintype.elems G).val := finset.mem_univ e, - have h2 : 0 < multiset.card (fintype.elems G).val := - begin - apply (multiset.card_pos_iff_exists_mem).mpr, - exact Exists.intro e h1, - end, - exact multiset.card_pos.mp h2, -end - -end group - -/- - --------------------------------------------------------- - To list - --------------------------------------------------------- --/ - -namespace list - --- Given a list `l`, where each element is of type --- `bitvec` of a given length `len`, convert this to a --- `vector`, truncating the list at `len_vec` elements. -def to_vec_of_bitvec - (len_bitvec : ℕ) (len_vec: ℕ) (l : list (bitvec len_bitvec)) : - vector (bitvec len_bitvec ) len_vec := - ⟨list.take' len_vec l, list.take'_length len_vec l⟩ - -end list - -/- - --------------------------------------------------------- - To ascii - --------------------------------------------------------- --/ - -namespace ascii - --- https://www.rapidtables.com/code/text/ascii-table.html - -notation `ascii.A` := 0b01000001 -- 65 -notation `ascii.B` := 0b01000010 -- 66 -notation `ascii.C` := 0b01000011 -- 67 -notation `ascii.D` := 0b01000100 -- 68 -notation `ascii.E` := 0b01000101 -- 69 -notation `ascii.F` := 0b01000110 -- 70 -notation `ascii.G` := 0b01000111 -- 71 -notation `ascii.H` := 0b01001000 -- 72 -notation `ascii.I` := 0b01001001 -- 73 -notation `ascii.J` := 0b01001010 -- 74 -notation `ascii.K` := 0b01001011 -- 75 -notation `ascii.L` := 0b01001100 -- 76 -notation `ascii.M` := 0b01001101 -- 77 -notation `ascii.N` := 0b01001110 -- 78 -notation `ascii.O` := 0b01001111 -- 79 -notation `ascii.P` := 0b01010000 -- 80 -notation `ascii.Q` := 0b01010001 -- 81 -notation `ascii.R` := 0b01010010 -- 82 -notation `ascii.S` := 0b01010011 -- 83 -notation `ascii.T` := 0b01010100 -- 84 -notation `ascii.U` := 0b01010101 -- 85 -notation `ascii.V` := 0b01010110 -- 86 -notation `ascii.W` := 0b01010111 -- 87 -notation `ascii.X` := 0b01011000 -- 88 -notation `ascii.Y` := 0b01011001 -- 89 -notation `ascii.Z` := 0b01011010 -- 90 - -notation `ascii.[space]` := 0b00100000 -- 32 -notation `ascii.[period]` := 0b00101110 -- 46 - - -end ascii diff --git a/src/uniform.lean b/src/uniform.lean deleted file mode 100644 index 1f9fc1e..0000000 --- a/src/uniform.lean +++ /dev/null @@ -1,40 +0,0 @@ -/- - ----------------------------------------------------------- - Uniform distributions over zmod q, bitvecs, and finite groups - ----------------------------------------------------------- --/ - -import to_mathlib -import probability.probability_mass_function.uniform - -variables (G : Type) [fintype G] [group G] [decidable_eq G] - -noncomputable theory - -def uniform_bitvec (n : ℕ) : pmf (bitvec n) := - pmf.uniform_of_fintype (bitvec n) - -def uniform_grp : pmf G := - pmf.uniform_of_fintype G - -variable (g : G) -#check (uniform_grp G) - -def uniform_zmod (n : ℕ) [ne_zero n] [group (zmod n)] : pmf (zmod n) := uniform_grp (zmod n) - -def uniform_2 [group (zmod 2)]: pmf (zmod 2) := uniform_zmod 2 - -lemma uniform_grp_prob : - ∀ (g : G), (uniform_grp G) g = 1 / fintype.card G := -begin - intro g, - rw [uniform_grp, pmf.uniform_of_fintype_apply, inv_eq_one_div], -end - -lemma uniform_zmod_prob {n : ℕ} [ne_zero n] : - ∀ (a : zmod n), (uniform_zmod n) a = 1/n := -begin - intro a, - rw [uniform_zmod, uniform_grp, pmf.uniform_of_fintype_apply], - simp, -end