5.5. Primary constructions of bent functions🔗

Theorem5.5.1

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Theorem 4.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 8

Reverse dependency previews

Preview

Proposition 5.5.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagscarletchapter-6maiorana-mcfarlandrelation-48pages-83-84fidelity-exact

Maiorana--McFarland construction (Carlet, Relation (48), pp. 83--84). For x,y\in V_m, let f(x,y)=x\mathbin\cdot\pi(y)+g(y), where g:V_m\to\mathbb F_2 is arbitrary. The function f is bent if and only if \pi:V_m\to V_m is bijective. In that case \widetilde f(a,b)=b\mathbin\cdot\pi^{-1}(a)+g(\pi^{-1}(a)).

Lean code for Theorem5.5.1●8 declarations

defdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarland.lean

complete

def CryptBoolean.booleanMaioranaMcFarlandPermutation {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (m + m)

def CryptBoolean.booleanMaioranaMcFarlandPermutation
  {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (m + m)

The Boolean-valued original Maiorana--McFarland function associated to a
permutation and an arbitrary Boolean offset.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarland.lean

complete

theorem CryptBoolean.booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks
  {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m) (x y : FABL.F₂Cube m) :
  CryptBoolean.booleanMaioranaMcFarlandPermutation π g
      (FABL.joinF₂CubeBlocks x y) =
    FABL.f₂DotProduct x (π y) + g y

theorem CryptBoolean.booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks
  {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m)
  (x y : FABL.F₂Cube m) :
  CryptBoolean.booleanMaioranaMcFarlandPermutation
      π g (FABL.joinF₂CubeBlocks x y) =
    FABL.f₂DotProduct x (π y) + g y

Evaluation of the Boolean Maiorana--McFarland function on its two
coordinate blocks.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarland.lean

complete

theorem CryptBoolean.isMaioranaMcFarland_of_eq_permutation {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + n))
  (g : CryptBoolean.BooleanFunction n) (π : Equiv.Perm (FABL.F₂Cube n))
  (hf :
    ∀ (x y : FABL.F₂Cube n),
      f (FABL.joinF₂CubeBlocks x y) = FABL.f₂DotProduct x (π y) + g y) :
  CryptBoolean.IsMaioranaMcFarland f

theorem CryptBoolean.isMaioranaMcFarland_of_eq_permutation
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + n))
  (g : CryptBoolean.BooleanFunction n)
  (π : Equiv.Perm (FABL.F₂Cube n))
  (hf :
    ∀ (x y : FABL.F₂Cube n),
      f (FABL.joinF₂CubeBlocks x y) =
        FABL.f₂DotProduct x (π y) + g y) :
  CryptBoolean.IsMaioranaMcFarland f

The original permutation construction belongs to the Maiorana--McFarland
class introduced in Chapter 5.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarland.lean

complete

theorem CryptBoolean.walshTransform_maioranaMcFarlandPermutation {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + n))
  (g : CryptBoolean.BooleanFunction n) (π : Equiv.Perm (FABL.F₂Cube n))
  (hf :
    ∀ (x y : FABL.F₂Cube n),
      f (FABL.joinF₂CubeBlocks x y) = FABL.f₂DotProduct x (π y) + g y)
  (a b : FABL.F₂Cube n) :
  CryptBoolean.walshTransform f (FABL.joinF₂CubeBlocks a b) =
    CryptBoolean.bitSignInt
        (g ((Equiv.symm π) a) +
          FABL.f₂DotProduct b ((Equiv.symm π) a)) *
      2 ^ n

theorem CryptBoolean.walshTransform_maioranaMcFarlandPermutation
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + n))
  (g : CryptBoolean.BooleanFunction n)
  (π : Equiv.Perm (FABL.F₂Cube n))
  (hf :
    ∀ (x y : FABL.F₂Cube n),
      f (FABL.joinF₂CubeBlocks x y) =
        FABL.f₂DotProduct x (π y) + g y)
  (a b : FABL.F₂Cube n) :
  CryptBoolean.walshTransform f
      (FABL.joinF₂CubeBlocks a b) =
    CryptBoolean.bitSignInt
        (g ((Equiv.symm π) a) +
          FABL.f₂DotProduct b
            ((Equiv.symm π) a)) *
      2 ^ n

