Cryptographic Boolean Functions in Lean

4.6. Functions with low univariate degree🔗

Theorem4.6.1
Group: Chapter 4: Classes with Provable Spectra and Weights (30)
Group member previews
Preview
Theorem 4.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1XL∃∀N
Tagscarletchapter-5additive-character-sumsweil-boundtheorem-7reference-245page-76source-open

Weil bound (Carlet, Theorem 7, p. 76). Let q be a prime power, let P\in\mathbb F_q[X] have degree d\ge1 with \gcd(d,q)=1, and let \chi be a nontrivial additive character of \mathbb F_q. Then \left|\sum_{x\in\mathbb F_q}\chi(P(x))\right| \le(d-1)\sqrt q.

The binary trace specialization fixes \chi as an additive character.

Theorem4.6.2
Group: Chapter 4: Classes with Provable Spectra and Weights (30)
Group member previews
Preview
Theorem 4.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.5.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-5trace-pairingcharacter-sumswalsh-transformnonlinearitypage-76fidelity-explicit-character-identification

Walsh coefficients as trace-character sums. Let \theta:V_n\simeq_{\mathbb F_2}\operatorname{GF}(2^n), let a\in\operatorname{GF}(2^n)^\times, and let P\in\operatorname{GF}(2^n)[X]. For u\in V_n, let b\in\operatorname{GF}(2^n) be the unique trace-pairing coefficient such that u\mathbin\cdot x=\operatorname{Tr}_n(b\theta(x))\qquad(x\in V_n), and W_{\operatorname{Tr}_n(aP\circ\theta)}(u) =\sum_{y\in\operatorname{GF}(2^n)} (-1)^{\operatorname{Tr}_n(a(P(y)+(b/a)y))}. Therefore, if the absolute value of the sum on the right is at most B for every linear perturbation P+cX, then \max_u|W_{\operatorname{Tr}_n(aP\circ\theta)}(u)|\le B \quad\text{and}\quad \operatorname{nl}(\operatorname{Tr}_n(aP\circ\theta)) \ge \frac{2^n-B}{2}.

Lean code for Theorem4.6.2●6 declarations
  • defdefined in CryptBoolean/Carlet/Chapter05/WeilNonlinearityReduction.lean
    complete
    def CryptBoolean.tracePolynomialBooleanFunction {n : ℕ}
  (theta : FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n)
  (P : Polynomial (CryptBoolean.BinaryGaloisField n)) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.tracePolynomialBooleanFunction
  {n : ℕ}
  (theta :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n)
  (P :
    Polynomial
      (CryptBoolean.BinaryGaloisField
        n)) :
  CryptBoolean.BooleanFunction n
    The Boolean function obtained by applying the binary absolute trace to a scaled polynomial.
  • defdefined in CryptBoolean/Carlet/Chapter05/WeilNonlinearityReduction.lean
    complete
    def CryptBoolean.tracePolynomialCharacterSum {n : ℕ}
  (a : CryptBoolean.BinaryGaloisField n)
  (P : Polynomial (CryptBoolean.BinaryGaloisField n)) : ℤ
    def CryptBoolean.tracePolynomialCharacterSum
  {n : ℕ}
  (a : CryptBoolean.BinaryGaloisField n)
  (P :
    Polynomial
      (CryptBoolean.BinaryGaloisField
        n)) :
  ℤ
    The unnormalized integer additive-character sum attached to a scaled finite-field polynomial.
  • theoremdefined in CryptBoolean/Carlet/Chapter05/WeilNonlinearityReduction.lean
    complete
    theorem CryptBoolean.exists_tracePolynomialCharacterSum_eq_walshTransform
  {n : ℕ}
  (theta : FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n) (ha : a ≠ 0)
  (P : Polynomial (CryptBoolean.BinaryGaloisField n))
  (u : FABL.F₂Cube n) :
  ∃ b,
    (∀ (x : FABL.F₂Cube n),
        FABL.f₂DotProduct u x =
          (CryptBoolean.absoluteTrace n) (b * theta x)) ∧
      CryptBoolean.walshTransform
          (CryptBoolean.tracePolynomialBooleanFunction theta a P) u =
        CryptBoolean.tracePolynomialCharacterSum a
          (P + Polynomial.C (b / a) * Polynomial.X)
    theorem CryptBoolean.exists_tracePolynomialCharacterSum_eq_walshTransform
  {n : ℕ}
  (theta :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n)
  (ha : a ≠ 0)
  (P :
    Polynomial
      (CryptBoolean.BinaryGaloisField n))
  (u : FABL.F₂Cube n) :
  ∃ b,
    (∀ (x : FABL.F₂Cube n),
        FABL.f₂DotProduct u x =
          (CryptBoolean.absoluteTrace n)
            (b * theta x)) ∧
      CryptBoolean.walshTransform
          (CryptBoolean.tracePolynomialBooleanFunction
            theta a P)
          u =
        CryptBoolean.tracePolynomialCharacterSum
          a
          (P +
            Polynomial.C (b / a) *
              Polynomial.X)
    A raw Walsh coefficient of a binary trace polynomial is a complete additive-character sum;
