7.2. Constructions and obstructions🔗

Theorem7.2.1

Group: Chapter 7: Strict avalanche and propagation criteria (13)

Group member previews

Preview

Theorem 7.1.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Theorem 1.7.3

Loading preview

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

used by 0✓L∃∀N

Tagscarletchapter-8maiorana-mcfarlandpropagation-criterionconstructionpage-132fidelity-exact

Maiorana--McFarland propagation construction (Carlet, p. 132). Let \phi:V_s\to V_r, g:V_s\to\mathbb F_2, and f(x,y)=x\cdot\phi(y)\oplus g(y). For a\in V_r and b\in V_s, its derivative is D_{(a,b)}f(x,y)=x\cdot D_b\phi(y)\oplus a\cdot\phi(y\oplus b)\oplus D_bg(y). Suppose that D_b\phi(y)\ne0 for every y and every nonzero b with w_H(b)\le\ell, and that y\mapsto a\cdot\phi(y) is balanced for every nonzero a with w_H(a)\le\ell. Then f satisfies \mathrm{PC}(\ell). The first hypothesis is equivalent to every fiber of \phi being empty, a singleton, or a code of minimum distance greater than \ell.

Lean code for Theorem7.2.1●8 declarations

defdefined in CryptBoolean/Carlet/Chapter08/MaioranaMcFarland.lean

complete

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

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

The additive derivative of a binary-cube-valued map.

theoremdefined in CryptBoolean/Carlet/Chapter08/MaioranaMcFarland.lean

complete

theorem CryptBoolean.binaryMapDerivative_zero {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) :
  CryptBoolean.binaryMapDerivative φ 0 = 0

theorem CryptBoolean.binaryMapDerivative_zero
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) :
  CryptBoolean.binaryMapDerivative φ 0 = 0

The additive derivative of a binary map in the zero direction vanishes.

defdefined in CryptBoolean/Carlet/Chapter08/MaioranaMcFarland.lean

complete

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

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

The fibers of `φ` have minimum Hamming distance greater than `l`.
Empty and singleton fibers satisfy the condition vacuously.

theoremdefined in CryptBoolean/Carlet/Chapter08/MaioranaMcFarland.lean

complete

theorem CryptBoolean.booleanDerivative_booleanMaioranaMcFarlandGeneral_append
  {r s : ℕ} (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  FABL.booleanDerivative
      (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g)
      (Fin.append a b) =
    CryptBoolean.booleanMaioranaMcFarlandGeneral
      (CryptBoolean.binaryMapDerivative φ b) fun y =>
      FABL.f₂DotProduct a (φ (y + b)) + FABL.booleanDerivative g b y

theorem CryptBoolean.booleanDerivative_booleanMaioranaMcFarlandGeneral_append
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  FABL.booleanDerivative
      (CryptBoolean.booleanMaioranaMcFarlandGeneral
        φ g)
      (Fin.append a b) =
    CryptBoolean.booleanMaioranaMcFarlandGeneral
      (CryptBoolean.binaryMapDerivative φ
        b)
      fun y =>
      FABL.f₂DotProduct a (φ (y + b)) +
        FABL.booleanDerivative g b y

The derivative of a general Maiorana--McFarland function is again a
general Maiorana--McFarland function.

theoremdefined in CryptBoolean/Carlet/Chapter08/MaioranaMcFarland.lean

complete

theorem CryptBoolean.booleanDerivative_booleanMaioranaMcFarlandGeneral_append_apply
  {r s : ℕ} (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (a x : FABL.F₂Cube r)
  (b y : FABL.F₂Cube s) :
  FABL.booleanDerivative
      (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g)
      (Fin.append a b) (Fin.append x y) =
    FABL.f₂DotProduct x (CryptBoolean.binaryMapDerivative φ b y) +
        FABL.f₂DotProduct a (φ (y + b)) +
      FABL.booleanDerivative g b y

theorem CryptBoolean.booleanDerivative_booleanMaioranaMcFarlandGeneral_append_apply
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (a x : FABL.F₂Cube r)
  (b y : FABL.F₂Cube s) :
  FABL.booleanDerivative
      (CryptBoolean.booleanMaioranaMcFarlandGeneral
        φ g)
      (Fin.append a b) (Fin.append x y) =
    FABL.f₂DotProduct x
          (CryptBoolean.binaryMapDerivative
            φ b y) +
        FABL.f₂DotProduct a (φ (y + b)) +
      FABL.booleanDerivative g b y

Carlet's displayed pointwise derivative identity.

theoremdefined in CryptBoolean/Carlet/Chapter08/MaioranaMcFarland.lean

complete

theorem CryptBoolean.binaryMapDerivative_ne_zero_iff_fibersHaveMinimumDistanceGreaterThan
  {r s : ℕ} (φ : FABL.F₂Cube s → FABL.F₂Cube r) (l : ℕ) :
  (∀ (b : FABL.F₂Cube s),
      b ≠ 0 →
        (FABL.f₂Support b).card ≤ l →
          ∀ (y : FABL.F₂Cube s),
            CryptBoolean.binaryMapDerivative φ b y ≠ 0) ↔
    CryptBoolean.MaioranaMcFarlandFibersHaveMinimumDistanceGreaterThan φ
      l

theorem CryptBoolean.binaryMapDerivative_ne_zero_iff_fibersHaveMinimumDistanceGreaterThan
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (l : ℕ) :
  (∀ (b : FABL.F₂Cube s),
      b ≠ 0 →
        (FABL.f₂Support b).card ≤ l →
          ∀ (y : FABL.F₂Cube s),
            CryptBoolean.binaryMapDerivative
                φ b y ≠
              0) ↔
    CryptBoolean.MaioranaMcFarlandFibersHaveMinimumDistanceGreaterThan
      φ l

Nonvanishing map derivatives in all nonzero directions of weight at most
`l` are equivalent to every fiber having minimum distance greater than `l`.

theoremdefined in CryptBoolean/Carlet/Chapter08/MaioranaMcFarland.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterion_booleanMaioranaMcFarlandGeneral
  {r s : ℕ} (l : ℕ) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hderivative :
    ∀ (b : FABL.F₂Cube s),
      b ≠ 0 →
        (FABL.f₂Support b).card ≤ l →
          ∀ (y : FABL.F₂Cube s),
            CryptBoolean.binaryMapDerivative φ b y ≠ 0)
  (hbalanced :
    ∀ (a : FABL.F₂Cube r),
      a ≠ 0 →
        (FABL.f₂Support a).card ≤ l →
          CryptBoolean.IsBalanced fun y => FABL.f₂DotProduct a (φ y)) :
  CryptBoolean.SatisfiesPropagationCriterion l
    (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g)

theorem CryptBoolean.satisfiesPropagationCriterion_booleanMaioranaMcFarlandGeneral
  {r s : ℕ} (l : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hderivative :
    ∀ (b : FABL.F₂Cube s),
      b ≠ 0 →
        (FABL.f₂Support b).card ≤ l →
          ∀ (y : FABL.F₂Cube s),
            CryptBoolean.binaryMapDerivative
                φ b y ≠
              0)
  (hbalanced :
    ∀ (a : FABL.F₂Cube r),
      a ≠ 0 →
        (FABL.f₂Support a).card ≤ l →
          CryptBoolean.IsBalanced fun y =>
            FABL.f₂DotProduct a (φ y)) :
  CryptBoolean.SatisfiesPropagationCriterion
    l
    (CryptBoolean.booleanMaioranaMcFarlandGeneral
      φ g)

Carlet's Maiorana--McFarland sufficient condition for `PC(l)`.

theoremdefined in CryptBoolean/Carlet/Chapter08/MaioranaMcFarland.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterion_booleanMaioranaMcFarlandGeneral_of_fibers
  {r s : ℕ} (l : ℕ) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hfibers :
    CryptBoolean.MaioranaMcFarlandFibersHaveMinimumDistanceGreaterThan φ
      l)
  (hbalanced :
    ∀ (a : FABL.F₂Cube r),
      a ≠ 0 →
        (FABL.f₂Support a).card ≤ l →
          CryptBoolean.IsBalanced fun y => FABL.f₂DotProduct a (φ y)) :
  CryptBoolean.SatisfiesPropagationCriterion l
    (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g)