Carlet relation (48): the exact raw Walsh transform of the original
Maiorana--McFarland construction.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarland.lean

complete

theorem CryptBoolean.isBent_of_maioranaMcFarlandPermutation {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + n))
  (g : CryptBoolean.BooleanFunction n) (π : Equiv.Perm (FABL.F₂Cube n))
  (hf :
    ∀ (x y : FABL.F₂Cube n),
      f (FABL.joinF₂CubeBlocks x y) = FABL.f₂DotProduct x (π y) + g y) :
  CryptBoolean.IsBent f

theorem CryptBoolean.isBent_of_maioranaMcFarlandPermutation
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + n))
  (g : CryptBoolean.BooleanFunction n)
  (π : Equiv.Perm (FABL.F₂Cube n))
  (hf :
    ∀ (x y : FABL.F₂Cube n),
      f (FABL.joinF₂CubeBlocks x y) =
        FABL.f₂DotProduct x (π y) + g y) :
  CryptBoolean.IsBent f

Every Boolean function satisfying Carlet relation (48) is bent.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarland.lean

complete

theorem CryptBoolean.isBent_booleanMaioranaMcFarlandPermutation {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.IsBent
    (CryptBoolean.booleanMaioranaMcFarlandPermutation π g)

theorem CryptBoolean.isBent_booleanMaioranaMcFarlandPermutation
  {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.IsBent
    (CryptBoolean.booleanMaioranaMcFarlandPermutation
      π g)

Every Boolean-valued original Maiorana--McFarland function is bent.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarland.lean

complete

theorem CryptBoolean.bentDual_maioranaMcFarlandPermutation {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + n))
  (g : CryptBoolean.BooleanFunction n) (π : Equiv.Perm (FABL.F₂Cube n))
  (hf :
    ∀ (x y : FABL.F₂Cube n),
      f (FABL.joinF₂CubeBlocks x y) = FABL.f₂DotProduct x (π y) + g y)
  (a b : FABL.F₂Cube n) :
  CryptBoolean.bentDual f (FABL.joinF₂CubeBlocks a b) =
    FABL.f₂DotProduct b ((Equiv.symm π) a) + g ((Equiv.symm π) a)

theorem CryptBoolean.bentDual_maioranaMcFarlandPermutation
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + n))
  (g : CryptBoolean.BooleanFunction n)
  (π : Equiv.Perm (FABL.F₂Cube n))
  (hf :
    ∀ (x y : FABL.F₂Cube n),
      f (FABL.joinF₂CubeBlocks x y) =
        FABL.f₂DotProduct x (π y) + g y)
  (a b : FABL.F₂Cube n) :
  CryptBoolean.bentDual f
      (FABL.joinF₂CubeBlocks a b) =
    FABL.f₂DotProduct b
        ((Equiv.symm π) a) +
      g ((Equiv.symm π) a)

The dual of the original Maiorana--McFarland construction is obtained by
applying the inverse permutation to the first frequency block.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandGeneral.lean

complete

theorem CryptBoolean.isBent_iff_bijective_maioranaMcFarland {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + n))
  (φ : FABL.F₂Cube n → FABL.F₂Cube n)
  (g : CryptBoolean.BooleanFunction n)
  (hf :
    ∀ (x y : Fin n → FABL.𝔽₂),
      f (Fin.append x y) = FABL.f₂DotProduct x (φ y) + g y) :
  CryptBoolean.IsBent f ↔ Function.Bijective φ

theorem CryptBoolean.isBent_iff_bijective_maioranaMcFarland
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + n))
  (φ : FABL.F₂Cube n → FABL.F₂Cube n)
  (g : CryptBoolean.BooleanFunction n)
  (hf :
    ∀ (x y : Fin n → FABL.𝔽₂),
      f (Fin.append x y) =
        FABL.f₂DotProduct x (φ y) + g y) :
  CryptBoolean.IsBent f ↔
    Function.Bijective φ