the Walsh linear term becomes `b / a` times `X`.
  • theoremdefined in CryptBoolean/Carlet/Chapter05/WeilNonlinearityReduction.lean
    complete
    theorem CryptBoolean.maxWalshMagnitude_tracePolynomialBooleanFunction_le {n : ℕ}
  (theta : FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n) (ha : a ≠ 0)
  (P : Polynomial (CryptBoolean.BinaryGaloisField n)) (B : ℝ)
  (hcharacter :
    ∀ (c : CryptBoolean.BinaryGaloisField n),
      |↑(CryptBoolean.tracePolynomialCharacterSum a
              (P + Polynomial.C c * Polynomial.X))| ≤
        B) :
  ↑(CryptBoolean.maxWalshMagnitude
        (CryptBoolean.tracePolynomialBooleanFunction theta a P)) ≤
    B
    theorem CryptBoolean.maxWalshMagnitude_tracePolynomialBooleanFunction_le
  {n : ℕ}
  (theta :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n)
  (ha : a ≠ 0)
  (P :
    Polynomial
      (CryptBoolean.BinaryGaloisField n))
  (B : ℝ)
  (hcharacter :
    ∀
      (c :
        CryptBoolean.BinaryGaloisField n),
      |↑(CryptBoolean.tracePolynomialCharacterSum
              a
              (P +
                Polynomial.C c *
                  Polynomial.X))| ≤
        B) :
  ↑(CryptBoolean.maxWalshMagnitude
        (CryptBoolean.tracePolynomialBooleanFunction
          theta a P)) ≤
    B
    A uniform bound for every linear perturbation of a finite-field polynomial bounds the maximum
