Cryptographic Boolean Functions in Lean

7. Strict avalanche and propagation criteria🔗

Carlet's Chapter 8 develops propagation criteria through derivative balancedness, Walsh-square identities, nonlinearity bounds, constructions, coordinate restrictions, and criteria of order. Throughout, V_n=\mathbb F_2^n and W_f denotes the unnormalized Walsh transform.

  1. 7.1. Propagation criteria and Walsh analysis
  2. 7.2. Constructions and obstructions
  3. 7.3. Propagation criteria of order