Cryptographic Boolean Functions in Lean

9.5. Algebraic immunity🔗

Theorem9.5.1
Group: Chapter 9: Symmetric and rotation-symmetric functions (22)
Group member previews
Preview
Definition 9.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 3.7.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-10symmetric-functionsalgebraic-immunitymajority-functionsclassificationodd-dimensionreference-242reference-300page-146fidelity-exact

Optimal algebraic immunity in odd dimension (Carlet, p. 146). Let n>0 be odd and define the majority function \operatorname{Maj}_n by \operatorname{Maj}_n(x)=1 \quad\Longleftrightarrow\quad w_H(x)>\frac n2. For every symmetric Boolean function f:V_n\to\mathbb F_2, \operatorname{AI}(f)=\frac{n+1}{2} if and only if f=\operatorname{Maj}_n \quad\text{or}\quad f=\operatorname{Maj}_n+1. Thus, up to addition of a constant, majority is the unique symmetric function of optimal algebraic immunity in odd dimension.

Lean code for Theorem9.5.1●15 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.isSymmetricBooleanFunction_carletStrictMajority {n : ℕ} :
  CryptBoolean.IsSymmetricBooleanFunction
    (CryptBoolean.carletStrictMajority n)
    theorem CryptBoolean.isSymmetricBooleanFunction_carletStrictMajority
  {n : ℕ} :
  CryptBoolean.IsSymmetricBooleanFunction
    (CryptBoolean.carletStrictMajority n)
    Strict majority is a symmetric Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.IsSymmetricBooleanFunction.add_constant_one {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  CryptBoolean.IsSymmetricBooleanFunction (f + 1)
    theorem CryptBoolean.IsSymmetricBooleanFunction.add_constant_one
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.IsSymmetricBooleanFunction
    (f + 1)
    Output complementation preserves symmetry.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.isSymmetricBooleanFunction_carletStrictMajority_add_one
  {n : ℕ} :
  CryptBoolean.IsSymmetricBooleanFunction
    (CryptBoolean.carletStrictMajority n + 1)
    theorem CryptBoolean.isSymmetricBooleanFunction_carletStrictMajority_add_one
  {n : ℕ} :
  CryptBoolean.IsSymmetricBooleanFunction
    (CryptBoolean.carletStrictMajority n +
      1)
    The complement of strict majority is symmetric.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.symmetricWeightProfile_carletStrictMajority_eq_one_iff
  {n : ℕ} (r : Fin (n + 1)) :
  CryptBoolean.symmetricWeightProfile
        (CryptBoolean.carletStrictMajority n) r =
      1 ↔
    n < 2 * ↑r
    theorem CryptBoolean.symmetricWeightProfile_carletStrictMajority_eq_one_iff
  {n : ℕ} (r : Fin (n + 1)) :
  CryptBoolean.symmetricWeightProfile
        (CryptBoolean.carletStrictMajority
          n)
        r =
      1 ↔
    n < 2 * ↑r
    The strict-majority weight profile is the strict upper-half threshold.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.symmetricWeightProfile_carletStrictMajority_add_one_eq_one_iff
  {n : ℕ} (r : Fin (n + 1)) :
  CryptBoolean.symmetricWeightProfile
        (CryptBoolean.carletStrictMajority n + 1) r =
      1 ↔
    2 * ↑r ≤ n
    theorem CryptBoolean.symmetricWeightProfile_carletStrictMajority_add_one_eq_one_iff
  {n : ℕ} (r : Fin (n + 1)) :
  CryptBoolean.symmetricWeightProfile
        (CryptBoolean.carletStrictMajority
            n +
          1)
        r =
      1 ↔
    2 * ↑r ≤ n
    The complemented strict-majority profile is the weak lower-half
threshold.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.eq_carletStrictMajority_of_symmetricWeightProfile {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hprofile :
    ∀ (r : Fin (n + 1)),
      CryptBoolean.symmetricWeightProfile f r = 1 ↔ n < 2 * ↑r) :
  f = CryptBoolean.carletStrictMajority n
    theorem CryptBoolean.eq_carletStrictMajority_of_symmetricWeightProfile
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hprofile :
    ∀ (r : Fin (n + 1)),
      CryptBoolean.symmetricWeightProfile
            f r =
          1 ↔
        n < 2 * ↑r) :
  f = CryptBoolean.carletStrictMajority n
    A symmetric function with the strict upper-half profile is strict