raw Walsh magnitude of its binary trace function.
  • theoremdefined in CryptBoolean/Carlet/Chapter05/WeilNonlinearityReduction.lean
    complete
    theorem CryptBoolean.two_pow_le_two_mul_nonlinearity_add_of_tracePolynomialCharacterSum_le
  {n : ℕ}
  (theta : FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n) (ha : a ≠ 0)
  (P : Polynomial (CryptBoolean.BinaryGaloisField n)) (B : ℝ)
  (hcharacter :
    ∀ (c : CryptBoolean.BinaryGaloisField n),
      |↑(CryptBoolean.tracePolynomialCharacterSum a
              (P + Polynomial.C c * Polynomial.X))| ≤
        B) :
  2 ^ n ≤
    2 *
        ↑(CryptBoolean.nonlinearity
            (CryptBoolean.tracePolynomialBooleanFunction theta a P)) +
      B
    theorem CryptBoolean.two_pow_le_two_mul_nonlinearity_add_of_tracePolynomialCharacterSum_le
  {n : ℕ}
  (theta :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n)
  (ha : a ≠ 0)
  (P :
    Polynomial
      (CryptBoolean.BinaryGaloisField n))
  (B : ℝ)
  (hcharacter :
    ∀
      (c :
        CryptBoolean.BinaryGaloisField n),
      |↑(CryptBoolean.tracePolynomialCharacterSum
              a
              (P +
                Polynomial.C c *
                  Polynomial.X))| ≤
        B) :
  2 ^ n ≤
    2 *
        ↑(CryptBoolean.nonlinearity
            (CryptBoolean.tracePolynomialBooleanFunction
              theta a P)) +
      B
    Division-free nonlinearity lower bound obtained from a uniform complete character-sum bound.
  • theoremdefined in CryptBoolean/Carlet/Chapter05/WeilNonlinearityReduction.lean
    complete
    theorem CryptBoolean.tracePolynomialCharacterSum_nonlinearity_lower_bound
  {n : ℕ}
  (theta : FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n) (ha : a ≠ 0)
  (P : Polynomial (CryptBoolean.BinaryGaloisField n)) (B : ℝ)
  (hcharacter :
    ∀ (c : CryptBoolean.BinaryGaloisField n),
      |↑(CryptBoolean.tracePolynomialCharacterSum a
              (P + Polynomial.C c * Polynomial.X))| ≤
        B) :
  2 ^ n / 2 - B / 2 ≤
    ↑(CryptBoolean.nonlinearity
        (CryptBoolean.tracePolynomialBooleanFunction theta a P))
    theorem CryptBoolean.tracePolynomialCharacterSum_nonlinearity_lower_bound
  {n : ℕ}
  (theta :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (a : CryptBoolean.BinaryGaloisField n)
  (ha : a ≠ 0)
  (P :
    Polynomial
      (CryptBoolean.BinaryGaloisField n))
  (B : ℝ)
  (hcharacter :
    ∀
      (c :
        CryptBoolean.BinaryGaloisField n),
      |↑(CryptBoolean.tracePolynomialCharacterSum
              a
              (P +
                Polynomial.C c *
                  Polynomial.X))| ≤
        B) :
  2 ^ n / 2 - B / 2 ≤
    ↑(CryptBoolean.nonlinearity
        (CryptBoolean.tracePolynomialBooleanFunction
          theta a P))
    Real-valued half-factor form of the nonlinearity reduction.

The trace-pairing coefficient identifies every cube character with a unique finite-field trace character. The character-sum estimate is a hypothesis in this reduction; Theorem 7 supplies it for the stated polynomial degrees.

Corollary4.6.3
Group: Chapter 4: Classes with Provable Spectra and Weights (30)
Group member previews
Preview
Theorem 4.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 4.6.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0XL∃∀N
Tagscarletchapter-5weil-boundnonlinearitytracepage-76source-open

Binary Weil nonlinearity bound (Carlet, consequence of Theorem 7, p. 76). Let n>0, let P\in\operatorname{GF}(2^n)[X] have odd degree d>1, and let a\in\operatorname{GF}(2^n) be nonzero. For every \mathbb F_2-linear equivalence \theta:V_n\simeq\operatorname{GF}(2^n), define h_\theta(x)=\operatorname{Tr}_n\bigl(aP(\theta(x))\bigr). Then every Walsh coefficient of h_\theta has magnitude at most (d-1)\sqrt{2^n}, and \operatorname{nl}(h_\theta) \ge2^{n-1}-\frac{d-1}{2}\sqrt{2^n}.

Theorem4.6.4
Group: Chapter 4: Classes with Provable Spectra and Weights (30)
Group member previews
Preview
Theorem 4.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0XL∃∀N
Tagscarletchapter-5reciprocal-polynomialscharacter-sumskloosterman-sumsreferences-96-325page-76source-openfidelity-source-correction

Reciprocal-polynomial character-sum bound (Carlet, p. 76). Let n>0 and let P,Q\in\operatorname{GF}(2^n)[X] have odd degrees. Then \left| \sum_{x\in\operatorname{GF}(2^n)^\times} (-1)^{\operatorname{Tr}_n(P(x^{-1})+Q(x))} \right| \le(\deg P+\deg Q)\sqrt{2^n}. If \operatorname{inv}(0)=0 and \operatorname{inv}(x)=x^{-1} for x\ne0, then the whole-field convention satisfies \left| \sum_{x\in\operatorname{GF}(2^n)} (-1)^{\operatorname{Tr}_n(P(\operatorname{inv}(x))+Q(x))} \right| \le1+(\deg P+\deg Q)\sqrt{2^n}. For P(X)=X and Q(X)=aX, the punctured sums are the Kloosterman sums.

Carlet prints a one-sided inequality over the whole field after assigning \operatorname{inv}(0)=0. Theorem 1 of reference 325 states the sharp absolute-value bound over the nonzero Teichmuller units, which specialize here to \operatorname{GF}(2^n)^\times. The omitted summand has modulus one, so the displayed whole-field consequence requires the added 1.