For equal coordinate blocks, bijectivity of the frequency map is both
necessary and sufficient for the Maiorana--McFarland function to be bent.

Proposition5.5.2

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Corollary 4.4.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 5.5.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagscarletchapter-6proposition-20relation-49pages-84-85fidelity-exact

Proposition 20 (Carlet, Relation (49), pp. 84--85). Let n=r+s be even with r\le s, let \varphi:V_s\to V_r, and put f_{\varphi,g}(x,y)=x\mathbin\cdot\varphi(y)+g(y). For every a\in V_r and b\in V_s, W_{f_{\varphi,g}}(a,b) =2^r\sum_{y\in\varphi^{-1}(a)}(-1)^{g(y)+b\mathbin\cdot y}. If every fiber \varphi^{-1}(a) is an affine subspace of dimension s-r and, when r<s, the restriction of g to every fiber is bent, then f_{\varphi,g} is bent.

Lean code for Proposition5.5.2●4 declarations

defdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandGeneral.lean

complete

def CryptBoolean.maioranaMcFarlandFiberCharacterSum {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) : ℤ

def CryptBoolean.maioranaMcFarlandFiberCharacterSum
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) : ℤ

The signed character sum over a fiber in the general
Maiorana--McFarland construction.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandGeneral.lean

complete

theorem CryptBoolean.walshTransform_maioranaMcFarlandGeneral {r s : ℕ}
  (f : CryptBoolean.BooleanFunction (r + s))
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hf :
    ∀ (x : Fin r → FABL.𝔽₂) (y : Fin s → FABL.𝔽₂),
      f (Fin.append x y) = FABL.f₂DotProduct x (φ y) + g y)
  (a : FABL.F₂Cube r) (b : FABL.F₂Cube s) :
  CryptBoolean.walshTransform f (Fin.append a b) =
    2 ^ r * CryptBoolean.maioranaMcFarlandFiberCharacterSum φ g a b

theorem CryptBoolean.walshTransform_maioranaMcFarlandGeneral
  {r s : ℕ}
  (f :
    CryptBoolean.BooleanFunction (r + s))
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hf :
    ∀ (x : Fin r → FABL.𝔽₂)
      (y : Fin s → FABL.𝔽₂),
      f (Fin.append x y) =
        FABL.f₂DotProduct x (φ y) + g y)
  (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  CryptBoolean.walshTransform f
      (Fin.append a b) =
    2 ^ r *
      CryptBoolean.maioranaMcFarlandFiberCharacterSum
        φ g a b

Carlet relation (49): the raw Walsh coefficient of a general
Maiorana--McFarland function is the corresponding fiber character sum
multiplied by the size of the first coordinate block.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandGeneral.lean

complete

theorem CryptBoolean.isBent_iff_maioranaMcFarlandFiberCharacterSum_natAbs
  {r s : ℕ} (f : CryptBoolean.BooleanFunction (r + s))
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hf :
    ∀ (x : Fin r → FABL.𝔽₂) (y : Fin s → FABL.𝔽₂),
      f (Fin.append x y) = FABL.f₂DotProduct x (φ y) + g y)
  (_heven : Even (r + s)) :
  CryptBoolean.IsBent f ↔
    r ≤ (r + s) / 2 ∧
      ∀ (a : FABL.F₂Cube r) (b : FABL.F₂Cube s),
        (CryptBoolean.maioranaMcFarlandFiberCharacterSum φ g a
              b).natAbs =
          2 ^ ((r + s) / 2 - r)

theorem CryptBoolean.isBent_iff_maioranaMcFarlandFiberCharacterSum_natAbs
  {r s : ℕ}
  (f :
    CryptBoolean.BooleanFunction (r + s))
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hf :
    ∀ (x : Fin r → FABL.𝔽₂)
      (y : Fin s → FABL.𝔽₂),
      f (Fin.append x y) =
        FABL.f₂DotProduct x (φ y) + g y)
  (_heven : Even (r + s)) :
  CryptBoolean.IsBent f ↔
    r ≤ (r + s) / 2 ∧
      ∀ (a : FABL.F₂Cube r)
        (b : FABL.F₂Cube s),
        (CryptBoolean.maioranaMcFarlandFiberCharacterSum
              φ g a b).natAbs =
          2 ^ ((r + s) / 2 - r)

