Cryptographic Boolean Functions in Lean

3.5. Propagation criteria🔗

Definition3.5.1
Group: Chapter 3: Boolean functions and cryptography (72)
Group member previews
Preview
Theorem 3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 4
Statement dependency previews
Preview
Theorem 1.7.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 13
Reverse dependency previews
Preview
Theorem 3.2.18
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-4propagation-criterionsacepcpages-58-59fidelity-exact

Propagation criteria (Carlet, pp. 58--59). A function f satisfies the propagation criterion with respect to E\subseteq V_n if D_af is balanced for every a\in E. It satisfies \mathrm{PC}(\ell) if \Delta_f(a)=0 \quad\text{whenever}\quad 0<w_H(a)\le\ell; \mathrm{SAC} is \mathrm{PC}(1). The order-k form requires every restriction obtained by fixing k coordinates to satisfy the criterion. Finally, \mathrm{EPC}(\ell) of order k requires every such nonzero D_af to be k-resilient; it implies the corresponding propagation criterion.

Lean code for Definition3.5.1●17 declarations
  • defdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    def CryptBoolean.lowWeightNonzeroDirections {n : ℕ} (l : ℕ) :
  Set (FABL.F₂Cube n)
    def CryptBoolean.lowWeightNonzeroDirections
  {n : ℕ} (l : ℕ) : Set (FABL.F₂Cube n)
    The nonzero directions of Hamming weight at most `l`.
  • defdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    def CryptBoolean.SatisfiesPropagationCriterionOn {n : ℕ}
  (E : Set (FABL.F₂Cube n)) (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.SatisfiesPropagationCriterionOn
  {n : ℕ} (E : Set (FABL.F₂Cube n))
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    Carlet's propagation criterion with respect to a set of directions.
  • defdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    def CryptBoolean.SatisfiesPropagationCriterion {n : ℕ} (l : ℕ)
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.SatisfiesPropagationCriterion
  {n : ℕ} (l : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    Carlet's propagation criterion `PC(l)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    theorem CryptBoolean.satisfiesPropagationCriterion_iff_on_lowWeightNonzeroDirections
  {n : ℕ} (l : ℕ) (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesPropagationCriterion l f ↔
    CryptBoolean.SatisfiesPropagationCriterionOn
      (CryptBoolean.lowWeightNonzeroDirections l) f
    theorem CryptBoolean.satisfiesPropagationCriterion_iff_on_lowWeightNonzeroDirections
  {n : ℕ} (l : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesPropagationCriterion
      l f ↔
    CryptBoolean.SatisfiesPropagationCriterionOn
      (CryptBoolean.lowWeightNonzeroDirections
        l)
      f
    `PC(l)` is propagation with respect to exactly the nonzero directions of weight at most
`l`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    theorem CryptBoolean.isBalanced_booleanDerivative_iff_autocorrelation_eq_zero
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) :
  CryptBoolean.IsBalanced (FABL.booleanDerivative f a) ↔
    CryptBoolean.autocorrelation f a = 0
    theorem CryptBoolean.isBalanced_booleanDerivative_iff_autocorrelation_eq_zero
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  CryptBoolean.IsBalanced
      (FABL.booleanDerivative f a) ↔
    CryptBoolean.autocorrelation f a = 0
    Balancedness of a directional derivative is equivalent to vanishing autocorrelation in
that direction.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    theorem CryptBoolean.satisfiesPropagationCriterion_iff_autocorrelation_eq_zero
  {n : ℕ} (l : ℕ) (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesPropagationCriterion l f ↔
    ∀ (a : FABL.F₂Cube n),
      a ≠ 0 →
        (FABL.f₂Support a).card ≤ l →
          CryptBoolean.autocorrelation f a = 0
    theorem CryptBoolean.satisfiesPropagationCriterion_iff_autocorrelation_eq_zero
  {n : ℕ} (l : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesPropagationCriterion
      l f ↔
    ∀ (a : FABL.F₂Cube n),
      a ≠ 0 →
        (FABL.f₂Support a).card ≤ l →
          CryptBoolean.autocorrelation f
              a =
            0
    Carlet's autocorrelation form of `PC(l)`.
  • defdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    def CryptBoolean.SatisfiesStrictAvalancheCriterion {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.SatisfiesStrictAvalancheCriterion
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    The strict avalanche criterion is `PC(1)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    theorem CryptBoolean.satisfiesStrictAvalancheCriterion_iff_pc_one {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesStrictAvalancheCriterion f ↔
    CryptBoolean.SatisfiesPropagationCriterion 1 f
    theorem CryptBoolean.satisfiesStrictAvalancheCriterion_iff_pc_one
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesStrictAvalancheCriterion
      f ↔
    CryptBoolean.SatisfiesPropagationCriterion
      1 f
    SAC is definitionally the first propagation criterion.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    theorem CryptBoolean.SatisfiesPropagationCriterion.mono {n l l' : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.SatisfiesPropagationCriterion l f)
  (hll' : l' ≤ l) : CryptBoolean.SatisfiesPropagationCriterion l' f
    theorem CryptBoolean.SatisfiesPropagationCriterion.mono
  {n l l' : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.SatisfiesPropagationCriterion
      l f)
  (hll' : l' ≤ l) :
  CryptBoolean.SatisfiesPropagationCriterion
    l' f
    Lowering the propagation parameter preserves the criterion.
  • defdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    def CryptBoolean.coordinateRestriction {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) : CryptBoolean.BooleanFunction J.card
    def CryptBoolean.coordinateRestriction {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) :
  CryptBoolean.BooleanFunction J.card
    A coordinate restriction, canonically reindexed by `Fin J.card`, built from FABL's
restriction and Boolean-encoding APIs.
  • defdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    def CryptBoolean.SatisfiesPropagationCriterionOfOrder {n : ℕ} (l k : ℕ)
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.SatisfiesPropagationCriterionOfOrder
  {n : ℕ} (l k : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    The order-`k` propagation criterion: every restriction fixing exactly `k`
coordinates satisfies `PC(l)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    theorem CryptBoolean.SatisfiesPropagationCriterionOfOrder.mono_order
  {n l k k' : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.SatisfiesPropagationCriterionOfOrder l k f)
  (hknl : k ≤ n - l) (hk'k : k' ≤ k) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l k' f
    theorem CryptBoolean.SatisfiesPropagationCriterionOfOrder.mono_order
  {n l k k' : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k f)
  (hknl : k ≤ n - l) (hk'k : k' ≤ k) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
    l k' f
    Carlet's order monotonicity: in the source range `k ≤ n - l`, order `k`
implies every lower restriction order.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    theorem CryptBoolean.SatisfiesPropagationCriterionOfOrder.mono_level
  {n l l' k : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.SatisfiesPropagationCriterionOfOrder l k f)
  (hl'l : l' ≤ l) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l' k f
    theorem CryptBoolean.SatisfiesPropagationCriterionOfOrder.mono_level
  {n l l' k : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k f)
  (hl'l : l' ≤ l) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
    l' k f
    Lowering the propagation parameter preserves every fixed-coordinate order.
  • defdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    def CryptBoolean.SatisfiesStrictAvalancheCriterionOfOrder {n : ℕ} (k : ℕ)
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.SatisfiesStrictAvalancheCriterionOfOrder
  {n : ℕ} (k : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    SAC of order `k` is `PC(1)` of order `k`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    theorem CryptBoolean.satisfiesStrictAvalancheCriterionOfOrder_iff_pc_one {n : ℕ}
  (k : ℕ) (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesStrictAvalancheCriterionOfOrder k f ↔
    CryptBoolean.SatisfiesPropagationCriterionOfOrder 1 k f
    theorem CryptBoolean.satisfiesStrictAvalancheCriterionOfOrder_iff_pc_one
  {n : ℕ} (k : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesStrictAvalancheCriterionOfOrder
      k f ↔
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      1 k f
    SAC of order `k` is exactly `PC(1)` of order `k`.
  • defdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    def CryptBoolean.SatisfiesExtendedPropagationCriterion {n : ℕ} (l k : ℕ)
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.SatisfiesExtendedPropagationCriterion
  {n : ℕ} (l k : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    The extended propagation criterion `EPC(l)` of order `k`: each derivative in a
nonzero direction of weight at most `l` is `k`-resilient.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean
    complete
    theorem CryptBoolean.SatisfiesExtendedPropagationCriterion.toPropagationCriterionOfOrder
  {n l k : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.SatisfiesExtendedPropagationCriterion l k f) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l k f
    theorem CryptBoolean.SatisfiesExtendedPropagationCriterion.toPropagationCriterionOfOrder
  {n l k : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.SatisfiesExtendedPropagationCriterion
      l k f) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
    l k f
    The extended criterion is stronger than the corresponding order-`k` propagation
criterion.