theorem CryptBoolean.satisfiesPropagationCriterion_booleanMaioranaMcFarlandGeneral_of_fibers
  {r s : ℕ} (l : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hfibers :
    CryptBoolean.MaioranaMcFarlandFibersHaveMinimumDistanceGreaterThan
      φ l)
  (hbalanced :
    ∀ (a : FABL.F₂Cube r),
      a ≠ 0 →
        (FABL.f₂Support a).card ≤ l →
          CryptBoolean.IsBalanced fun y =>
            FABL.f₂DotProduct a (φ y)) :
  CryptBoolean.SatisfiesPropagationCriterion
    l
    (CryptBoolean.booleanMaioranaMcFarlandGeneral
      φ g)

The fiber-distance form of Carlet's Maiorana--McFarland propagation
construction.

Theorem7.2.2

Group: Chapter 7: Strict avalanche and propagation criteria (13)

Group member previews

Preview

Theorem 7.1.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Proposition 6.3.10

Loading preview

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

used by 0✓L∃∀N

Tagscarletchapter-8dobbertinpropagation-criterionobstructionpage-132fidelity-exact

Obstruction for Dobbertin's construction (Carlet, p. 132). Let n>0 be even. Let f:V_{n/2}\times V_{n/2}\to\mathbb F_2 be bent with f(x,0)=0 for every x, let g:V_{n/2}\to\mathbb F_2 be balanced, and define h(x,y)=f(x,y)\oplus\delta_0(y)g(x). If n/2\le\ell\le n, then h does not satisfy \mathrm{PC}(\ell).

Lean code for Theorem7.2.2●1 theorem

theoremdefined in CryptBoolean/Carlet/Chapter08/DobbertinObstruction.lean

complete

theorem CryptBoolean.not_satisfiesPropagationCriterion_dobbertinConstruction
  {m : ℕ} (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) (_hm : 0 < m)
  (hf : CryptBoolean.IsBent f)
  (hflat : ∀ (x : FABL.F₂Cube m), f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) (l : ℕ) (hlower : m ≤ l)
  (_hupper : l ≤ m + m) :
  ¬CryptBoolean.SatisfiesPropagationCriterion l
      (CryptBoolean.dobbertinConstruction f g)

theorem CryptBoolean.not_satisfiesPropagationCriterion_dobbertinConstruction
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (_hm : 0 < m)
  (hf : CryptBoolean.IsBent f)
  (hflat :
    ∀ (x : FABL.F₂Cube m),
      f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) (l : ℕ)
  (hlower : m ≤ l) (_hupper : l ≤ m + m) :
  ¬CryptBoolean.SatisfiesPropagationCriterion
      l
      (CryptBoolean.dobbertinConstruction
        f g)

Carlet Section 8.1.2: Dobbertin's balanced modification of a normal bent
function cannot satisfy `PC(l)` when `l` is at least half the dimension.