Under the source's even-dimension hypothesis, a general
Maiorana--McFarland function is bent exactly when the first block fits within
half the dimension and every fiber character sum has the stated magnitude.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandGeneral.lean

complete

theorem CryptBoolean.isBent_maioranaMcFarlandGeneral_of_affineFibers {r s : ℕ}
  (f : CryptBoolean.BooleanFunction (r + s))
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hf :
    ∀ (x : Fin r → FABL.𝔽₂) (y : Fin s → FABL.𝔽₂),
      f (Fin.append x y) = FABL.f₂DotProduct x (φ y) + g y)
  (hrle : r ≤ s) (heven : Even (r + s))
  (E : FABL.F₂Cube r → Submodule FABL.𝔽₂ (FABL.F₂Cube s))
  (z : FABL.F₂Cube r → FABL.F₂Cube s)
  (e : (a : FABL.F₂Cube r) → FABL.F₂Cube (s - r) ≃ₗ[FABL.𝔽₂] ↥(E a))
  (hfiber :
    ∀ (a : FABL.F₂Cube r) (y : FABL.F₂Cube s),
      φ y = a ↔ ∃ x, y = ↑((e a) x) + z a)
  (hbent :
    r < s →
      ∀ (a : FABL.F₂Cube r),
        CryptBoolean.IsBent
          (CryptBoolean.coordinateAffineSubspaceRestriction g (E a)
            (z a) (e a))) :
  CryptBoolean.IsBent f

theorem CryptBoolean.isBent_maioranaMcFarlandGeneral_of_affineFibers
  {r s : ℕ}
  (f :
    CryptBoolean.BooleanFunction (r + s))
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hf :
    ∀ (x : Fin r → FABL.𝔽₂)
      (y : Fin s → FABL.𝔽₂),
      f (Fin.append x y) =
        FABL.f₂DotProduct x (φ y) + g y)
  (hrle : r ≤ s) (heven : Even (r + s))
  (E :
    FABL.F₂Cube r →
      Submodule FABL.𝔽₂ (FABL.F₂Cube s))
  (z : FABL.F₂Cube r → FABL.F₂Cube s)
  (e :
    (a : FABL.F₂Cube r) →
      FABL.F₂Cube (s - r) ≃ₗ[FABL.𝔽₂]
        ↥(E a))
  (hfiber :
    ∀ (a : FABL.F₂Cube r)
      (y : FABL.F₂Cube s),
      φ y = a ↔ ∃ x, y = ↑((e a) x) + z a)
  (hbent :
    r < s →
      ∀ (a : FABL.F₂Cube r),
        CryptBoolean.IsBent
          (CryptBoolean.coordinateAffineSubspaceRestriction
            g (E a) (z a) (e a))) :
  CryptBoolean.IsBent f

Carlet Proposition 20: if the fibers of `φ` are affine subspaces of
dimension `s - r` and the restrictions of `g` to the positive-dimensional
fibers are bent, then the associated general Maiorana--McFarland function is
bent.

Theorem5.5.3

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

Tagscarletchapter-6page-85fidelity-exact

Balance of the Maiorana--McFarland frequency map (Carlet, p. 85). Let n=r+s be even. If f_{\varphi,g}(x,y)=x\mathbin\cdot\varphi(y)+g(y) is bent on V_r\times V_s, then r\le s and \varphi:V_s\to V_r is uniformly distributed. Explicitly, |\varphi^{-1}(a)|=2^{s-r} \qquad(a\in V_r).

Lean code for Theorem5.5.3●2 declarations

defdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBalance.lean

complete

def CryptBoolean.IsBalancedCubeMap {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) : Prop

def CryptBoolean.IsBalancedCubeMap {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) :
  Prop

A map between binary cubes is balanced when all output fibers have the
cardinality forced by the two cube dimensions.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBalance.lean

complete