majority.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.eq_carletStrictMajority_add_one_of_symmetricWeightProfile
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hprofile :
    ∀ (r : Fin (n + 1)),
      CryptBoolean.symmetricWeightProfile f r = 1 ↔ 2 * ↑r ≤ n) :
  f = CryptBoolean.carletStrictMajority n + 1
    theorem CryptBoolean.eq_carletStrictMajority_add_one_of_symmetricWeightProfile
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hprofile :
    ∀ (r : Fin (n + 1)),
      CryptBoolean.symmetricWeightProfile
            f r =
          1 ↔
        2 * ↑r ≤ n) :
  f =
    CryptBoolean.carletStrictMajority n +
      1
    A symmetric function with the weak lower-half profile is the complement
of strict majority.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.eq_carletStrictMajority_or_add_one_iff_weightProfile
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  f = CryptBoolean.carletStrictMajority n ∨
      f = CryptBoolean.carletStrictMajority n + 1 ↔
    (∀ (r : Fin (n + 1)),
        CryptBoolean.symmetricWeightProfile f r = 1 ↔ n < 2 * ↑r) ∨
      ∀ (r : Fin (n + 1)),
        CryptBoolean.symmetricWeightProfile f r = 1 ↔ 2 * ↑r ≤ n
    theorem CryptBoolean.eq_carletStrictMajority_or_add_one_iff_weightProfile
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  f =
        CryptBoolean.carletStrictMajority
          n ∨
      f =
        CryptBoolean.carletStrictMajority
            n +
          1 ↔
    (∀ (r : Fin (n + 1)),
        CryptBoolean.symmetricWeightProfile
              f r =
            1 ↔
          n < 2 * ↑r) ∨
      ∀ (r : Fin (n + 1)),
        CryptBoolean.symmetricWeightProfile
              f r =
            1 ↔
          2 * ↑r ≤ n
    For a symmetric function, being strict majority up to complementation is
equivalent to having one of the two half-threshold profiles.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.algebraicImmunity_carletStrictMajority_add_one {n : ℕ} :
  CryptBoolean.algebraicImmunity
      (CryptBoolean.carletStrictMajority n + 1) =
    (n + 1) / 2
    theorem CryptBoolean.algebraicImmunity_carletStrictMajority_add_one
  {n : ℕ} :
  CryptBoolean.algebraicImmunity
      (CryptBoolean.carletStrictMajority
          n +
        1) =
    (n + 1) / 2
    The complement of strict majority has optimal algebraic immunity.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.symmetric_optimalAlgebraicImmunity_of_eq_carletStrictMajority_or_add_one
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf :
    f = CryptBoolean.carletStrictMajority n ∨
      f = CryptBoolean.carletStrictMajority n + 1) :
  CryptBoolean.IsSymmetricBooleanFunction f ∧
    CryptBoolean.algebraicImmunity f = (n + 1) / 2
    theorem CryptBoolean.symmetric_optimalAlgebraicImmunity_of_eq_carletStrictMajority_or_add_one
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    f =
        CryptBoolean.carletStrictMajority
          n ∨
      f =
        CryptBoolean.carletStrictMajority
            n +
          1) :
  CryptBoolean.IsSymmetricBooleanFunction
      f ∧
    CryptBoolean.algebraicImmunity f =
      (n + 1) / 2
    Strict majority and its complement are symmetric functions of optimal
algebraic immunity.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.annihilatorEvaluationLinearMap_injective_of_lt_algebraicImmunity
  {n d : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hd : d < CryptBoolean.algebraicImmunity f) :
  Function.Injective ⇑(CryptBoolean.annihilatorEvaluationLinearMap f d)
    theorem CryptBoolean.annihilatorEvaluationLinearMap_injective_of_lt_algebraicImmunity
  {n d : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hd :
    d <
      CryptBoolean.algebraicImmunity f) :
  Function.Injective
    ⇑(CryptBoolean.annihilatorEvaluationLinearMap
        f d)
    Evaluation of degree-at-most-`d` functions on the support is injective
