diff --git a/Complexity/Crypto/Computational/Nonuniform/Basic.lean b/Complexity/Crypto/Computational/Nonuniform/Basic.lean index 5da5039116..995515ac49 100644 --- a/Complexity/Crypto/Computational/Nonuniform/Basic.lean +++ b/Complexity/Crypto/Computational/Nonuniform/Basic.lean @@ -27,12 +27,13 @@ family need not be computable, so it can hard-wire information about every param `NonuniformlyIndistinguishable`, `NonuniformOneWay` and `NonuniformPRG` relativize `ComputationallyIndistinguishable`, `OneWay` and `PseudorandomGenerator` to this class. Each uniform adversary is an advice adversary that ignores empty advice, so every nonuniform notion -implies its uniform counterpart. `IndistinguishableWithAdvice advice` fixes one advice family; -with empty advice it is exactly uniform indistinguishability, so a reduction proved relative to a -fixed family yields both the uniform and the nonuniform theorem. Moreover, an advice word may carry -a value of any type under any encoding (`IndistinguishableWithAdvice.negligible_encoded`, -`NonuniformOneWay.inversion_negligible_encoded`): an adversary need not decode its advice, since -it may run on the encoded word exactly as on the typed value. +implies its uniform counterpart. `IndistinguishableWithAdvice advice` and +`InversionHardWithAdvice f advice` fix one advice family; with empty advice they are exactly the +uniform notions, so a reduction proved relative to a fixed family yields both the uniform and the +nonuniform theorem. Moreover, an advice word may carry a value of any type under any encoding +(`IndistinguishableWithAdvice.negligible_encoded`, +`InversionHardWithAdvice.inversion_negligible_encoded`): an adversary need not decode its advice, +since it may run on the encoded word exactly as on the typed value. These are definitions, not assertions that such primitives exist. @@ -42,6 +43,8 @@ These are definitions, not assertions that such primitives exist. tests given one fixed advice family. * `Cslib.Crypto.NonuniformlyIndistinguishable`: indistinguishability with every polynomially bounded advice family. +* `Cslib.Crypto.InversionHardWithAdvice`: hardness of inversion against uniform strict PPT + inverters given one fixed advice family. * `Cslib.Crypto.NonuniformOneWay`: one-wayness against inverters given polynomially bounded advice. * `Cslib.Crypto.NonuniformPRG`: a stretching generator whose output is nonuniformly @@ -60,7 +63,9 @@ These are definitions, not assertions that such primitives exist. indistinguishability is indistinguishability with empty advice. * `Cslib.Crypto.IndistinguishableWithAdvice.map`: efficient postprocessing. * `Cslib.Crypto.IndistinguishableWithAdvice.negligible_encoded`, - `Cslib.Crypto.NonuniformOneWay.inversion_negligible_encoded`: advice of any encoded type. + `Cslib.Crypto.InversionHardWithAdvice.inversion_negligible_encoded`: advice of any encoded type. +* `Cslib.Crypto.oneWay_iff_inversionHardWithAdvice_nil`: uniform one-wayness is hardness of + inversion with empty advice. * `Cslib.Crypto.not_computationallyIndistinguishable_pure_uniformList`, `Cslib.Crypto.not_nonuniformlyIndistinguishable_pure_uniformList`: fixed words are distinguishable from uniform words, so the indistinguishability notions are not trivially true. @@ -219,51 +224,45 @@ theorem not_nonuniformlyIndistinguishable_pure_uniformList (target : ℕ → Lis not_computationallyIndistinguishable_pure_uniformList target hlength h.computationallyIndistinguishable -/-- A function is **nonuniformly one-way** when one deterministic polynomial-time algorithm -evaluates it and, for every polynomially bounded advice family, each uniform strict PPT inverter -reading the parameter, the advice word and the image has negligible probability of finding any -preimage of a uniform input. -/ -structure NonuniformOneWay (f : List Bool → List Bool) : Prop where - /-- A deterministic polynomial-time algorithm evaluates the function. -/ - polyTime : ComputableInPolyTime f encBits encBits - /-- With each polynomially bounded advice family, inversion is indistinguishable from certain - failure. -/ - secure : ∀ advice : ℕ → List Bool, PolynomiallyBounded (fun n => (advice n).length) → - Game.Indistinguishable - (fun (adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool)) n => - ProbComp.eval (inversionGame f (fun n image => adversary ((n, advice n), image)) n)) - (fun _ _ => PMF.pure false) (IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits) - -/-- Each efficient inverter with polynomially bounded advice has negligible success. -/ -theorem NonuniformOneWay.inversion_negligible {f : List Bool → List Bool} - (h : NonuniformOneWay f) (adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool)) - (hPPT : IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits adversary) - {advice : ℕ → List Bool} (hadvice : PolynomiallyBounded (fun n => (advice n).length)) : +/-- **Inversion of `f` is hard with advice** `advice` when each uniform strict PPT inverter +reading the parameter `n`, the advice word `advice n` and the image of a uniform `n`-bit input has +negligible probability of finding any preimage. The advice family is not bounded here; its length +is charged to the inverter's clock. With empty advice this is the security condition of `OneWay` +(`oneWay_iff_inversionHardWithAdvice_nil`). -/ +def InversionHardWithAdvice (f : List Bool → List Bool) (advice : ℕ → List Bool) : Prop := + Game.Indistinguishable + (fun (adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool)) n => + ProbComp.eval (inversionGame f (fun n image => adversary ((n, advice n), image)) n)) + (fun _ _ => PMF.pure false) (IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits) + +/-- Each efficient inverter with the given advice has negligible success. -/ +theorem InversionHardWithAdvice.inversion_negligible {f : List Bool → List Bool} + {advice : ℕ → List Bool} (h : InversionHardWithAdvice f advice) + (adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool)) + (hPPT : IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits adversary) : Negligible (fun n => Game.succProbability (ProbComp.eval (inversionGame f (fun n image => adversary ((n, advice n), image)) n))) := by - simpa only [Game.advantage_pure_false] using h.secure advice hadvice adversary hPPT + simpa only [Game.advantage_pure_false] using h adversary hPPT -/-- Establish nonuniform one-wayness by bounding the success probability of every efficient -inverter with polynomially bounded advice. -/ -theorem NonuniformOneWay.of_inversion_negligible {f : List Bool → List Bool} - (hf : ComputableInPolyTime f encBits encBits) +/-- Establish hardness with advice by bounding every efficient inverter's success +probability. -/ +theorem InversionHardWithAdvice.of_inversion_negligible {f : List Bool → List Bool} + {advice : ℕ → List Bool} (h : ∀ adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool), IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits adversary → - ∀ advice : ℕ → List Bool, PolynomiallyBounded (fun n => (advice n).length) → Negligible (fun n => Game.succProbability (ProbComp.eval (inversionGame f (fun n image => adversary ((n, advice n), image)) n)))) : - NonuniformOneWay f := by - refine ⟨hf, fun advice hadvice adversary hPPT => ?_⟩ - simpa only [Game.advantage_pure_false] using h adversary hPPT advice hadvice - -/-- **Advice of any encoded type.** A nonuniformly one-way function resists every uniform strict -PPT inverter reading an advice value of an arbitrary type, under an arbitrary encoding with -polynomially bounded lengths. -/ -theorem NonuniformOneWay.inversion_negligible_encoded {f : List Bool → List Bool} - (h : NonuniformOneWay f) {γ : Type} {encAdvice : γ ↪ List Bool} + InversionHardWithAdvice f advice := fun adversary hPPT => by + simpa only [Game.advantage_pure_false] using h adversary hPPT + +/-- **Advice of any encoded type.** Hardness with the advice words `encAdvice (advice n)` covers +every uniform strict PPT inverter that reads the advice value `advice n` itself, of an arbitrary +type under an arbitrary encoding. -/ +theorem InversionHardWithAdvice.inversion_negligible_encoded {f : List Bool → List Bool} + {γ : Type} {encAdvice : γ ↪ List Bool} {advice : ℕ → γ} + (h : InversionHardWithAdvice f (fun n => encAdvice (advice n))) {adversary : (ℕ × γ) × List Bool → ProbComp (List Bool)} - (hPPT : IsPPTOn (encPair (encPair encUnary encAdvice) encBits) encBits adversary) - {advice : ℕ → γ} (hadvice : PolynomiallyBounded (fun n => (encAdvice (advice n)).length)) : + (hPPT : IsPPTOn (encPair (encPair encUnary encAdvice) encBits) encBits adversary) : Negligible (fun n => Game.succProbability (ProbComp.eval (inversionGame f (fun n image => adversary ((n, advice n), image)) n))) := by obtain ⟨extension, hextension, heq⟩ := @@ -280,16 +279,62 @@ theorem NonuniformOneWay.inversion_negligible_encoded {f : List Bool → List Bo (encPair (encPair encUnary encBits) encBits ((n, encAdvice (advice n)), image))) n) = ProbComp.eval (inversionGame f (fun n image => adversary ((n, advice n), image)) n) := by simp only [inversionGame, ProbComp.eval_bind, hkey] - simpa only [hgame] using h.inversion_negligible _ hword hadvice + simpa only [hgame] using h.inversion_negligible _ hword + +/-- **Uniform one-wayness is the empty-advice case.** A uniform inverter is an advice inverter +that ignores its advice, and an advice inverter run on empty advice is a uniform inverter. -/ +theorem oneWay_iff_inversionHardWithAdvice_nil {f : List Bool → List Bool} : + OneWay f ↔ + ComputableInPolyTime f encBits encBits ∧ InversionHardWithAdvice f (fun _ => []) := by + constructor + · intro h + refine ⟨h.polyTime, .of_inversion_negligible fun adversary hPPT => ?_⟩ + have hprepare : ComputableInPolyTime (fun input : ℕ × List Bool => ((input.1, []), input.2)) + (encPair encUnary encBits) (encPair (encPair encUnary encBits) encBits) := by fun_prop + exact h.inversion_negligible (fun n image => adversary ((n, []), image)) + (hPPT.preprocess hprepare) + · rintro ⟨hf, h⟩ + refine OneWay.of_inversion_negligible hf fun adversary hPPT => ?_ + have hneg := h.inversion_negligible (fun input => adversary input.1.1 input.2) + (isPPTOn_dropAdvice hPPT) + simpa only using hneg + +/-- A function is **nonuniformly one-way** when one deterministic polynomial-time algorithm +evaluates it and inversion is hard with every polynomially bounded advice family. -/ +structure NonuniformOneWay (f : List Bool → List Bool) : Prop where + /-- A deterministic polynomial-time algorithm evaluates the function. -/ + polyTime : ComputableInPolyTime f encBits encBits + /-- With each polynomially bounded advice family, inversion is hard. -/ + secure : ∀ advice : ℕ → List Bool, PolynomiallyBounded (fun n => (advice n).length) → + InversionHardWithAdvice f advice + +/-- Each efficient inverter with polynomially bounded advice has negligible success. -/ +theorem NonuniformOneWay.inversion_negligible {f : List Bool → List Bool} + (h : NonuniformOneWay f) (adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool)) + (hPPT : IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits adversary) + {advice : ℕ → List Bool} (hadvice : PolynomiallyBounded (fun n => (advice n).length)) : + Negligible (fun n => Game.succProbability (ProbComp.eval + (inversionGame f (fun n image => adversary ((n, advice n), image)) n))) := + (h.secure advice hadvice).inversion_negligible adversary hPPT + +/-- Establish nonuniform one-wayness by bounding the success probability of every efficient +inverter with polynomially bounded advice. -/ +theorem NonuniformOneWay.of_inversion_negligible {f : List Bool → List Bool} + (hf : ComputableInPolyTime f encBits encBits) + (h : ∀ adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool), + IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits adversary → + ∀ advice : ℕ → List Bool, PolynomiallyBounded (fun n => (advice n).length) → + Negligible (fun n => Game.succProbability (ProbComp.eval + (inversionGame f (fun n image => adversary ((n, advice n), image)) n)))) : + NonuniformOneWay f := + ⟨hf, fun advice hadvice => + .of_inversion_negligible fun adversary hPPT => h adversary hPPT advice hadvice⟩ /-- Nonuniform one-wayness implies uniform one-wayness: a uniform inverter ignores empty advice. -/ theorem NonuniformOneWay.toOneWay {f : List Bool → List Bool} (h : NonuniformOneWay f) : - OneWay f := by - refine OneWay.of_inversion_negligible h.polyTime fun adversary hPPT => ?_ - have hneg := h.inversion_negligible (fun input => adversary input.1.1 input.2) - (isPPTOn_dropAdvice hPPT) (advice := fun _ => []) (PolynomiallyBounded.const 0) - simpa only using hneg + OneWay f := + oneWay_iff_inversionHardWithAdvice_nil.mpr ⟨h.polyTime, h.secure _ (PolynomiallyBounded.const 0)⟩ /-- A **nonuniform pseudorandom generator**: a plain polynomial-time generator with exact output length `length`, strictly expanding every seed length, whose output on a uniform seed is diff --git a/Complexity/Crypto/Computational/OneWay/Normalize.lean b/Complexity/Crypto/Computational/OneWay/Normalize.lean index 4e9a651799..993086580d 100644 --- a/Complexity/Crypto/Computational/OneWay/Normalize.lean +++ b/Complexity/Crypto/Computational/OneWay/Normalize.lean @@ -7,6 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Crypto.Computational.Nonuniform.Basic public import Complexity.Crypto.Computational.OneWay public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Padding import Complexity.Probability.PMF.Bind @@ -19,7 +20,8 @@ import Complexity.Tactic.PPT Self-delimiting padding using an output-size bound makes the output length depend only on the input length. Equality of padded images implies equality of the original images, even for a -candidate of a different length. A uniform strict PPT reduction therefore preserves one-wayness. +candidate of a different length. A uniform strict PPT reduction, which passes any advice through +unchanged, therefore preserves one-wayness, uniform or nonuniform. This supplies the fixed-output-width interface used by the pseudoentropy construction without assuming that the original function is length-preserving, injective or regular. @@ -29,9 +31,13 @@ assuming that the original function is length-preserving, injective or regular. ## Main results -* `Cslib.Crypto.OneWay.normalize`: output normalization preserves one-wayness. -* `Cslib.Crypto.OneWay.exists_fixedOutputLength`: every OWF yields an OWF with - a uniformly polynomial-time output-length function. +* `Cslib.Crypto.InversionHardWithAdvice.normalize`: output normalization preserves hardness of + inversion with any fixed advice family. +* `Cslib.Crypto.OneWay.normalize`, `Cslib.Crypto.NonuniformOneWay.normalize`: output + normalization preserves uniform and nonuniform one-wayness. +* `Cslib.Crypto.OneWay.exists_fixedOutputLength`, + `Cslib.Crypto.NonuniformOneWay.exists_fixedOutputLength`: every (nonuniform) OWF yields one + with a uniformly polynomial-time output-length function. ## References @@ -40,7 +46,7 @@ assuming that the original function is length-preserving, injective or regular. Adapted from Crypto/Computational/OneWay/Normalize.lean on the cslib `crypto` branch at `5ff69ca93402e7c947208dc56396d6d86203ccd8`. This is the word-encoding reduction to the write-up's -fixed-output-width setting, using the shared tidy machine calculus and nonnegative game API. +fixed-output-width setting, using plain polynomial-time certificates and the nonnegative game API. -/ @[expose] public section @@ -86,19 +92,44 @@ theorem inversion_le (f : List Bool → List Bool) (bound : ℕ → ℕ) (advers end OneWayNormalization +/-- **Normalization relative to fixed advice.** Self-delimiting output padding preserves hardness +of inversion with any fixed advice family: the reduction pads its challenge and passes the advice +through. Uniform one-wayness (`OneWay.normalize`) is the empty-advice case. -/ +theorem InversionHardWithAdvice.normalize {f : List Bool → List Bool} {advice : ℕ → List Bool} + (h : InversionHardWithAdvice f advice) (bound : ℕ → ℕ) + (hbound : ComputableInPolyTime bound encUnary encUnary) : + InversionHardWithAdvice (OneWayNormalization.normalize f bound) advice := by + refine .of_inversion_negligible fun adversary hPPT => ?_ + have hprepare : ComputableInPolyTime + (fun ((n, word), image) => ((n, word), BitString.padWord (bound n) image)) + (encPair (encPair encUnary encBits) encBits) + (encPair (encPair encUnary encBits) encBits) := by fun_prop + exact negligible_of_le (h.inversion_negligible _ (hPPT.preprocess hprepare)) + (OneWayNormalization.inversion_le f bound (fun n image => adversary ((n, advice n), image))) + /-- Self-delimiting output padding preserves one-wayness against uniform strict PPT inverters. -/ theorem OneWay.normalize {f : List Bool → List Bool} (hf : OneWay f) (bound : ℕ → ℕ) (hbound : ComputableInPolyTime bound encUnary encUnary) : OneWay (OneWayNormalization.normalize f bound) := by - have hbound := hbound.tidy - apply OneWay.of_inversion_negligible - (.of_tidy <| - (OneWayNormalization.computableInPolyTime_normalize hf.polyTime (.of_tidy hbound)).tidy) - intro adversary hPPT - have hreduce : IsPPT encBits (fun n image => - adversary n (BitString.padWord (bound n) image)) := by ppt - exact negligible_of_le (hf.inversion_negligible _ hreduce) - (OneWayNormalization.inversion_le f bound adversary) + obtain ⟨hpoly, hhard⟩ := oneWay_iff_inversionHardWithAdvice_nil.mp hf + exact oneWay_iff_inversionHardWithAdvice_nil.mpr + ⟨OneWayNormalization.computableInPolyTime_normalize hpoly hbound, hhard.normalize bound hbound⟩ + +/-- Self-delimiting output padding preserves nonuniform one-wayness. -/ +theorem NonuniformOneWay.normalize {f : List Bool → List Bool} (hf : NonuniformOneWay f) + (bound : ℕ → ℕ) (hbound : ComputableInPolyTime bound encUnary encUnary) : + NonuniformOneWay (OneWayNormalization.normalize f bound) := + ⟨OneWayNormalization.computableInPolyTime_normalize hf.polyTime hbound, + fun advice hadvice => (hf.secure advice hadvice).normalize bound hbound⟩ + +/-- The output-size bound used to normalize an efficient function: a polynomial dominating its +output length. -/ +private theorem exists_normalizationBound {f : List Bool → List Bool} + (hf : ComputableInPolyTime f encBits encBits) : + ∃ bound : ℕ → ℕ, ComputableInPolyTime bound encUnary encUnary ∧ + ∀ input, (f input).length ≤ bound input.length := by + obtain ⟨c, d, hsize⟩ := hf.polyBounded_length.exists_le + exact ⟨fun n => c * (n + 1) ^ d, by fun_prop, hsize⟩ /-- Every OWF yields an OWF whose output length depends only on the input length. Both evaluation and this unary output-length function are uniformly polynomial time. -/ @@ -106,15 +137,19 @@ theorem OneWay.exists_fixedOutputLength {f : List Bool → List Bool} (hf : OneW ∃ (g : List Bool → List Bool) (length : ℕ → ℕ), OneWay g ∧ (∀ input, (g input).length = length input.length) ∧ ComputableInPolyTime length encUnary encUnary := by - simp only [Turing.MultiTapeTM.computableInPolyTime_iff_computableTidilyInPolyTime] - obtain ⟨c, d, hsize⟩ := hf.polyTime.polyBounded_length.exists_le - let bound (n : ℕ) := c * (n + 1) ^ d - have hbound : ComputableTidilyInPolyTime bound encUnary encUnary := by - unfold bound - fun_prop - refine ⟨OneWayNormalization.normalize f bound, fun n => 2 * bound n + 1, - hf.normalize bound (.of_tidy hbound), ?_, by fun_prop⟩ - intro input - exact BitString.length_padWord (hsize input) + obtain ⟨bound, hbound, hsize⟩ := exists_normalizationBound hf.polyTime + exact ⟨OneWayNormalization.normalize f bound, fun n => 2 * bound n + 1, + hf.normalize bound hbound, fun input => BitString.length_padWord (hsize input), by fun_prop⟩ + +/-- Every nonuniform OWF yields a nonuniform OWF whose output length depends only on the input +length, with a uniformly polynomial-time output-length function. -/ +theorem NonuniformOneWay.exists_fixedOutputLength {f : List Bool → List Bool} + (hf : NonuniformOneWay f) : + ∃ (g : List Bool → List Bool) (length : ℕ → ℕ), NonuniformOneWay g ∧ + (∀ input, (g input).length = length input.length) ∧ + ComputableInPolyTime length encUnary encUnary := by + obtain ⟨bound, hbound, hsize⟩ := exists_normalizationBound hf.polyTime + exact ⟨OneWayNormalization.normalize f bound, fun n => 2 * bound n + 1, + hf.normalize bound hbound, fun input => BitString.length_padWord (hsize input), by fun_prop⟩ end Cslib.Crypto diff --git a/ComplexityTests/Crypto/Nonuniform.lean b/ComplexityTests/Crypto/Nonuniform.lean index 63ee3c5ed5..f818b494b6 100644 --- a/ComplexityTests/Crypto/Nonuniform.lean +++ b/ComplexityTests/Crypto/Nonuniform.lean @@ -21,6 +21,12 @@ open Cslib Cslib.Crypto example (word : List Bool) : ¬ NonuniformOneWay (fun _ => word) := fun h => not_oneWay_const word h.toOneWay +/-- Inverting a constant function is not hard even with empty advice: by +`oneWay_iff_inversionHardWithAdvice_nil` that would make it uniformly one-way. -/ +example (word : List Bool) : ¬ InversionHardWithAdvice (fun _ => word) (fun _ => []) := + fun h => not_oneWay_const word (oneWay_iff_inversionHardWithAdvice_nil.mpr + ⟨Turing.MultiTapeTM.ComputableInPolyTime.const word, h⟩) + /-- The nonuniform indistinguishability relation holds between equal ensembles. -/ example : NonuniformlyIndistinguishable (fun n => BitString.uniformList n) (fun n => BitString.uniformList n) :=