diff --git a/LICENSE.txt b/LICENSE.txt new file mode 100644 index 0000000..19dc35b --- /dev/null +++ b/LICENSE.txt @@ -0,0 +1,175 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. \ No newline at end of file diff --git a/VerifiedCommitments.lean b/VerifiedCommitments.lean index 7cf78a6..e7ca8b4 100644 --- a/VerifiedCommitments.lean +++ b/VerifiedCommitments.lean @@ -1,3 +1,10 @@ +import VerifiedCommitments.CommitmentScheme import VerifiedCommitments.dlog -import VerifiedCommitments.pedersen -import VerifiedCommitments.«commitment-scheme» +import VerifiedCommitments.PedersenBinding +import VerifiedCommitments.PedersenHiding +import VerifiedCommitments.PedersenScheme +import VerifiedCommitments.ProofUtils +import VerifiedCommitments.«scratch-skip-bind» +import VerifiedCommitments.ZModUtil +import VerifiedCommitments.MapPMFBijection +import VerifiedCommitments.cryptolib diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean index 45596e7..6a0ac0e 100644 --- a/VerifiedCommitments/CommitmentScheme.lean +++ b/VerifiedCommitments/CommitmentScheme.lean @@ -3,26 +3,17 @@ import Mathlib.Probability.ProbabilityMassFunction.Monad import Mathlib.Probability.ProbabilityMassFunction.Constructions import Mathlib.Data.ZMod.Defs - --- namespace Crypto - or similar? --- structure Commit (C O : Type) where --- c : C --- o : O - structure CommitmentScheme (M C O K : Type) where setup : PMF (K × O) commit : K → M → PMF (C × O) verify : K → M → C → O → ZMod 2 -namespace Adversary -structure guess (M C O : Type) where +structure BindingGuess (M C O : Type) where c : C m : M m' : M o : O o': O -end Adversary - namespace Commitment @@ -49,25 +40,14 @@ def perfect_binding (scheme : CommitmentScheme M C O K) : Prop := -- Security depends on generating the parameters correctly, but at this level probably alright to have the group and generator fixed -- h should be inside the game, because its unique to a specific run def comp_binding_game (scheme : CommitmentScheme M C O K) - (A : K → PMF (C × M × M × O × O)) : PMF $ ZMod 2 := - open scoped Classical in - PMF.bind scheme.setup (fun h => - PMF.bind (A h.1) (fun (c, m , m', o, o') => - if scheme.verify h.1 m c o = 1 ∧ scheme.verify h.1 m' c o' = 1 ∧ m ≠ m' then pure 1 else pure 0 )) - -def computational_binding [DecidableEq M] (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop := - ∀ (A : K → PMF (C × M × M × O × O)), comp_binding_game scheme A 1 ≤ ε - --- With Adversary namespace -def comp_binding_game' (scheme : CommitmentScheme M C O K) - (A' : K → PMF (Adversary.guess M C O)) : PMF $ ZMod 2 := + (A' : K → PMF (BindingGuess M C O)) : PMF $ ZMod 2 := open scoped Classical in PMF.bind scheme.setup (fun h => PMF.bind (A' h.1) (fun guess => if scheme.verify h.1 guess.m guess.c guess.o = 1 ∧ scheme.verify h.1 guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m' then pure 1 else pure 0 )) -def computational_binding' [DecidableEq M] (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop := - ∀ (A' : K → PMF (Adversary.guess M C O )), comp_binding_game' scheme A' 1 ≤ ε +def computational_binding [DecidableEq M] (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop := + ∀ (A' : K → PMF (BindingGuess M C O )), comp_binding_game scheme A' 1 ≤ ε -- Perfect hiding diff --git a/VerifiedCommitments/MapPMFBijection.lean b/VerifiedCommitments/MapPMFBijection.lean new file mode 100644 index 0000000..26d9f91 --- /dev/null +++ b/VerifiedCommitments/MapPMFBijection.lean @@ -0,0 +1,32 @@ +-- formalmethods.io © 2025 by William DeMeo is licensed under CC BY-NC-SA 4.0 +-- https://formalmethods.io/ + +import Mathlib.Probability.Distributions.Uniform + +open Classical + +lemma map_uniformOfFintype_equiv + {α β : Type*} [Fintype α] [Fintype β] [DecidableEq β] [Nonempty α] [Nonempty β] + (e : α ≃ β) : + PMF.map e (PMF.uniformOfFintype α) = PMF.uniformOfFintype β := by + ext b + rw [PMF.map_apply] + simp only [PMF.uniformOfFintype_apply] + have h_equiv : (∑' (a : α), if b = e a then (↑(Fintype.card α : ENNReal))⁻¹ else 0) = + (∑' (a : α), if a = e.symm b then (↑(Fintype.card α))⁻¹ else 0) := by + congr 1 + ext a + by_cases h : b = e a + · rw [if_pos h, if_pos] + rw [←Equiv.symm_apply_apply e a] + rw [h] + · rw [if_neg h, if_neg] + intro contra + subst contra + rw [Equiv.apply_symm_apply e] at h + apply h + rfl + rw [h_equiv] + rw [tsum_ite_eq] + congr 1 + rw [Fintype.card_congr e] diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean new file mode 100644 index 0000000..c45c986 --- /dev/null +++ b/VerifiedCommitments/Pedersen.lean @@ -0,0 +1,403 @@ +import VerifiedCommitments.CommitmentScheme +import Mathlib.Data.Nat.Prime.Defs +import Mathlib.GroupTheory.OrderOfElement +import VerifiedCommitments.ZModUtil +import Mathlib.Probability.Distributions.Uniform +import Mathlib.Algebra.Field.ZMod +import VerifiedCommitments.MapPMFBijection +import VerifiedCommitments.cryptolib +import Mathlib.Tactic + +namespace Pedersen + +/- ======================================== + PUBLIC PARAMETERS + ======================================== -/ + +class PedersenScheme (G : Type) extends + Fintype G, Group G, IsCyclic G where + [decidable_G : DecidableEq G] + q : ℕ + [neZero_q : NeZero q] + prime_q : Nat.Prime q + g : G + card_eq : Fintype.card G = q + gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g + +-- Make instances available +variable {G : Type} [params : PedersenScheme G] +instance : DecidableEq G := params.decidable_G +instance : Fact (Nat.Prime params.q) := ⟨params.prime_q⟩ + +/- ======================================== + CORE LEMMAS + ======================================== -/ + +lemma ordg_eq_q : orderOf params.g = params.q := by + have h_card_zpow : Fintype.card (Subgroup.zpowers params.g) = orderOf params.g := Fintype.card_zpowers + have h_card_eq : Fintype.card (Subgroup.zpowers params.g) = Fintype.card G := by + have : Function.Bijective (Subtype.val : Subgroup.zpowers params.g → G) := by + constructor + · exact Subtype.val_injective + · intro x + use ⟨x, params.gen_G x⟩ + exact Fintype.card_of_bijective this + rw [← h_card_zpow, h_card_eq, params.card_eq] + + +/- ======================================== + SCHEME DEFINITION + ======================================== -/ + +noncomputable def setup : PMF (G × (ZMod params.q)) := + PMF.bind (PMF.uniformOfFintype (ZModMult params.q)) (fun a => return ⟨params.g^(val a).val, val a⟩) + +noncomputable def commit (h : G) (m : ZMod params.q) : PMF (G × (ZMod params.q)) := + PMF.bind (PMF.uniformOfFintype (ZMod params.q)) (fun r => return ⟨params.g^m.val * h^r.val, r⟩) + +def verify (h : G) (m : ZMod params.q) (c : G) (o : ZMod params.q) : ZMod 2 := + if c = params.g^m.val * h^o.val then 1 else 0 + +noncomputable def scheme : CommitmentScheme (ZMod params.q) G (ZMod params.q) G := + { + setup := setup, + commit := commit, + verify := verify + } + +noncomputable def generate_a : PMF (ZModMult params.q) := PMF.uniformOfFintype (ZModMult params.q) + +/- ======================================== + DLOG EXPERIMENT + ======================================== -/ + +section DLog + +noncomputable def DLogExperiment (A : G → PMF (ZMod params.q)) : PMF (ZMod 2) := + PMF.bind scheme.setup (fun h => + PMF.bind (A h.1) (fun x' => pure (if params.g^x'.val = params.g^(h.2).val then 1 else 0))) + +noncomputable def constructDlogAdversary + (A : G → PMF (BindingGuess (ZMod params.q) G (ZMod params.q))) + (h : G) : PMF (ZMod params.q) := + PMF.bind (A h) (fun guess => + if guess.o ≠ guess.o' then + return ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹) + else + PMF.uniformOfFintype (ZMod params.q)) + +end DLog + +/- ======================================== + HIDING PROPERTY + ======================================== -/ + +section Hiding + +lemma exp_bij (a : ZModMult params.q) (m : ZMod params.q) : Function.Bijective fun (r : ZMod params.q) => + params.g^((m + (val a) * r : ZMod params.q).val : ℤ) := by + apply (Fintype.bijective_iff_surjective_and_card _).mpr + simp [params.card_eq] + intro c + obtain ⟨k, hk⟩ := params.gen_G c + simp only at hk + simp only + + let z : ZMod params.q := (k : ZMod params.q) + have hk : params.g ^ (z.val : ℤ) = c := by + simp only [ZMod.natCast_val] + rw [←hk] + rw [ZMod.coe_intCast] + rw [← params.card_eq] + rw [@zpow_mod_card] + + let a_inv : ZMod params.q := (val a)⁻¹ + let r : ZMod params.q := a_inv * (z - m) + + have h_mod : (m + val a * r) = z := by + subst r a_inv + rw [←mul_assoc, mul_inv_cancel₀, one_mul] + · exact add_sub_cancel m z + · exact ZModMult.coe_ne_zero a + + grind only [ZMod.natCast_val] + + +noncomputable def expEquiv (a : ZModMult params.q) (m : ZMod params.q) : ZMod params.q ≃ G := +Equiv.ofBijective (fun (r : ZMod params.q) => params.g^((m + (val a) * r : ZMod params.q).val : ℤ)) (exp_bij a m) + +lemma expEquiv_unfold (a : ZModMult params.q) (m r : ZMod params.q) : + expEquiv a m r = params.g^m.val * (params.g^(val a).val)^r.val := by + unfold expEquiv + simp only [Equiv.ofBijective, Equiv.coe_fn_mk] + + have h_pow : (params.g^(val a).val)^r.val = params.g^((val a).val * r.val) := (pow_mul params.g (val a).val r.val).symm + rw [h_pow] + + simp only [← zpow_natCast] + rw [← zpow_add] + + have hord : orderOf params.g = params.q := ordg_eq_q + conv_lhs => rw [← zpow_mod_orderOf, hord] + + suffices h : (((m + (val a) * r).val : ℤ) % ↑params.q) = ((m.val : ℤ) + ((val a).val * r.val : ℤ)) % ↑params.q by + conv_rhs => rw [← zpow_mod_orderOf, hord] + rw [h] + congr 1 + + conv_lhs => rw [ZMod.val_add, ZMod.val_mul] + norm_cast + rw [Nat.add_mod, Nat.mul_mod] + simp + +lemma bij_uniform_for_fixed_a (a : ZModMult params.q) (m : ZMod params.q) : + PMF.map (expEquiv a m) (PMF.uniformOfFintype (ZMod params.q)) = (PMF.uniformOfFintype G) := by + · expose_names; + exact map_uniformOfFintype_equiv (expEquiv a m) + +lemma bij_uniform_for_uniform_a (m : ZMod params.q) : + (PMF.bind (generate_a) + (fun a => PMF.map (expEquiv a m) (PMF.uniformOfFintype (ZMod params.q)))) = (PMF.uniformOfFintype G) := by + unfold generate_a + apply bind_skip_const' + intro a + · expose_names; exact bij_uniform_for_fixed_a a m + +lemma pedersen_commitment_uniform (m : ZMod params.q) (c : G) : + (PMF.map Prod.fst (PMF.bind (generate_a : PMF (ZModMult params.q)) + (fun a => commit (params.g^(val a).val) m )) c) = + ((1 : ENNReal) / (Fintype.card G)) := by + unfold commit + simp only [PMF.map_bind, pure, PMF.pure_map] + have h_eq : (PMF.bind (generate_a : PMF (ZModMult params.q)) + (fun a => PMF.bind (PMF.uniformOfFintype (ZMod params.q)) + (fun r => PMF.pure (params.g^m.val * (params.g^(val a).val)^r.val)))) = + (PMF.bind (generate_a : PMF (ZModMult params.q)) + (fun a => PMF.map (expEquiv a m) (PMF.uniformOfFintype (ZMod params.q)))) := by + apply bind_skip' + intro a + ext x + simp only [PMF.bind_apply, PMF.map_apply, PMF.pure_apply, PMF.uniformOfFintype_apply] + congr 1; ext r + by_cases h : x = params.g^m.val * (params.g^(val a).val)^r.val + · simp only [h, ↓reduceIte] + rw [← expEquiv_unfold a m r] + simp + · simp only [h, ↓reduceIte] + have : x ≠ expEquiv a m r := by + intro contra + rw [expEquiv_unfold a m r] at contra + exact h contra + simp [this] + rw [h_eq] + rw [bij_uniform_for_uniform_a m] + simp [PMF.uniformOfFintype_apply] + +theorem perfect_hiding : Commitment.perfect_hiding (@scheme G params) := by + unfold Commitment.perfect_hiding + intros m m' c + unfold Commitment.do_commit Pedersen.scheme + simp only [] + unfold Pedersen.setup Pedersen.commit + simp only [PMF.bind_bind] + have h_lhs : ((PMF.uniformOfFintype (ZModMult params.q)).bind fun a => + PMF.bind (pure (params.g^(val a).val, val a)) fun h => + (PMF.uniformOfFintype (ZMod params.q)).bind fun r => + PMF.bind (pure (params.g^m.val * h.1^r.val, r)) fun commit => + pure commit.1) c = 1 / Fintype.card G := by + simp only [pure, PMF.pure_bind] + convert pedersen_commitment_uniform m c using 2 + unfold generate_a Pedersen.commit + simp only [PMF.map_bind, pure, PMF.pure_map] + have h_rhs : ((PMF.uniformOfFintype (ZModMult params.q)).bind fun a => + PMF.bind (pure (params.g^(val a).val, val a)) fun h => + (PMF.uniformOfFintype (ZMod params.q)).bind fun r => + PMF.bind (pure (params.g^m'.val * h.1^r.val, r)) fun commit => + pure commit.1) c = 1 / Fintype.card G := by + simp only [pure, PMF.pure_bind] + convert pedersen_commitment_uniform m' c using 2 + unfold generate_a Pedersen.commit + simp only [PMF.map_bind, pure, PMF.pure_map] + rw [h_lhs, h_rhs] + +end Hiding + +/- ======================================== + BINDING PROPERTY + ======================================== -/ + +section Binding + +lemma binding_implies_dlog (a : ZMod params.q) (guess : BindingGuess (ZMod params.q) G (ZMod params.q)) : + let h := params.g ^ a.val + let verify := fun (m : ZMod params.q) (c : G) (o : ZMod params.q) => if c = params.g^m.val * h^o.val then (1 : ZMod 2) else 0 + (verify guess.m guess.c guess.o = 1 ∧ verify guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m') → + (guess.o ≠ guess.o' → params.g^(((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val) = h) := by + intro h verify ⟨h1, h2, m_ne⟩ o_ne + simp only [verify] at h1 h2 + split at h1 <;> split at h2 + case' isTrue.isTrue c_eq1 c_eq2 => + simp only [h] at c_eq1 c_eq2 + + have collision : params.g^guess.m.val * (params.g^a.val)^guess.o.val = params.g^guess.m'.val * (params.g^a.val)^guess.o'.val := by + rw [← c_eq1, c_eq2] + + conv_lhs at collision => arg 2; rw [← pow_mul] + conv_rhs at collision => arg 2; rw [← pow_mul] + rw [← pow_add, ← pow_add] at collision + + have h_coprime : (guess.o' - guess.o).val.Coprime params.q := by + cases Nat.coprime_or_dvd_of_prime params.prime_q (guess.o' - guess.o).val with + | inl h_cop => exact Nat.coprime_comm.mp h_cop + | inr h_dvd => + exfalso + have h_zero : guess.o' - guess.o = 0 := by + rw [← ZMod.val_eq_zero] + have h_mod_zero : (guess.o' - guess.o).val % params.q = 0 := Nat.mod_eq_zero_of_dvd h_dvd + have h_val_bound : (guess.o' - guess.o).val < params.q := ZMod.val_lt (guess.o' - guess.o) + exact Nat.eq_zero_of_dvd_of_lt h_dvd h_val_bound + exact o_ne.symm (eq_of_sub_eq_zero h_zero) + + have h_congr_nat : guess.m.val + a.val * guess.o.val ≡ guess.m'.val + a.val * guess.o'.val [MOD params.q] := by + simpa [ordg_eq_q] using (pow_eq_pow_iff_modEq.mp collision) + + have h_zmod : (guess.m + a * guess.o : ZMod params.q) = (guess.m' + a * guess.o' : ZMod params.q) := by + have eq_cast : ((guess.m.val + a.val * guess.o.val : ℕ) : ZMod params.q) = + ((guess.m'.val + a.val * guess.o'.val : ℕ) : ZMod params.q) := + ZMod.natCast_eq_natCast_iff _ _ _ |>.mpr h_congr_nat + simp at eq_cast + exact eq_cast + + grind only + all_goals contradiction + + +lemma binding_as_hard_dlog + (A : G → PMF (BindingGuess (ZMod params.q) G (ZMod params.q))) : -- Pedersen adversary + Commitment.comp_binding_game (scheme) A 1 ≤ DLogExperiment (constructDlogAdversary A) 1 := by + unfold Commitment.comp_binding_game DLogExperiment constructDlogAdversary + + simp only [Pedersen.scheme, Pedersen.setup, Pedersen.verify] + + rw [PMF.bind_apply, PMF.bind_apply] + apply ENNReal.tsum_le_tsum + intro ⟨h, a⟩ + + by_cases h_case : h = params.g^a.val + + · -- Case: h = g^a.val (pair is in support of setup) + subst h_case + apply mul_le_mul_right + conv_rhs => rw [PMF.bind_bind] + + -- Same structure as above + rw [PMF.bind_apply, PMF.bind_apply] + apply ENNReal.tsum_le_tsum + intro guess + + apply mul_le_mul_right + + simp only [ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not, ne_eq, ite_not, + PMF.bind_apply, tsum_fintype] + rw [@DFunLike.ite_apply] + split_ifs with h₁ h₂ + + · -- Case 1: h₁ binding collision AND h₂ (o = o') + -- This is the contradiction case: o = o' + exfalso + obtain ⟨eq1, eq2, m_ne⟩ := h₁ + + have ho_eq : (params.g^a.val)^guess.o.val = (params.g^a.val)^guess.o'.val := by + rw [h₂] + + have collision : params.g^guess.m.val * (params.g^a.val)^guess.o.val = params.g^guess.m'.val * (params.g^a.val)^guess.o.val := by + calc params.g^guess.m.val * (params.g^a.val)^guess.o.val + = guess.c := eq1.symm + _ = params.g^guess.m'.val * (params.g^a.val)^guess.o'.val := eq2 + _ = params.g^guess.m'.val * (params.g^a.val)^guess.o.val := by rw [← ho_eq] + + have g_eq : params.g^guess.m.val = params.g^guess.m'.val := mul_right_cancel collision + + have h_congr : guess.m.val ≡ guess.m'.val [MOD params.q] := by + simpa [ordg_eq_q] using (pow_eq_pow_iff_modEq.mp g_eq) + + have m_eq : guess.m = guess.m' := by + have eq_cast : ((guess.m.val : ℕ) : ZMod params.q) = ((guess.m'.val : ℕ) : ZMod params.q) := + ZMod.natCast_eq_natCast_iff guess.m.val guess.m'.val params.q |>.mpr h_congr + simp at eq_cast + exact eq_cast + exact m_ne m_eq + + · -- Case 2: Binding collision (h₁) AND o ≠ o' (¬h₂) + -- This is the main case where we use binding_implies_dlog + have h_o_ne : guess.o ≠ guess.o' := h₂ + let x' := (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ + + have h₁' : (let h := params.g^a.val; + let verify := fun m c o => if c = params.g^m.val * h^o.val then (1 : ZMod 2) else 0; + verify guess.m guess.c guess.o = 1 ∧ verify guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m') := by + grind only + + have h_dlog : params.g^x'.val = params.g^a.val := by + apply binding_implies_dlog a guess h₁' h_o_ne + + -- The RHS is a sum over a single-element distribution (pure x') + -- The sum includes the term for x = x', which equals 1 + have h_term : (PMF.pure x') x' * (PMF.pure (if params.g^x'.val = params.g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) = 1 := by + simp only [h_dlog] + rw [PMF.pure_apply, PMF.pure_apply] + norm_num + + have h_zero : ∀ x ∈ Finset.univ, x ∉ ({x'} : Finset (ZMod params.q)) → + (PMF.pure x') x * (PMF.pure (if params.g^x.val = params.g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) = 0 := by + intros x _ hx + rw [PMF.pure_apply] + simp only [Finset.mem_singleton] at hx + simp [hx] + + have h_sum_ge : (PMF.pure x') x' * (PMF.pure (if params.g^x'.val = params.g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) ≤ + ∑ x, (PMF.pure x') x * (PMF.pure (if params.g^x.val = params.g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) := by + rw [← Finset.sum_subset (Finset.subset_univ {x'}) h_zero] + simp only [Finset.sum_singleton] + rfl + + calc (PMF.pure (1 : ZMod 2)) (1 : ZMod 2) + = 1 := by rw [PMF.pure_apply]; norm_num + _ = (PMF.pure x') x' * (PMF.pure (if params.g^x'.val = params.g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) := h_term.symm + _ ≤ ∑ x, (PMF.pure x') x * (PMF.pure (if params.g^x.val = params.g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) := h_sum_ge + + · -- Case 3: No collision (¬h₁) AND o = o' (h✝) + show (PMF.pure (0 : ZMod 2)) (1 : ZMod 2) ≤ _ + rw [PMF.pure_apply] + norm_num + + · -- Case 4: No collision (¬h₁) AND o ≠ o' (¬h✝) + show (PMF.pure (0 : ZMod 2)) (1 : ZMod 2) ≤ _ + rw [PMF.pure_apply] + norm_num + + · -- Case neg: h ≠ g^a.val (pair is NOT in support) + have h_prob_zero : ((PMF.uniformOfFintype (ZModMult params.q)).bind fun a_mult => PMF.pure (params.g^(val a_mult).val, val a_mult)) (h, a) = 0 := by + rw [PMF.bind_apply, tsum_fintype] + apply Finset.sum_eq_zero + intros a_mult _ + rw [PMF.pure_apply, PMF.uniformOfFintype_apply] + split_ifs with h_eq + · grind only + · simp only [mul_zero] + change ((PMF.uniformOfFintype (ZModMult params.q)).bind fun a_mult => PMF.pure (params.g^(val a_mult).val, val a_mult)) (h, a) * _ ≤ + ((PMF.uniformOfFintype (ZModMult params.q)).bind fun a_mult => PMF.pure (params.g^(val a_mult).val, val a_mult)) (h, a) * _ + rw [h_prob_zero] + simp only [zero_mul, le_refl] + +theorem computational_binding : + ∀ (ε : ENNReal), + (∀ (A' : G → PMF (ZMod params.q)), DLogExperiment A' 1 ≤ ε) → + (∀ (A : G → PMF (BindingGuess (ZMod params.q) G (ZMod params.q))), + Commitment.comp_binding_game (@scheme G params) A 1 ≤ ε) := by + intro ε A' A + exact le_trans (binding_as_hard_dlog A) (A' (constructDlogAdversary A)) + +end Binding + +end Pedersen diff --git a/VerifiedCommitments/PedersenBinding.lean b/VerifiedCommitments/PedersenBinding.lean deleted file mode 100644 index aaee00e..0000000 --- a/VerifiedCommitments/PedersenBinding.lean +++ /dev/null @@ -1,261 +0,0 @@ -import VerifiedCommitments.PedersenScheme -import VerifiedCommitments.dlog -import Mathlib.Tactic -import VerifiedCommitments.«scratch-skip-bind» - -namespace Pedersen - --- Helper lemma: if binding succeeds, then either o = o' or we can extract the discrete log -lemma binding_implies_dlog - (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] (hq_prime : Nat.Prime q) - (G_card_q : Fintype.card G = q) - (hg_gen : orderOf g = Fintype.card G) - (a : ZMod q) (guess : Adversary.guess (ZMod q) G (ZMod q)) : - let h := g ^ a.val - let verify := fun (m : ZMod q) (c : G) (o : ZMod q) => if c = g^m.val * h^o.val then (1 : ZMod 2) else 0 - (verify guess.m guess.c guess.o = 1 ∧ verify guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m') → - (guess.o ≠ guess.o' → g^(((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val) = h) := by - intro h verify ⟨h1, h2, m_ne⟩ o_ne - -- From h1: guess.c = g^(guess.m).val * h^(guess.o).val - -- From h2: guess.c = g^(guess.m').val * h^(guess.o').val - simp only [verify] at h1 h2 - split at h1 <;> split at h2 - case' isTrue.isTrue c_eq1 c_eq2 => - simp only [h] at c_eq1 c_eq2 - - have collision : g^guess.m.val * (g^a.val)^guess.o.val = g^guess.m'.val * (g^a.val)^guess.o'.val := by - rw [← c_eq1, c_eq2] - - conv_lhs at collision => arg 2; rw [← pow_mul] - conv_rhs at collision => arg 2; rw [← pow_mul] - rw [← pow_add, ← pow_add] at collision - - have h_coprime : (guess.o' - guess.o).val.Coprime q := by - cases' Nat.coprime_or_dvd_of_prime hq_prime (guess.o' - guess.o).val with h_cop h_dvd - · exact Nat.coprime_comm.mp h_cop - · exfalso - have h_zero : guess.o' - guess.o = 0 := by - rw [← ZMod.val_eq_zero] - have h_mod_zero : (guess.o' - guess.o).val % q = 0 := Nat.mod_eq_zero_of_dvd h_dvd - have h_val_bound : (guess.o' - guess.o).val < q := ZMod.val_lt (guess.o' - guess.o) - exact Nat.eq_zero_of_dvd_of_lt h_dvd h_val_bound - exact o_ne.symm (eq_of_sub_eq_zero h_zero) - - have h_ord : orderOf g = q := by - rw [← G_card_q]; exact hg_gen - - have h_congr_nat : guess.m.val + a.val * guess.o.val ≡ guess.m'.val + a.val * guess.o'.val [MOD q] := by - simpa [h_ord] using (pow_eq_pow_iff_modEq.mp collision) - - have h_zmod : (guess.m + a * guess.o : ZMod q) = (guess.m' + a * guess.o' : ZMod q) := by - have eq_cast : ((guess.m.val + a.val * guess.o.val : ℕ) : ZMod q) = - ((guess.m'.val + a.val * guess.o'.val : ℕ) : ZMod q) := - (ZMod.eq_iff_modEq_nat _).mpr h_congr_nat - simp at eq_cast - exact eq_cast - - have h_lin : a * (guess.o' - guess.o) = guess.m - guess.m' := by grind - - have h_unit : guess.o' - guess.o ≠ 0 := sub_ne_zero.mpr o_ne.symm - - have h_solve_x : a = (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ := by - calc a = a * 1 := by rw [mul_one] - _ = a * ((guess.o' - guess.o) * (guess.o' - guess.o)⁻¹) := by - haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩ - rw [← one_mul a] - congr 1 - have h_field_inv : (guess.o' - guess.o) * (guess.o' - guess.o)⁻¹ = 1 := by - apply Field.mul_inv_cancel - exact h_unit - exact h_field_inv.symm - _ = (a * (guess.o' - guess.o)) * (guess.o' - guess.o)⁻¹ := by rw [mul_assoc] - _ = (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ := by rw [h_lin] - - have h_congr_final : ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val ≡ a.val [MOD q] := by - have h1 : (((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val : ZMod q) = (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ := - ZMod.natCast_zmod_val ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹) - have h2 : (a.val : ZMod q) = a := ZMod.natCast_zmod_val a - rw [← ZMod.eq_iff_modEq_nat] - rw [h1, h2] - exact h_solve_x.symm - - have h_eq : g ^ ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val = g ^ a.val := - (pow_eq_pow_iff_modEq.mpr (by rwa [h_ord])) - - rw [h_eq] - all_goals contradiction - -lemma binding_as_hard_dlog - (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] (hq_prime : Nat.Prime q) - (G_card_q : Fintype.card G = q) - (hg_gen : orderOf g = Fintype.card G) - (A : G → PMF (Adversary.guess (ZMod q) G (ZMod q))) : -- Pedersen adversary - haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩; - Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ DLog.experiment G g q hq_prime (DLog.adversary' G q A) 1 := by - haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩ - -- Unfold definitions - unfold Commitment.comp_binding_game' DLog.experiment DLog.adversary' - simp only [Pedersen.scheme, Pedersen.setup, Pedersen.verify] - - -- Expand the bind applications - rw [PMF.bind_apply, PMF.bind_apply] - - -- Both sum over the same type: G × ZMod q (the pairs from setup) - -- We need pointwise inequality - apply ENNReal.tsum_le_tsum - intro ⟨h, a⟩ - - -- Key observation: setup only returns pairs (g^x.val, x) - -- So if h ≠ g^a.val, the probability of this pair is 0 and inequality holds trivially - by_cases h_case : h = g^a.val - - · -- Case: h = g^a.val (pair is in support of setup) - subst h_case -- Replace h with g^a.val everywhere - - -- Now we have h = g^a.val as needed! - apply mul_le_mul_right - - -- Now compare the inner probabilities - -- Continue with the proof that was already working - -- First, use bind associativity on RHS to flatten the nested binds - conv_rhs => rw [PMF.bind_bind] - - -- Now both have structure: (A (g^a.val)).bind (fun guess => ...) 1 - -- Expand the bind application - rw [PMF.bind_apply, PMF.bind_apply] - - -- Now both are sums over Adversary.guess - apply ENNReal.tsum_le_tsum - intro guess - - apply mul_le_mul_right - - -- For each guess, show: - -- (if [binding succeeds] then pure 1 else pure 0) 1 ≤ - -- ((if o≠o' then pure x' else uniform).bind (λ x'. pure (if g^x'=g^a then 1 else 0))) 1 - - simp only [ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not, ne_eq, ite_not, - PMF.bind_apply, tsum_fintype] - rw [@DFunLike.ite_apply] - split_ifs with h₁ h₂ - - · -- Case 1: h₁ (binding) AND h₂ (o = o') - -- This is the contradiction case: o = o' but binding succeeds - exfalso - obtain ⟨eq1, eq2, m_ne⟩ := h₁ - -- Since h₂: o = o', we have (g^a.val)^o.val = (g^a.val)^o'.val - have ho_eq : (g^a.val)^guess.o.val = (g^a.val)^guess.o'.val := by - rw [h₂] - -- So: g^m.val * (g^a.val)^o.val = g^m'.val * (g^a.val)^o.val - have collision : g^guess.m.val * (g^a.val)^guess.o.val = g^guess.m'.val * (g^a.val)^guess.o.val := by - calc g^guess.m.val * (g^a.val)^guess.o.val - = guess.c := eq1.symm - _ = g^guess.m'.val * (g^a.val)^guess.o'.val := eq2 - _ = g^guess.m'.val * (g^a.val)^guess.o.val := by rw [← ho_eq] - -- Cancel (g^a.val)^o.val from both sides - have g_eq : g^guess.m.val = g^guess.m'.val := mul_right_cancel collision - -- Since g is a generator, this means m.val ≡ m'.val (mod q) - have h_ord : orderOf g = q := by rw [← G_card_q]; exact hg_gen - have h_congr : guess.m.val ≡ guess.m'.val [MOD q] := by - simpa [h_ord] using (pow_eq_pow_iff_modEq.mp g_eq) - -- Therefore m = m' in ZMod q - have m_eq : guess.m = guess.m' := by - have eq_cast : ((guess.m.val : ℕ) : ZMod q) = ((guess.m'.val : ℕ) : ZMod q) := - ZMod.natCast_eq_natCast_iff guess.m.val guess.m'.val q |>.mpr h_congr - simp at eq_cast - exact eq_cast - exact m_ne m_eq - - · -- Case 2: Binding succeeds (h₁) AND o ≠ o' (¬h₂) - -- This is the main case where we use binding_implies_dlog - have h_o_ne : guess.o ≠ guess.o' := h₂ - let x' := (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ - - -- Convert h₁ to the form expected by binding_implies_dlog - have h₁' : (let h := g^a.val; - let verify := fun m c o => if c = g^m.val * h^o.val then (1 : ZMod 2) else 0; - verify guess.m guess.c guess.o = 1 ∧ verify guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m') := by - obtain ⟨eq1, eq2, m_ne⟩ := h₁ - simp only [] - refine ⟨?_, ?_, m_ne⟩ - · split - · rfl - · contradiction - · split - · rfl - · contradiction - - -- By binding_implies_dlog, g^x'.val = g^a.val - have h_dlog : g^x'.val = g^a.val := by - apply binding_implies_dlog G g q hq_prime G_card_q hg_gen a guess h₁' h_o_ne - - -- The RHS is a sum over a single-element distribution (pure x') - -- The sum includes the term for x = x', which equals 1 - have h_term : (PMF.pure x') x' * (PMF.pure (if g^x'.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) = 1 := by - rw [PMF.pure_apply, PMF.pure_apply] - simp only [h_dlog] - norm_num - have h_zero : ∀ x ∈ Finset.univ, x ∉ ({x'} : Finset (ZMod q)) → - (PMF.pure x') x * (PMF.pure (if g^x.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) = 0 := by - intros x _ hx - rw [PMF.pure_apply] - simp only [Finset.mem_singleton] at hx - simp [hx] - have h_sum_ge : (PMF.pure x') x' * (PMF.pure (if g^x'.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) ≤ - ∑ x, (PMF.pure x') x * (PMF.pure (if g^x.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) := by - rw [← Finset.sum_subset (Finset.subset_univ {x'}) h_zero] - simp only [Finset.sum_singleton] - rfl - calc (PMF.pure (1 : ZMod 2)) (1 : ZMod 2) - = 1 := by rw [PMF.pure_apply]; norm_num - _ = (PMF.pure x') x' * (PMF.pure (if g^x'.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) := h_term.symm - _ ≤ ∑ x, (PMF.pure x') x * (PMF.pure (if g^x.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) := h_sum_ge - - · -- Case 3: Binding fails (¬h₁) AND o = o' (h✝) - show (PMF.pure (0 : ZMod 2)) (1 : ZMod 2) ≤ _ - rw [PMF.pure_apply] - norm_num - - · -- Case 4: Binding fails (¬h₁) AND o ≠ o' (¬h✝) - show (PMF.pure (0 : ZMod 2)) (1 : ZMod 2) ≤ _ - rw [PMF.pure_apply] - norm_num - - · -- Case neg: h ≠ g^a.val (pair is NOT in support) - -- Setup only returns pairs of the form (g^x.val, x) - -- So if h ≠ g^a.val, then (h, a) has probability 0 in the setup distribution - -- Therefore both sides are 0 * something = 0, and 0 ≤ 0 - have h_prob_zero : ((PMF.uniformOfFintype (ZModMult q)).bind fun a_mult => PMF.pure (g^(val a_mult).val, val a_mult)) (h, a) = 0 := by - rw [PMF.bind_apply, tsum_fintype] - apply Finset.sum_eq_zero - intros a_mult _ - rw [PMF.pure_apply, PMF.uniformOfFintype_apply] - split_ifs with h_eq - · -- If (h, a) = (g^(val a_mult).val, val a_mult) - -- Then h = g^(val a_mult).val and a = val a_mult - exfalso - have eq_h : h = g^(val a_mult).val := (Prod.mk.injEq _ _ _ _).mp h_eq |>.1 - have eq_a : a = val a_mult := (Prod.mk.injEq _ _ _ _).mp h_eq |>.2 - rw [← eq_a] at eq_h - exact h_case eq_h - · simp - change ((PMF.uniformOfFintype (ZModMult q)).bind fun a_mult => PMF.pure (g^(val a_mult).val, val a_mult)) (h, a) * _ ≤ - ((PMF.uniformOfFintype (ZModMult q)).bind fun a_mult => PMF.pure (g^(val a_mult).val, val a_mult)) (h, a) * _ - rw [h_prob_zero] - simp only [zero_mul, le_refl] - - -theorem computational_binding : - ∀ (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] [Fact (Nat.Prime q)] (hq_prime : (Nat.Prime q)) (ε : ENNReal) - (G_card_q : Fintype.card G = q) - (hg_gen : orderOf g = Fintype.card G), - (∀ (A : G → PMF (ZMod q)), DLog.experiment G g q hq_prime A 1 ≤ ε) → - (∀ (A : G → PMF (Adversary.guess (ZMod q) G (ZMod q))), - ∃ hq_prime : Nat.Prime q, Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ ε) := by - intro G _ _ _ _ g q _ _ _ hq_prime ε G_card_q hg_gen hdlog A - use hq_prime - exact le_trans (binding_as_hard_dlog G g q hq_prime G_card_q hg_gen A) (hdlog (DLog.adversary' G q A)) -end Pedersen diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean deleted file mode 100644 index 5657287..0000000 --- a/VerifiedCommitments/PedersenHiding.lean +++ /dev/null @@ -1,248 +0,0 @@ -import VerifiedCommitments.PedersenScheme -import VerifiedCommitments.ZModUtil - --- Temporary -import VerifiedCommitments.«scratch-skip-bind» - -namespace Pedersen - -variable {G: Type} [Fintype G] [Group G] -variable (q : ℕ) [Fact (Nat.Prime q)] -variable (G_card_q : Fintype.card G = q) -variable (g : G) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g) -include G_card_q -include g_gen_G - --- Temporary? -variable [IsCyclic G] [DecidableEq G] (hq_prime : Nat.Prime q) - -lemma ordg_eq_q : orderOf g = q := by - have h_card_zpow : Fintype.card (Subgroup.zpowers g) = orderOf g := Fintype.card_zpowers - -- zpowers g has the same cardinality as G since g generates G - have h_card_eq : Fintype.card (Subgroup.zpowers g) = Fintype.card G := by - -- Every element of G is in zpowers g, so they're in bijection - have : Function.Bijective (Subtype.val : Subgroup.zpowers g → G) := by - constructor - · exact Subtype.val_injective - · intro x - use ⟨x, g_gen_G x⟩ - exact Fintype.card_of_bijective this - rw [← h_card_zpow, h_card_eq, G_card_q] - - -lemma exp_bij' (a : ZModMult q) (m : ZMod q) : Function.Bijective fun (r : ZMod q) => g^((m + (val a) * r : ZMod q).val : ℤ) := by - apply (Fintype.bijective_iff_surjective_and_card _).mpr - simp [G_card_q] - intro c --So take any cc ∈ GG - obtain ⟨k, hk⟩ := g_gen_G c - simp only at hk - simp only - - let z : ZMod q := (k : ZMod q) -- Since g is a generator we have c = g^z for some z ∈ Zq - have hk' : g ^ (z.val : ℤ) = c := by - rw [←hk] - simp only [ZMod.natCast_val] - rw [ZMod.coe_intCast] - rw [← G_card_q] - rw [@zpow_mod_card] - - -- we need g^m+a^r = g^z - -- This is the case iff m + ar ≡ z (mod q) - -- This is the case iff t ≡ a^−1 * (z − m) (mod q) - let a_unit := Units.mk0 (a.val : ZMod q) a.2 - let r : ZMod q := (a_unit⁻¹ : ZMod q) * (z - m) - have h_mod : (m + a_unit * r) = z := by - subst r - rw [IsUnit.mul_inv_cancel_left (Exists.intro a_unit rfl) (z - m)] - simp - - have h_pow : g^((m + a_unit * r).val : ℤ) = c := by - rw [←hk'] - subst r - rw [h_mod] - - rw [←ZMod.cast_eq_val] at h_pow -- Transfer ↑ and .val back to .cast - exact Exists.intro (r) h_pow - - --- Fintype instance for commit -instance {C O : Type} [Fintype C] [Fintype O] : Fintype (C × O) := - Fintype.ofEquiv (C × O) { - toFun := fun ⟨c, o⟩ => ⟨c, o⟩ - invFun := fun ⟨c, o⟩ => ⟨c, o⟩ - left_inv := fun _ => rfl - right_inv := fun x => by cases x; rfl - } - -noncomputable def expEquiv (a : ZModMult q) (m : ZMod q) : ZMod q ≃ G := -Equiv.ofBijective (fun (r : ZMod q) => g^((m + (val a) * r : ZMod q).val : ℤ)) (exp_bij' q G_card_q g g_gen_G a m) - - -#check expEquiv q G_card_q g g_gen_G - -lemma expEquiv_unfold (a : ZModMult q) (m r : ZMod q) : - expEquiv q G_card_q g g_gen_G a m r = g^m.val * (g^(val a).val)^r.val := by - unfold expEquiv - simp only [Equiv.ofBijective, Equiv.coe_fn_mk] - - have h_pow : (g^(val a).val)^r.val = g^((val a).val * r.val) := (pow_mul g (val a).val r.val).symm - rw [h_pow] - - simp only [← zpow_natCast] - rw [← zpow_add] - - have hord : orderOf g = q := ordg_eq_q q G_card_q g g_gen_G - conv_lhs => rw [← zpow_mod_orderOf, hord] - - suffices h : (((m + (val a) * r).val : ℤ) % ↑q) = ((m.val : ℤ) + ((val a).val * r.val : ℤ)) % ↑q by - conv_rhs => rw [← zpow_mod_orderOf, hord] - rw [h] - congr 1 - - conv_lhs => rw [ZMod.val_add, ZMod.val_mul] - norm_cast - rw [Nat.add_mod, Nat.mul_mod] - simp - - -open Classical -- needed here or α must be DecidableEq -/-! ### 2. Mapping a uniform PMF through a bijection stays uniform -------------/ --- Courtesy of formalmethods.io -lemma map_uniformOfFintype_equiv - {α β : Type*} [Fintype α] [Fintype β] [DecidableEq β] [Nonempty α] [Nonempty β] - (e : α ≃ β) : - PMF.map e (PMF.uniformOfFintype α) = PMF.uniformOfFintype β := by - -- Prove equality of PMFs by showing they assign the same probability to each element - ext b - -- Goal: (PMF.map e (uniformOfFintype α)) b = (uniformOfFintype β) b - - -- Step 1: Simplify the LHS using PMF.map_apply - rw [PMF.map_apply] - -- This gives us: ∑' (a : α), if b = e a then (uniformOfFintype α) a else 0 - - -- Step 2: Simplify the uniform distribution on α - simp only [PMF.uniformOfFintype_apply] - -- Goal: ∑' (a : α), if b = e a then (↑(card α))⁻¹ else 0 = (↑(card β))⁻¹ - - -- Step 3: The sum has exactly one non-zero term when a = e.symm b - -- We can rewrite this as a sum over the singleton {e.symm b} - have h_equiv : (∑' (a : α), if b = e a then (↑(Fintype.card α : ENNReal))⁻¹ else 0) = - (∑' (a : α), if a = e.symm b then (↑(Fintype.card α))⁻¹ else 0) := by - congr 1 - ext a - -- Show: (if b = e a then (↑(card α))⁻¹ else 0) = (if a = e.symm b then (↑(card α))⁻¹ else 0) - by_cases h : b = e a - · -- Case: b = e a - rw [if_pos h, if_pos] - -- Need to show a = e.symm b - rw [←Equiv.symm_apply_apply e a] - rw [h] - · -- Case: b ≠ e a - rw [if_neg h, if_neg] - -- Need to show a ≠ e.symm b - intro contra - subst contra - rw [Equiv.apply_symm_apply e] at h - apply h - rfl - - -- Step 4: Apply the equivalence and simplify - rw [h_equiv] - rw [tsum_ite_eq] - -- Goal: (↑(card α))⁻¹ = (↑(card β))⁻¹ - - -- Step 5: Use the fact that equivalent finite types have the same cardinality - congr 1 - rw [Fintype.card_congr e] - -lemma bind_eq_map - {α β : Type*} [Fintype α] [Fintype β] [DecidableEq β] [Nonempty α] [Nonempty β] - (e : α ≃ β) : - PMF.map e (PMF.uniformOfFintype α) = PMF.bind (PMF.uniformOfFintype α) (fun a => pure (e a)) := by - rfl - -lemma bind_eq_map' : ∀ (fixed_a : ZModMult q) (fixed_m : ZMod q), - PMF.map (expEquiv q G_card_q g g_gen_G fixed_a fixed_m) (PMF.uniformOfFintype (ZMod q)) = - PMF.bind (PMF.uniformOfFintype (ZMod q)) (fun a => PMF.pure (expEquiv q G_card_q g g_gen_G fixed_a fixed_m a)) - := by - intros - exact rfl - -lemma bij_uniform_for_fixed_a (a : ZModMult q) (m : ZMod q) : - PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)) = (PMF.uniformOfFintype G) := by - · expose_names; - exact map_uniformOfFintype_equiv q G_card_q g g_gen_G (expEquiv q G_card_q g g_gen_G a m) - -lemma bij_uniform_for_uniform_a (m : ZMod q) : - (PMF.bind (generate_a q) - (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)))) = (PMF.uniformOfFintype G) := by - unfold generate_a - apply bind_skip_const' - intro a - · expose_names; exact bij_uniform_for_fixed_a q G_card_q g g_gen_G a m - -lemma pedersen_commitment_uniform (m : ZMod q) (c : G) : - (PMF.map Prod.fst ((PMF.bind (generate_a q) - (fun a => Pedersen.commit G g q (g^(val a).val) m ))) c) = - ((1 : ENNReal) / (Fintype.card G)) := by - unfold Pedersen.commit - simp only [PMF.map_bind, pure, PMF.pure_map] - have h_eq : (PMF.bind (generate_a q) - (fun a => PMF.bind (PMF.uniformOfFintype (ZMod q)) - (fun r => PMF.pure (g^m.val * (g^(val a).val)^r.val)))) = - (PMF.bind (generate_a q) - (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)))) := by - apply bind_skip' - intro a - ext x - simp only [PMF.bind_apply, PMF.map_apply, PMF.pure_apply, PMF.uniformOfFintype_apply] - congr 1; ext r - by_cases h : x = g^m.val * (g^(val a).val)^r.val - · simp only [h, ↓reduceIte] - rw [← expEquiv_unfold q G_card_q g g_gen_G a m r] - simp - · simp only [h, ↓reduceIte] - have : x ≠ expEquiv q G_card_q g g_gen_G a m r := by - intro contra - rw [expEquiv_unfold q G_card_q g g_gen_G a m r] at contra - exact h contra - simp [this] - rw [h_eq] - rw [bij_uniform_for_uniform_a q G_card_q g g_gen_G m] - simp [PMF.uniformOfFintype_apply] - - -end Pedersen - -theorem Pedersen.perfect_hiding : ∀ (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) - (G_card_q : Fintype.card G = q) - (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g), - haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩; Commitment.perfect_hiding (Pedersen.scheme G g q hq_prime) := by - intros G _ _ _ _ g q _ hq_prime G_card_q g_gen_G - haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩ - unfold Commitment.perfect_hiding - intros m m' c - unfold Commitment.do_commit Pedersen.scheme - simp only [] - unfold Pedersen.setup Pedersen.commit - simp only [PMF.bind_bind] - have h_lhs : ((PMF.uniformOfFintype (ZModMult q)).bind fun a => - PMF.bind (pure (g^(val a).val, val a)) fun h => - (PMF.uniformOfFintype (ZMod q)).bind fun r => - PMF.bind (pure (g^m.val * h.1^r.val, r)) fun commit => - pure commit.1) c = 1 / Fintype.card G := by - simp only [pure, PMF.pure_bind] - convert pedersen_commitment_uniform q G_card_q g g_gen_G m c using 2 - unfold generate_a Pedersen.commit - simp only [PMF.map_bind, pure, PMF.pure_map] - have h_rhs : ((PMF.uniformOfFintype (ZModMult q)).bind fun a => - PMF.bind (pure (g^(val a).val, val a)) fun h => - (PMF.uniformOfFintype (ZMod q)).bind fun r => - PMF.bind (pure (g^m'.val * h.1^r.val, r)) fun commit => - pure commit.1) c = 1 / Fintype.card G := by - simp only [pure, PMF.pure_bind] - convert pedersen_commitment_uniform q G_card_q g g_gen_G m' c using 2 - unfold generate_a Pedersen.commit - simp only [PMF.map_bind, pure, PMF.pure_map] - rw [h_lhs, h_rhs] diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean deleted file mode 100644 index f78a6e0..0000000 --- a/VerifiedCommitments/PedersenScheme.lean +++ /dev/null @@ -1,42 +0,0 @@ -import VerifiedCommitments.CommitmentScheme -import Mathlib.Probability.Distributions.Uniform -import VerifiedCommitments.ZModUtil - -namespace Pedersen - --- TODO: I'm not sure this should be here, or that --- Setup should definitely return h, but should there be another def hanging around that computes an a independently? --- The two alternatives below for bind in setup may have some bearing on how the binding proof progresses, unless I change the dlog definitions to match... - -noncomputable def generate_a (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] : PMF (ZModMult q) := - PMF.uniformOfFintype (ZModMult q) - - -noncomputable section - - def setup (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (hq_prime : Nat.Prime q) : PMF (G × (ZMod q)) := - PMF.bind (PMF.uniformOfFintype (ZModMult q)) (fun a => return ⟨g^(val a).val, val a⟩) - -- PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val) - - def commit (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] (h : G) (m : ZMod q) : PMF (G × (ZMod q)) := - PMF.bind (PMF.uniformOfFintype (ZMod q)) (fun r => return ⟨g^m.val * h^r.val, r⟩) - - def verify (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] (h : G) (m : ZMod q) (c : G) (o : ZMod q): ZMod 2 := - if c = g^m.val * h^o.val then 1 else 0 - - def scheme - (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (hq_prime : Nat.Prime q) : - CommitmentScheme (ZMod q) G (ZMod q) G := { - setup := setup G g q hq_prime, - commit (h : G) (m : ZMod q) := commit G g q h m, - verify (h : G) (m : ZMod q) (c : G) (o : ZMod q):= verify G g q h m c o - } - -end -end Pedersen - -instance {G : Type} {q : ℕ} [NeZero q] : Nonempty (G × (ZMod q)) := sorry diff --git a/VerifiedCommitments/ZModUtil.lean b/VerifiedCommitments/ZModUtil.lean index def9da1..fa2f45a 100644 --- a/VerifiedCommitments/ZModUtil.lean +++ b/VerifiedCommitments/ZModUtil.lean @@ -19,6 +19,10 @@ def ZModMult (q : ℕ) [NeZero q] := {a : ZMod q // a ≠ 0} -- Helper function to extract the value from ZModMult def val {q : ℕ} [NeZero q] (a : ZModMult q) : ZMod q := a.val +lemma ZModMult.coe_ne_zero {q : ℕ} [NeZero q] (a : ZModMult q) : (val a : ZMod q) ≠ 0 := + a.property + + -- Fintype instance for ZModMult instance {q : ℕ} [NeZero q] : Fintype (ZModMult q) := Fintype.subtype ((Finset.univ : Finset (ZMod q)).erase 0) (by simp [Finset.mem_erase]) diff --git a/VerifiedCommitments/cryptolib.lean b/VerifiedCommitments/cryptolib.lean new file mode 100644 index 0000000..3bad996 --- /dev/null +++ b/VerifiedCommitments/cryptolib.lean @@ -0,0 +1,18 @@ +-- From cryptolib licensed under Apache 2.0 +-- https://github.com/joeylupo/cryptolib + +import Mathlib.Probability.ProbabilityMassFunction.Monad + +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 only [PMF.bind_apply, ha] + +lemma bind_skip_const' (pa : PMF α) (pb : PMF β) (f : α → PMF β) : (∀ (a : α), f a = pb) → pa.bind f = pb := by + intros ha + ext + simp + simp_rw [ha] + simp [ENNReal.tsum_mul_right] diff --git a/VerifiedCommitments/dlog.lean b/VerifiedCommitments/dlog.lean deleted file mode 100644 index 60fe676..0000000 --- a/VerifiedCommitments/dlog.lean +++ /dev/null @@ -1,50 +0,0 @@ -import VerifiedCommitments.PedersenScheme - -namespace DLog - -noncomputable section - --- Modification of Attack game and advantage as specified in Boneh 10.4 to account for check between generated x and x' -def attack_game (G : Type) [Group G] (q : ℕ) [NeZero q] (g : G) (A : G → PMF (ZMod q)) : PMF (ZMod 2) := -PMF.bind (PMF.uniformOfFintype (ZMod q)) (fun x => - PMF.bind (A (g^x.val)) (fun x' => pure (if x = x' then 1 else 0))) - --- The advantage of an attacker A in the DLog problem --- attack_game returns a PMF () -def advantage (G : Type) [Group G] (q : ℕ) [NeZero q] (g : G) (A : G → PMF (ZMod q)) : ENNReal := attack_game G q g A 1 - -#check Pedersen.scheme -noncomputable def experiment - (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G) - (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (hq_prime : Nat.Prime q) - (A' : G → PMF (ZMod q)) : PMF (ZMod 2) := - PMF.bind (Pedersen.scheme G g q hq_prime).setup (fun h => - PMF.bind (A' h.1) (fun x' => pure (if g^x'.val = g^(h.2).val then 1 else 0))) - -- PMF.bind (PMF.uniformOfFintype (ZModMult q)) (fun x => - -- PMF.bind (A' (g^(val x).val)) (fun x' => pure (if g^x'.val = g^(val x).val then 1 else 0))) - - noncomputable def adversary - (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] - (q : ℕ) [NeZero q] - (A : G → PMF (G × ZMod q × ZMod q × ZMod q × ZMod q)) - (h : G) : PMF (ZMod q) := - PMF.bind (A h) (fun (_c, m, m', o, o') => - if o ≠ o' then - return ((m - m') * (o' - o)⁻¹) - else - PMF.uniformOfFintype (ZMod q) - ) - - noncomputable def adversary' - (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] - (q : ℕ) [NeZero q] - (A' : G → PMF (Adversary.guess (ZMod q) G (ZMod q))) - (h : G) : PMF (ZMod q) := - PMF.bind (A' h) (fun guess => - if guess.o ≠ guess.o' then - return ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹) - else - PMF.uniformOfFintype (ZMod q) - ) -end -end DLog