theorem CryptBoolean.isBalancedCubeMap_of_isBent_maioranaMcFarlandGeneral
  {r s : ℕ} (f : CryptBoolean.BooleanFunction (r + s))
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hf :
    ∀ (x : Fin r → FABL.𝔽₂) (y : Fin s → FABL.𝔽₂),
      f (Fin.append x y) = FABL.f₂DotProduct x (φ y) + g y)
  (heven : Even (r + s)) (hbent : CryptBoolean.IsBent f) :
  CryptBoolean.IsBalancedCubeMap φ

theorem CryptBoolean.isBalancedCubeMap_of_isBent_maioranaMcFarlandGeneral
  {r s : ℕ}
  (f :
    CryptBoolean.BooleanFunction (r + s))
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hf :
    ∀ (x : Fin r → FABL.𝔽₂)
      (y : Fin s → FABL.𝔽₂),
      f (Fin.append x y) =
        FABL.f₂DotProduct x (φ y) + g y)
  (heven : Even (r + s))
  (hbent : CryptBoolean.IsBent f) :
  CryptBoolean.IsBalancedCubeMap φ

If a general Maiorana--McFarland representation is bent, then its
frequency map is uniformly distributed over the output cube.

Theorem5.5.4

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

Tagscarletchapter-6page-86fidelity-exact

Half-dimensional linear spaces of bent functions (Carlet, p. 86). For every m>0, there is an m-dimensional \mathbb F_2-linear subspace B of the Boolean functions on V_{2m} such that f\in B\setminus\{0\}\quad\Longrightarrow\quad f\text{ is bent}.

Lean code for Theorem5.5.4●12 declarations

defdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean

complete

def CryptBoolean.binaryGaloisFieldCoordinateEquiv (m : ℕ) (hm : 0 < m) :
  FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m

def CryptBoolean.binaryGaloisFieldCoordinateEquiv
  (m : ℕ) (hm : 0 < m) :
  FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
    CryptBoolean.BinaryGaloisField m

Binary coordinates on a positive-dimensional binary Galois field.

defdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean

complete

def CryptBoolean.fieldMultiplicationCubeMap {m : ℕ}
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m)
  (a : CryptBoolean.BinaryGaloisField m) : FABL.F₂Cube m → FABL.F₂Cube m

def CryptBoolean.fieldMultiplicationCubeMap
  {m : ℕ}
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m)
  (a : CryptBoolean.BinaryGaloisField m) :
  FABL.F₂Cube m → FABL.F₂Cube m

Multiplication by a field element, transported to binary cube
coordinates.

defdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean

complete

def CryptBoolean.fieldMaioranaMcFarlandFunction {m : ℕ}
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m)
  (a : CryptBoolean.BinaryGaloisField m) :
  CryptBoolean.BooleanFunction (m + m)

def CryptBoolean.fieldMaioranaMcFarlandFunction
  {m : ℕ}
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m)
  (a : CryptBoolean.BinaryGaloisField m) :
  CryptBoolean.BooleanFunction (m + m)

The Maiorana--McFarland function indexed linearly by a field element.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean

complete

theorem CryptBoolean.fieldMaioranaMcFarlandFunction_joinF₂CubeBlocks {m : ℕ}
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m)
  (a : CryptBoolean.BinaryGaloisField m) (x y : FABL.F₂Cube m) :
  CryptBoolean.fieldMaioranaMcFarlandFunction theta a
      (FABL.joinF₂CubeBlocks x y) =
    FABL.f₂DotProduct x
      (CryptBoolean.fieldMultiplicationCubeMap theta a y)

theorem CryptBoolean.fieldMaioranaMcFarlandFunction_joinF₂CubeBlocks
  {m : ℕ}
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m)
  (a : CryptBoolean.BinaryGaloisField m)
  (x y : FABL.F₂Cube m) :
  CryptBoolean.fieldMaioranaMcFarlandFunction
      theta a
      (FABL.joinF₂CubeBlocks x y) =
    FABL.f₂DotProduct x
      (CryptBoolean.fieldMultiplicationCubeMap
        theta a y)

defdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean

complete

def CryptBoolean.fieldMaioranaMcFarlandLinearMap {m : ℕ}
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m) :
  CryptBoolean.BinaryGaloisField m →ₗ[FABL.𝔽₂]
    CryptBoolean.BooleanFunction (m + m)

