From d7316835770d5fb594cd94111eb2fcc8514e12cd Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Sun, 13 Apr 2025 14:02:00 +0000 Subject: [PATCH 01/14] Move Apache 2.0 Lean 3 files into Lean 4 codebase --- .../Commitments.lean | 0 .../ComputationalDiffieHellman.lean | 0 .../DecisionalDiffieHellman.lean | 0 src/dlog.lean => Cryptolib/DiscreteLog.lean | 0 src/elgamal.lean => Cryptolib/ElGamal.lean | 0 src/negligible.lean => Cryptolib/Negligible.lean | 0 src/pedersen.lean => Cryptolib/Pedersen.lean | 0 .../PublicKeyEncryption.lean | 0 src/tactics.lean => Cryptolib/Tactic.lean | 0 src/to_mathlib.lean => Cryptolib/ToMathlib.lean | 0 src/uniform.lean => Cryptolib/Uniform.lean | 0 README.md | 15 ++++++++++++++- 12 files changed, 14 insertions(+), 1 deletion(-) rename src/commitments.lean => Cryptolib/Commitments.lean (100%) rename src/cdh.lean => Cryptolib/ComputationalDiffieHellman.lean (100%) rename src/ddh.lean => Cryptolib/DecisionalDiffieHellman.lean (100%) rename src/dlog.lean => Cryptolib/DiscreteLog.lean (100%) rename src/elgamal.lean => Cryptolib/ElGamal.lean (100%) rename src/negligible.lean => Cryptolib/Negligible.lean (100%) rename src/pedersen.lean => Cryptolib/Pedersen.lean (100%) rename src/pke.lean => Cryptolib/PublicKeyEncryption.lean (100%) rename src/tactics.lean => Cryptolib/Tactic.lean (100%) rename src/to_mathlib.lean => Cryptolib/ToMathlib.lean (100%) rename src/uniform.lean => Cryptolib/Uniform.lean (100%) diff --git a/src/commitments.lean b/Cryptolib/Commitments.lean similarity index 100% rename from src/commitments.lean rename to Cryptolib/Commitments.lean diff --git a/src/cdh.lean b/Cryptolib/ComputationalDiffieHellman.lean similarity index 100% rename from src/cdh.lean rename to Cryptolib/ComputationalDiffieHellman.lean diff --git a/src/ddh.lean b/Cryptolib/DecisionalDiffieHellman.lean similarity index 100% rename from src/ddh.lean rename to Cryptolib/DecisionalDiffieHellman.lean diff --git a/src/dlog.lean b/Cryptolib/DiscreteLog.lean similarity index 100% rename from src/dlog.lean rename to Cryptolib/DiscreteLog.lean diff --git a/src/elgamal.lean b/Cryptolib/ElGamal.lean similarity index 100% rename from src/elgamal.lean rename to Cryptolib/ElGamal.lean diff --git a/src/negligible.lean b/Cryptolib/Negligible.lean similarity index 100% rename from src/negligible.lean rename to Cryptolib/Negligible.lean diff --git a/src/pedersen.lean b/Cryptolib/Pedersen.lean similarity index 100% rename from src/pedersen.lean rename to Cryptolib/Pedersen.lean diff --git a/src/pke.lean b/Cryptolib/PublicKeyEncryption.lean similarity index 100% rename from src/pke.lean rename to Cryptolib/PublicKeyEncryption.lean diff --git a/src/tactics.lean b/Cryptolib/Tactic.lean similarity index 100% rename from src/tactics.lean rename to Cryptolib/Tactic.lean diff --git a/src/to_mathlib.lean b/Cryptolib/ToMathlib.lean similarity index 100% rename from src/to_mathlib.lean rename to Cryptolib/ToMathlib.lean diff --git a/src/uniform.lean b/Cryptolib/Uniform.lean similarity index 100% rename from src/uniform.lean rename to Cryptolib/Uniform.lean diff --git a/README.md b/README.md index df159fd..fc5cebd 100644 --- a/README.md +++ b/README.md @@ -50,7 +50,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 From a69c76c5753efb8acdc3d79f5be96911d7d1ca1e Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Sun, 13 Apr 2025 14:02:25 +0000 Subject: [PATCH 02/14] Migrate `ToMathlib.lean` to Lean 4 --- Cryptolib/ToMathlib.lean | 229 ++++++++++++++++++++------------------- README.md | 2 - 2 files changed, 119 insertions(+), 112 deletions(-) diff --git a/Cryptolib/ToMathlib.lean b/Cryptolib/ToMathlib.lean index 5c60d1f..e89cd70 100644 --- a/Cryptolib/ToMathlib.lean +++ b/Cryptolib/ToMathlib.lean @@ -1,13 +1,26 @@ -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 +/- +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. +-/ /- --------------------------------------------------------- @@ -15,12 +28,10 @@ import probability.probability_mass_function.uniform --------------------------------------------------------- -/ -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 +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 @@ -30,8 +41,8 @@ end --------------------------------------------------------- -/ -def is_cyclic.generator {G : Type} [group G] [is_cyclic G] (g : G): Prop := - ∀ (x : G), x ∈ subgroup.zpowers g +def is_cyclic.generator {G : Type} [Group G] [IsCyclic G] (g : G): Prop := + ∀ (x : G), x ∈ Subgroup.zpowers g /- @@ -40,53 +51,54 @@ def is_cyclic.generator {G : Type} [group G] [is_cyclic G] (g : G): Prop := --------------------------------------------------------- -/ -namespace bitvec +namespace BitVec -instance fintype : Π (n : ℕ), fintype (bitvec n) := by {intro n, exact vector.fintype} +instance fintype : Π (n : ℕ), Fintype (BitVec n) := by + intro n + sorry + -- exact Vector.fintype -lemma card (n : ℕ) : fintype.card (bitvec n) = 2^n := card_vector n +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 := -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 +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 : ℕ -variables a b c : bitvec n +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 rw [←add_assoc, add_self, ←zero_add] +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 := -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_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] +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))) := -begin - rw [←add_assoc, ←add_assoc, ←add_assoc], - rw [←add_assoc_self, add_self, ←zero_add], -end +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 +-- def to_list (length: ℕ) (B : BitVec length) : List Bool := +-- Vector.to_list B -end bitvec +end BitVec /- @@ -95,15 +107,18 @@ end bitvec --------------------------------------------------------- -/ -namespace zmod +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} +-- 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 +end ZMod @@ -113,11 +128,9 @@ end zmod --------------------------------------------------------- -/ -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 +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 @@ -127,23 +140,19 @@ end --------------------------------------------------------- -/ -variables (G : Type) [fintype G] [group G] +variable (G : Type) [Fintype G] [Group G] -namespace group +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 +-- 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 +end Group /- --------------------------------------------------------- @@ -151,17 +160,17 @@ end group --------------------------------------------------------- -/ -namespace 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⟩ +-- 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 +end List /- --------------------------------------------------------- @@ -173,35 +182,35 @@ 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 +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/README.md b/README.md index fc5cebd..9894b05 100644 --- a/README.md +++ b/README.md @@ -22,8 +22,6 @@ This library is a work-in-progress merge, port, and refactor of several forks of - [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 From 76e4d1b182ea598e023fd5f4576c2d40433dfae0 Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Sun, 13 Apr 2025 14:07:42 +0000 Subject: [PATCH 03/14] Migrate `Uniform.lean` to Lean 4 --- Cryptolib/Uniform.lean | 57 ++++++++++++++++++++++-------------------- README.md | 2 -- 2 files changed, 30 insertions(+), 29 deletions(-) diff --git a/Cryptolib/Uniform.lean b/Cryptolib/Uniform.lean index 1f9fc1e..d8dda48 100644 --- a/Cryptolib/Uniform.lean +++ b/Cryptolib/Uniform.lean @@ -1,40 +1,43 @@ /- - ----------------------------------------------------------- - Uniform distributions over zmod q, bitvecs, and finite groups - ----------------------------------------------------------- +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 -import to_mathlib -import probability.probability_mass_function.uniform +/-! +# Uniform distributions over ZMod q, BitVecs, and finite groups -variables (G : Type) [fintype G] [group G] [decidable_eq G] +This file defines the uniform distribution over a finite group as a PMF, including the +special case of Z_q, the integers modulo q. -noncomputable theory +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.uniform_of_fintype (bitvec n) +def uniform_bitvec (n : ℕ) : PMF (BitVec n) := + PMF.uniformOfFintype (BitVec n) -def uniform_grp : pmf G := - pmf.uniform_of_fintype G +def uniform_grp : PMF G := + PMF.uniformOfFintype 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_zmod (n : ℕ) [NeZero n] : PMF (ZMod n) := uniform_grp (ZMod n) -def uniform_2 [group (zmod 2)]: pmf (zmod 2) := uniform_zmod 2 +def uniform_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 + ∀ (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 9894b05..7d0c34b 100644 --- a/README.md +++ b/README.md @@ -22,8 +22,6 @@ This library is a work-in-progress merge, port, and refactor of several forks of - [tactics.lean](src/tactics.lean) - provides the `bindskip` and `bindconst` tactics to help prove equivalences between pmfs -- [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 From debd80cffee522bb0823bc237dfdcdeb1bb3f6cf Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Sun, 13 Apr 2025 20:04:11 +0000 Subject: [PATCH 04/14] Migrate `PublicKeyEncryption.lean` to Lean 4 --- Cryptolib/PublicKeyEncryption.lean | 79 +++++++++++++++++------------- README.md | 2 - 2 files changed, 44 insertions(+), 37 deletions(-) diff --git a/Cryptolib/PublicKeyEncryption.lean b/Cryptolib/PublicKeyEncryption.lean index e80ea9f..b3661dd 100644 --- a/Cryptolib/PublicKeyEncryption.lean +++ b/Cryptolib/PublicKeyEncryption.lean @@ -1,61 +1,70 @@ /- - ----------------------------------------------------------- - Security games as pmfs - ----------------------------------------------------------- +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 -import data.zmod.basic -import probability.probability_mass_function.basic -import to_mathlib -import uniform +/-! +# Security games as PMFs -noncomputable theory +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 +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...? +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 the a public-key protocol defined by keygen, - encrypt, and decrypt +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 +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 + 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 +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 +/- +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 +The semantic security game. +Returns 1 if the attacker A2 guesses the correct bit -/ -def SSG : pmf (zmod 2):= +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, + 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) +local notation "Pr[SSG(A)]" => (SSG keygen encrypt A1 A2 1) -def pke_semantic_security (ε : nnreal) : Prop := abs (Pr[SSG(A)] - 1/2) ≤ ε +def PkeSemanticSecurity (ε : NNReal) : Prop := abs (Pr[SSG(A)].toReal - 1/2) ≤ ε diff --git a/README.md b/README.md index 7d0c34b..1e8eaaa 100644 --- a/README.md +++ b/README.md @@ -18,8 +18,6 @@ This library is a work-in-progress merge, port, and refactor of several forks of - `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 - [rsa.lean](src/rsa.lean) - contains proof of correctness of the RSA public key encryption protocol From 3e258ab2a96bed9855e2ae66ad7a397c63c6ce01 Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Sun, 13 Apr 2025 20:16:43 +0000 Subject: [PATCH 05/14] Migrate `DecisionalDiffieHellman.lean` to Lean 4 --- Cryptolib/DecisionalDiffieHellman.lean | 56 ++++++++++++++------------ README.md | 2 - 2 files changed, 31 insertions(+), 27 deletions(-) diff --git a/Cryptolib/DecisionalDiffieHellman.lean b/Cryptolib/DecisionalDiffieHellman.lean index df0f80f..4863d44 100644 --- a/Cryptolib/DecisionalDiffieHellman.lean +++ b/Cryptolib/DecisionalDiffieHellman.lean @@ -1,46 +1,52 @@ /- - ----------------------------------------------------------- - The decisional Diffie-Hellman assumption as a security game - ----------------------------------------------------------- +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 -import probability.probability_mass_function.basic -import to_mathlib -import uniform +/-! +# The decisional Diffie-Hellman assumption as a security game -noncomputable theory +This file provides a formal specification of the decisional Diffie-Hellman assumption on a +finite cyclic group. +-/ + +noncomputable section 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)) +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 +-- include g_gen_G G_card_q -def DDH0 : pmf (zmod 2) := +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)), + 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) := +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), + 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 g_gen_G q G_card_q D 1) +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 g_gen_G q G_card_q D 1) +local notation "Pr[DDH1(D)]" => (DDH1 G g q D 1) -def DDH (ε : nnreal) : Prop := abs (Pr[DDH0(D)] - Pr[DDH1(D)]) ≤ ε +def DDH (ε : NNReal) : Prop := abs (Pr[DDH0(D)].toReal - Pr[DDH1(D)].toReal) ≤ ε end DDH diff --git a/README.md b/README.md index 1e8eaaa..cf1c688 100644 --- a/README.md +++ b/README.md @@ -12,8 +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 From 321683340b28b20f12532454a574711d0c3516d8 Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Sun, 13 Apr 2025 20:19:50 +0000 Subject: [PATCH 06/14] Migrate `Tactic.lean` to Lean 4 --- Cryptolib/Tactic.lean | 72 ++++++++++++++++++++++++++----------------- README.md | 2 -- 2 files changed, 43 insertions(+), 31 deletions(-) diff --git a/Cryptolib/Tactic.lean b/Cryptolib/Tactic.lean index 8a24f77..704429c 100644 --- a/Cryptolib/Tactic.lean +++ b/Cryptolib/Tactic.lean @@ -1,34 +1,48 @@ -import probability.probability_mass_function.basic -import probability.probability_mass_function.monad +/- +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. +-/ -variables {α β : Type} +variable {α β : 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' (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 := -begin - intro ha, - ext, - simp only [pmf.bind_apply, nnreal.coe_eq], - simp_rw ha, - simp [ennreal.tsum_mul_right], -end +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 +-- 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 +-- 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/README.md b/README.md index cf1c688..79eb9f6 100644 --- a/README.md +++ b/README.md @@ -16,8 +16,6 @@ This library is a work-in-progress merge, port, and refactor of several forks of - `negligible.lean` - defines negligible functions and provides several useful lemmas regarding negligible functions -- [tactics.lean](src/tactics.lean) - provides the `bindskip` and `bindconst` tactics to help prove equivalences between pmfs - - [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 From af3d64af3935c46e780076a0d2b49113fa8c5eba Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Sun, 13 Apr 2025 22:42:14 +0000 Subject: [PATCH 07/14] Migrate `ElGamal.lean` to Lean 4 --- Cryptolib/ElGamal.lean | 635 ++++++++++++++++++++--------------------- README.md | 2 - 2 files changed, 303 insertions(+), 334 deletions(-) diff --git a/Cryptolib/ElGamal.lean b/Cryptolib/ElGamal.lean index 84a12bf..87e2d50 100644 --- a/Cryptolib/ElGamal.lean +++ b/Cryptolib/ElGamal.lean @@ -1,50 +1,56 @@ /- - ----------------------------------------------------------- - Correctness and semantic security of ElGamal public-key - encryption scheme - ----------------------------------------------------------- +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. -/ -import ddh -import pke -import tactics -import to_mathlib -import uniform - -section elgamal +section ElGamal -noncomputable theory +noncomputable section -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) +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 -variables (A1 : G → pmf (G × G × A_state)) - (A2 : G → G → A_state → pmf (zmod 2)) +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 +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)) := +def keygen : PMF (G × (ZMod q)) := do - x ← uniform_zmod q, + 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) := +def encrypt (pk m : G) : PMF (G × G) := do - y ← uniform_zmod q, + 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)) +def decrypt (x : ZMod q)(c : G × G) : G := + (c.2 / (c.1^x.val)) /- ----------------------------------------------------------- @@ -52,33 +58,31 @@ def decrypt (x : zmod q)(c : G × G) : G := ----------------------------------------------------------- -/ -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 +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 : 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 +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] @@ -88,12 +92,12 @@ end ----------------------------------------------------------- -/ -def D (gx gy gz : G) : pmf (zmod 2) := +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) + 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 /- @@ -103,39 +107,37 @@ do -/ -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 +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) := +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, + 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) := +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, + 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') /- @@ -144,281 +146,254 @@ do 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 +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) := -begin - apply (fintype.bijective_iff_surjective_and_card _).mpr, - split, + 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, + { -- (λ (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, + 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), - }, + 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, + 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 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, - }, -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, + 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, + 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, + +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, - }, + 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 + 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)) := -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 + (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)) := -begin - simp_rw G1_G2_lemma2 _, - bind_skip_const with m, - congr, -end +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 := -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, +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, - }, -end + 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 := -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) +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 @@ -427,22 +402,18 @@ parameters (ε : nnreal) 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 +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/README.md b/README.md index 79eb9f6..61a66f4 100644 --- a/README.md +++ b/README.md @@ -12,8 +12,6 @@ This library is a work-in-progress merge, port, and refactor of several forks of ## Files in cryptolib -- [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 - [rsa.lean](src/rsa.lean) - contains proof of correctness of the RSA public key encryption protocol From b33b91753f43156384890ea1def25bb6e720562c Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Tue, 15 Apr 2025 03:00:11 +0000 Subject: [PATCH 08/14] Migrate `Negligible.lean` to Lean 4 --- Cryptolib/Negligible.lean | 377 ++++++++++++++++++-------------------- README.md | 2 - 2 files changed, 181 insertions(+), 198 deletions(-) diff --git a/Cryptolib/Negligible.lean b/Cryptolib/Negligible.lean index fe39d8c..72fb028 100644 --- a/Cryptolib/Negligible.lean +++ b/Cryptolib/Negligible.lean @@ -1,18 +1,26 @@ /- - ----------------------------------------------------------- - Negligible functions. +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 - ----------------------------------------------------------- -/ -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 @@ -20,239 +28,216 @@ import tactic.monotonicity. -/ def negligible (f : ℕ → ℝ) := ∀ c > 0, ∃ n₀, ∀ n, - n₀ ≤ n → abs (f n) < 1 / (n : ℝ)^c + 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, +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, + 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, + 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}, - end, - have goal : abs (f n) < 1 / 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, - }, + 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, + 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) * (1 / nr)^c : pow_succ (1 / nr) c - ... = (1 / nr) * (1 / nr^c) : by rw one_div_pow - ... ≤ (1 / (2 : ℝ)) * (1 / nr^c) : t2na, + 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, + 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, + 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 + 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 := -begin - intro h, - intros c hc, - have hh := hg c hc, - cases hh with n₀ hn₀, - use n₀, - intros n hn, + (∀ 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, -end + 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)) := -begin - intros hf, - induction m with k hk, + negligible f → negligible (λn => m * (f n)) := by + intros hf + induction' m with k hk { -- Base case - norm_num, - exact zero_negl, - }, + 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 + 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)) := -begin - intro hf, + 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, + 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, - }, + have kf_negl := nat_mul_negl_negl k hf + exact kf_negl + } { -- Show kf bounds mf from above - intro n, + intro n have h : abs m ≤ abs (k : ℝ) := calc - abs m ≤ (k : ℝ) : le_of_lt hk - ... = abs (k : ℝ) : (nat.abs_cast k).symm, + 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, + 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 + exact goal + } -theorem neg_exp_negl : negligible ((λn, (1 : ℝ) / 2^n) : ℕ → ℝ) := by sorry +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 -/ + 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/README.md b/README.md index 61a66f4..3923d91 100644 --- a/README.md +++ b/README.md @@ -12,8 +12,6 @@ This library is a work-in-progress merge, port, and refactor of several forks of ## Files in cryptolib -- `negligible.lean` - defines negligible functions and provides several useful lemmas regarding negligible functions - - [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 From 5d7cc3690cbcbd37e0fa77f840d1aeb990f45a2c Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Tue, 15 Apr 2025 03:27:11 +0000 Subject: [PATCH 09/14] Migrate `ComputationalDiffieHellman.lean` to Lean 4 --- Cryptolib/ComputationalDiffieHellman.lean | 45 ++++++++++++----------- 1 file changed, 24 insertions(+), 21 deletions(-) diff --git a/Cryptolib/ComputationalDiffieHellman.lean b/Cryptolib/ComputationalDiffieHellman.lean index 3de94d3..1cb252b 100644 --- a/Cryptolib/ComputationalDiffieHellman.lean +++ b/Cryptolib/ComputationalDiffieHellman.lean @@ -1,36 +1,39 @@ /- - --------------------------------------------------------------- - The computational Diffie-Hellman assumption as a security game - --------------------------------------------------------------- +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 -import measure_theory.probability_mass_function -import to_mathlib -import uniform +/-! +# The computational Diffie-Hellman assumption as a security game +-/ -noncomputable theory +noncomputable section 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) +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 +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), +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) +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 +#check CDH G g /- g_gen_G -/ q /- G_card_q -/ A -end CDH \ No newline at end of file +end CDH From c0f1cbc3864fd13459754893f3593608345029ac Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Tue, 15 Apr 2025 03:28:25 +0000 Subject: [PATCH 10/14] Migrate `DiscreteLog.lean` to Lean 4 --- Cryptolib/DiscreteLog.lean | 53 +++++++++++++++++++++----------------- 1 file changed, 30 insertions(+), 23 deletions(-) diff --git a/Cryptolib/DiscreteLog.lean b/Cryptolib/DiscreteLog.lean index 8af93df..d616709 100644 --- a/Cryptolib/DiscreteLog.lean +++ b/Cryptolib/DiscreteLog.lean @@ -1,40 +1,47 @@ -import measure_theory.probability_mass_function -import uniform - -noncomputable theory +/- +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 -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)) +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 - -- α ← uniform_zmod q, - -- let u := g^α.val, - -- α' ← A u, + -- let α ← uniform_zmod q + -- let u := g^α.val + -- let α' ← A u -def DL (h : G) : pmf (zmod 2) := -do - α ← uniform_zmod q, - let u := g^α.val, - α' ← 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 : ℝ) +-- 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[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 : ℝ) +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) ≤ ε +def DLadv (ε: NNReal) : Prop := abs (Pr[DL(A)].toReal - 1/2) ≤ ε -#check DL G g g_gen_G q G_card_q A +#check DL G g /- g_gen_G -/ q /- G_card_q -/ A -end DL \ No newline at end of file +end DL From c2af5f7a32e52751f3a50600ca1e39a1ba7a7c4b Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Tue, 15 Apr 2025 03:42:31 +0000 Subject: [PATCH 11/14] Migrate `Commitments.lean` to Lean 4 --- Cryptolib/Commitments.lean | 149 ++++++++++++++++++------------------- 1 file changed, 73 insertions(+), 76 deletions(-) diff --git a/Cryptolib/Commitments.lean b/Cryptolib/Commitments.lean index 962b4be..21825ed 100644 --- a/Cryptolib/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 From 7919f6b5f4b612984eb0c3770dbca490e77f3269 Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Tue, 15 Apr 2025 03:53:14 +0000 Subject: [PATCH 12/14] Migrate `Pedersen.lean` to Lean 4 --- Cryptolib/Pedersen.lean | 48 +++++++++++++++++++++-------------------- 1 file changed, 25 insertions(+), 23 deletions(-) diff --git a/Cryptolib/Pedersen.lean b/Cryptolib/Pedersen.lean index 0108d79..8280855 100644 --- a/Cryptolib/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 From 355193afb67569926be92f35f4986968f8301dc4 Mon Sep 17 00:00:00 2001 From: Kris Nuttycombe Date: Sat, 19 Apr 2025 12:10:54 -0600 Subject: [PATCH 13/14] Move Lean 3 block.lean into the Lean 4 codebase. --- src/block.lean => Cryptolib/Block.lean | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename src/block.lean => Cryptolib/Block.lean (100%) diff --git a/src/block.lean b/Cryptolib/Block.lean similarity index 100% rename from src/block.lean rename to Cryptolib/Block.lean From 1c41c6263bfdf8e6637ed99ae51e3343864cfec4 Mon Sep 17 00:00:00 2001 From: Kris Nuttycombe Date: Sat, 19 Apr 2025 12:50:07 -0600 Subject: [PATCH 14/14] Port block.lean to Lean 4 --- Cryptolib/Block.lean | 56 ++++++++++++++++++++------------------------ 1 file changed, 25 insertions(+), 31 deletions(-) diff --git a/Cryptolib/Block.lean b/Cryptolib/Block.lean index 5925144..fa0b5e1 100644 --- a/Cryptolib/Block.lean +++ b/Cryptolib/Block.lean @@ -4,53 +4,47 @@ ----------------------------------------------------------- -/ -import data.matrix.basic -import data.zmod.basic -import linear_algebra.matrix.nonsingular_inverse +import Mathlib.Data.Matrix.Basic +import Mathlib.Data.ZMod.Basic +import Mathlib.LinearAlgebra.Matrix.NonsingularInverse -open_locale matrix +open scoped Matrix -namespace hill +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. +/-! +# Hill cipher: A generalization of the affine cipher --- All operations will be mod 26. +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 -variables block : ℕ +variable (block : ℕ) -- The key matrix -variable A : matrix (fin block) (fin block) (zmod m) +variable (A : Matrix (Fin block) (Fin block) (ZMod m)) -- The plaintext vector -variable P : matrix (fin block) (fin 1) (zmod m) +variable (P : Matrix (Fin block) (Fin 1) (ZMod m)) -- The ciphertext vector -variable C : matrix (fin block) (fin 1) (zmod m) +variable (C : Matrix (Fin block) (Fin 1) (ZMod m)) -- Encryption -def encrypt : - matrix (fin block) (fin 1) (zmod m) := A ⬝ P +def encrypt : (Matrix (Fin block) (Fin 1) (ZMod m)) := A * P -- Decryption -noncomputable def decrypt : - matrix (fin block) (fin 1) (zmod m) := A⁻¹ ⬝ P +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 +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