whenever `d` is strictly below the algebraic immunity.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.annihilatorEvaluationLinearMap_injective_pair_of_odd_optimal
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hn : Odd n)
  (hAI : CryptBoolean.algebraicImmunity f = (n + 1) / 2) :
  Function.Injective
      ⇑(CryptBoolean.annihilatorEvaluationLinearMap f ((n - 1) / 2)) ∧
    Function.Injective
      ⇑(CryptBoolean.annihilatorEvaluationLinearMap (f + 1)
          ((n - 1) / 2))
    theorem CryptBoolean.annihilatorEvaluationLinearMap_injective_pair_of_odd_optimal
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : Odd n)
  (hAI :
    CryptBoolean.algebraicImmunity f =
      (n + 1) / 2) :
  Function.Injective
      ⇑(CryptBoolean.annihilatorEvaluationLinearMap
          f ((n - 1) / 2)) ∧
    Function.Injective
      ⇑(CryptBoolean.annihilatorEvaluationLinearMap
          (f + 1) ((n - 1) / 2))
    In odd dimension, optimal algebraic immunity makes both half-order
annihilator-evaluation maps injective.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.balanced_and_annihilatorEvaluation_injective_of_odd_optimal
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hn : Odd n)
  (hAI : CryptBoolean.algebraicImmunity f = (n + 1) / 2) :
  CryptBoolean.IsBalanced f ∧
    Function.Injective
        ⇑(CryptBoolean.annihilatorEvaluationLinearMap f ((n - 1) / 2)) ∧
      Function.Injective
        ⇑(CryptBoolean.annihilatorEvaluationLinearMap (f + 1)
            ((n - 1) / 2))
    theorem CryptBoolean.balanced_and_annihilatorEvaluation_injective_of_odd_optimal
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : Odd n)
  (hAI :
    CryptBoolean.algebraicImmunity f =
      (n + 1) / 2) :
  CryptBoolean.IsBalanced f ∧
    Function.Injective
        ⇑(CryptBoolean.annihilatorEvaluationLinearMap
            f ((n - 1) / 2)) ∧
      Function.Injective
        ⇑(CryptBoolean.annihilatorEvaluationLinearMap
            (f + 1) ((n - 1) / 2))
    An odd-dimensional function of optimal algebraic immunity is balanced,
and its support and complementary support both determine every Boolean
function of degree at most `(n-1)/2`.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.exists_symmetricWeightProfileNat_half_threshold_of_odd_optimal
  {n : ℕ} {f : CryptBoolean.BooleanFunction n} (hn : Odd n)
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hAI : CryptBoolean.algebraicImmunity f = (n + 1) / 2) :
  ∃ a,
    ∀ r ≤ n,
      CryptBoolean.symmetricWeightProfileNat f r =
        if 2 * r ≤ n then a else a + 1
    theorem CryptBoolean.exists_symmetricWeightProfileNat_half_threshold_of_odd_optimal
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hn : Odd n)
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hAI :
    CryptBoolean.algebraicImmunity f =
      (n + 1) / 2) :
  ∃ a,
    ∀ r ≤ n,
      CryptBoolean.symmetricWeightProfileNat
          f r =
        if 2 * r ≤ n then a else a + 1
    An odd-dimensional symmetric function of optimal algebraic immunity has
one constant profile value on the lower half of the weight layers and its
complementary value on the upper half.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean
    complete
    theorem CryptBoolean.symmetric_optimalAlgebraicImmunity_iff_eq_carletStrictMajority_or_add_one
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (_hnpos : 0 < n)
  (hn : Odd n) (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  CryptBoolean.algebraicImmunity f = (n + 1) / 2 ↔
    f = CryptBoolean.carletStrictMajority n ∨
      f = CryptBoolean.carletStrictMajority n + 1
    theorem CryptBoolean.symmetric_optimalAlgebraicImmunity_iff_eq_carletStrictMajority_or_add_one
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (_hnpos : 0 < n) (hn : Odd n)
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.algebraicImmunity f =
      (n + 1) / 2 ↔
    f =
        CryptBoolean.carletStrictMajority
          n ∨
      f =
        CryptBoolean.carletStrictMajority
            n +
          1
    For positive odd dimension, a symmetric Boolean function has optimal
algebraic immunity exactly when it is strict majority or its output
complement.