def CryptBoolean.fieldMaioranaMcFarlandLinearMap
  {m : ℕ}
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m) :
  CryptBoolean.BinaryGaloisField
      m →ₗ[FABL.𝔽₂]
    CryptBoolean.BooleanFunction (m + m)

The field-indexed Maiorana--McFarland family depends linearly on its
field parameter.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean

complete

theorem CryptBoolean.fieldMultiplicationCubeMap_bijective {m : ℕ}
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m)
  (a : CryptBoolean.BinaryGaloisField m) (ha : a ≠ 0) :
  Function.Bijective (CryptBoolean.fieldMultiplicationCubeMap theta a)

theorem CryptBoolean.fieldMultiplicationCubeMap_bijective
  {m : ℕ}
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m)
  (a : CryptBoolean.BinaryGaloisField m)
  (ha : a ≠ 0) :
  Function.Bijective
    (CryptBoolean.fieldMultiplicationCubeMap
      theta a)

Multiplication by a nonzero field parameter is a permutation of the
binary coordinate cube.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean

complete

theorem CryptBoolean.isBent_fieldMaioranaMcFarlandFunction {m : ℕ}
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m)
  (a : CryptBoolean.BinaryGaloisField m) (ha : a ≠ 0) :
  CryptBoolean.IsBent
    (CryptBoolean.fieldMaioranaMcFarlandFunction theta a)

theorem CryptBoolean.isBent_fieldMaioranaMcFarlandFunction
  {m : ℕ}
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m)
  (a : CryptBoolean.BinaryGaloisField m)
  (ha : a ≠ 0) :
  CryptBoolean.IsBent
    (CryptBoolean.fieldMaioranaMcFarlandFunction
      theta a)

Every nonzero member of the field-indexed family is bent.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean

complete

theorem CryptBoolean.fieldMaioranaMcFarlandLinearMap_injective {m : ℕ}
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m) :
  Function.Injective
    ⇑(CryptBoolean.fieldMaioranaMcFarlandLinearMap theta)

theorem CryptBoolean.fieldMaioranaMcFarlandLinearMap_injective
  {m : ℕ}
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m) :
  Function.Injective
    ⇑(CryptBoolean.fieldMaioranaMcFarlandLinearMap
        theta)

Distinct field parameters give distinct members of the linear family.

defdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean

complete

def CryptBoolean.maioranaMcFarlandBentSubspace {m : ℕ}
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m) :
  Submodule FABL.𝔽₂ (CryptBoolean.BooleanFunction (m + m))

def CryptBoolean.maioranaMcFarlandBentSubspace
  {m : ℕ}
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m) :
  Submodule FABL.𝔽₂
    (CryptBoolean.BooleanFunction (m + m))

The half-dimensional linear space obtained as the range of the
field-indexed family.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean

complete

theorem CryptBoolean.finrank_maioranaMcFarlandBentSubspace {m : ℕ} (hm : 0 < m)
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m) :
  Module.finrank FABL.𝔽₂
      ↥(CryptBoolean.maioranaMcFarlandBentSubspace theta) =
    m

theorem CryptBoolean.finrank_maioranaMcFarlandBentSubspace
  {m : ℕ} (hm : 0 < m)
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m) :
  Module.finrank FABL.𝔽₂
      ↥(CryptBoolean.maioranaMcFarlandBentSubspace
          theta) =
    m

The constructed bent-function space has dimension `m`.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean

complete

theorem CryptBoolean.isBent_of_mem_maioranaMcFarlandBentSubspace {m : ℕ}
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m)
  (f : CryptBoolean.BooleanFunction (m + m))
  (hf : f ∈ CryptBoolean.maioranaMcFarlandBentSubspace theta)
  (hf0 : f ≠ 0) : CryptBoolean.IsBent f

theorem CryptBoolean.isBent_of_mem_maioranaMcFarlandBentSubspace
  {m : ℕ}
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m)
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (hf :
    f ∈
      CryptBoolean.maioranaMcFarlandBentSubspace
        theta)
  (hf0 : f ≠ 0) : CryptBoolean.IsBent f

Every nonzero function in the constructed subspace is bent.

theoremdefined in CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean

complete

theorem CryptBoolean.exists_halfDimensionalBentSubspace (m : ℕ) (hm : 0 < m) :
  ∃ B,
    Module.finrank FABL.𝔽₂ ↥B = m ∧
      ∀ f ∈ B, f ≠ 0 → CryptBoolean.IsBent f

theorem CryptBoolean.exists_halfDimensionalBentSubspace
  (m : ℕ) (hm : 0 < m) :
  ∃ B,
    Module.finrank FABL.𝔽₂ ↥B = m ∧
      ∀ f ∈ B,
        f ≠ 0 → CryptBoolean.IsBent f

In every positive even dimension `2m`, there is an `m`-dimensional
linear space of Boolean functions whose nonzero members are bent.

Theorem5.5.5

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 2

Reverse dependency previews

Preview

Proposition 5.12.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagscarletchapter-6partial-spreadpages-85-86fidelity-exact-positive-half-dimension

Dillon's partial-spread construction (Carlet, pp. 85--86). Let n be even with n/2\ge2, and let \mathcal P be a family of n/2-dimensional subspaces of V_n such that distinct members meet only at zero. If |\mathcal P|=2^{n/2-1}\quad\text{or}\quad |\mathcal P|=2^{n/2-1}+1, then the sum over \mathbb F_2 of the indicators of the members of \mathcal P is bent. Its dual is obtained by replacing every member by its orthogonal complement in the corresponding exact partial-spread expression.

Lean code for Theorem5.5.5●8 declarations

defdefined in CryptBoolean/Carlet/Chapter06/PartialSpreads.lean

complete

def CryptBoolean.IsHalfDimensionalPartialSpread {n : ℕ}
  (P : Finset (Submodule FABL.𝔽₂ (FABL.F₂Cube n))) : Prop

def CryptBoolean.IsHalfDimensionalPartialSpread
  {n : ℕ}
  (P :
    Finset
      (Submodule FABL.𝔽₂
        (FABL.F₂Cube n))) :
  Prop

A finite family of half-dimensional subspaces whose distinct members
intersect only at the origin.

defdefined in CryptBoolean/Carlet/Chapter06/PartialSpreads.lean

complete

def CryptBoolean.HasPartialSpreadBentCardinality {n : ℕ}
  (P : Finset (Submodule FABL.𝔽₂ (FABL.F₂Cube n))) : Prop

def CryptBoolean.HasPartialSpreadBentCardinality
  {n : ℕ}
  (P :
    Finset
      (Submodule FABL.𝔽₂
        (FABL.F₂Cube n))) :
  Prop

The two cardinalities used by Dillon's partial-spread classes.

defdefined in CryptBoolean/Carlet/Chapter06/PartialSpreads.lean

complete

def CryptBoolean.partialSpreadFunction {n : ℕ}
  (P : Finset (Submodule FABL.𝔽₂ (FABL.F₂Cube n))) :
  CryptBoolean.BooleanFunction n

def CryptBoolean.partialSpreadFunction {n : ℕ}
  (P :
    Finset
      (Submodule FABL.𝔽₂
        (FABL.F₂Cube n))) :
  CryptBoolean.BooleanFunction n

The Boolean sum of the indicators of the members of a partial spread.

defdefined in CryptBoolean/Carlet/Chapter06/PartialSpreads.lean

complete

def CryptBoolean.partialSpreadCoefficients {n : ℕ}
  (P : Finset (Submodule FABL.𝔽₂ (FABL.F₂Cube n))) :
  Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ

def CryptBoolean.partialSpreadCoefficients
  {n : ℕ}
  (P :
    Finset
      (Submodule FABL.𝔽₂
        (FABL.F₂Cube n))) :
  Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ

The coefficient family selecting the members of a partial spread.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartialSpreads.lean

complete

theorem CryptBoolean.bitValueInt_partialSpreadFunction_of_ne_zero {n : ℕ}
  (P : Finset (Submodule FABL.𝔽₂ (FABL.F₂Cube n)))
  (hP : CryptBoolean.IsHalfDimensionalPartialSpread P)
  (x : FABL.F₂Cube n) (hx : x ≠ 0) :
  CryptBoolean.bitValueInt (CryptBoolean.partialSpreadFunction P x) =
    ∑ E ∈ P, CryptBoolean.linearSubspaceIndicatorInt E x

theorem CryptBoolean.bitValueInt_partialSpreadFunction_of_ne_zero
  {n : ℕ}
  (P :
    Finset
      (Submodule FABL.𝔽₂ (FABL.F₂Cube n)))
  (hP :
    CryptBoolean.IsHalfDimensionalPartialSpread
      P)
  (x : FABL.F₂Cube n) (hx : x ≠ 0) :
  CryptBoolean.bitValueInt
      (CryptBoolean.partialSpreadFunction
        P x) =
    ∑ E ∈ P,
      CryptBoolean.linearSubspaceIndicatorInt
        E x

Away from the origin, the Boolean indicator sum equals its ordinary
integer indicator sum.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartialSpreads.lean

complete

theorem CryptBoolean.partialSpreadFunction_zero {n : ℕ}
  (P : Finset (Submodule FABL.𝔽₂ (FABL.F₂Cube n))) :
  CryptBoolean.partialSpreadFunction P 0 = ↑P.card

theorem CryptBoolean.partialSpreadFunction_zero
  {n : ℕ}
  (P :
    Finset
      (Submodule FABL.𝔽₂
        (FABL.F₂Cube n))) :
  CryptBoolean.partialSpreadFunction P 0 =
    ↑P.card

At the origin, a partial-spread function records the parity of the
number of selected subspaces.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartialSpreads.lean

complete

theorem CryptBoolean.hasExactGPSRepresentation_partialSpreadFunction {n : ℕ}
  (P : Finset (Submodule FABL.𝔽₂ (FABL.F₂Cube n)))
  (hP : CryptBoolean.IsHalfDimensionalPartialSpread P)
  (hcard : CryptBoolean.HasPartialSpreadBentCardinality P)
  (hhalf : 2 ≤ n / 2) :
  CryptBoolean.HasExactGPSRepresentation
    (CryptBoolean.partialSpreadFunction P)
    (CryptBoolean.partialSpreadCoefficients P)

theorem CryptBoolean.hasExactGPSRepresentation_partialSpreadFunction
  {n : ℕ}
  (P :
    Finset
      (Submodule FABL.𝔽₂ (FABL.F₂Cube n)))
  (hP :
    CryptBoolean.IsHalfDimensionalPartialSpread
      P)
  (hcard :
    CryptBoolean.HasPartialSpreadBentCardinality
      P)
  (hhalf : 2 ≤ n / 2) :
  CryptBoolean.HasExactGPSRepresentation
    (CryptBoolean.partialSpreadFunction P)
    (CryptBoolean.partialSpreadCoefficients
      P)

A partial spread of either Dillon cardinality gives the exact generalized
partial-spread expression.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartialSpreads.lean

complete

theorem CryptBoolean.isBent_partialSpreadFunction {n : ℕ}
  (P : Finset (Submodule FABL.𝔽₂ (FABL.F₂Cube n)))
  (hP : CryptBoolean.IsHalfDimensionalPartialSpread P)
  (hcard : CryptBoolean.HasPartialSpreadBentCardinality P)
  (hnEven : Even n) (hhalf : 2 ≤ n / 2) :
  CryptBoolean.IsBent (CryptBoolean.partialSpreadFunction P)

theorem CryptBoolean.isBent_partialSpreadFunction
  {n : ℕ}
  (P :
    Finset
      (Submodule FABL.𝔽₂ (FABL.F₂Cube n)))
  (hP :
    CryptBoolean.IsHalfDimensionalPartialSpread
      P)
  (hcard :
    CryptBoolean.HasPartialSpreadBentCardinality
      P)
  (hnEven : Even n) (hhalf : 2 ≤ n / 2) :
  CryptBoolean.IsBent
    (CryptBoolean.partialSpreadFunction P)

Dillon's partial-spread construction: selecting either
`2^(n/2-1)` or `2^(n/2-1)+1` pairwise disjoint half-dimensional subspaces
produces a bent function.