Feistel networks and the Luby–Rackoff theorem

A Feistel round ([BS23], Section 4.5; [LR88]) turns an arbitrary function f : G → G on an additive group G into a bijection feistelRoundEquiv f : G × G ≃ G × G mapping (L, R) to (R, L + f R) with explicit inverse (L', R') ↦ (R' - f L', L') requiring no invertibility of f. Composing a list of round functions yields the multi-round Feistel cipher feistelNetwork, specialized to the three-round (feistel3) and four-round (feistel4) networks. Over any group of exponent two (∀ x : G, -x = x, including BitString n), swapping the two halves (Equiv.prodComm G G) conjugates feistelNetwork fs.reverse to the inverse cipher (feistelNetwork fs).symm.

We prove the Luby–Rackoff theorem ([BS23], Section 4.5, Theorem 4.9; [LR88]):

1. Information-theoretic core with Δ-universal Round 1: when the first round function is drawn from an ε-almost-Δ-universal family (IsDeltaUniversalHash seed₁ h₁ ε) and the second and third round functions are independent uniform random functions on G, any adaptive adversary program : OracleComp (fun _ : G × G => G × G) Bool making at most Q queries (IsQueryBounded program Q) distinguishes the three-round Feistel network from a uniform random function on G × G with advantage at most $$\binom{Q}{2} \cdot \varepsilon + \binom{Q}{2} \cdot \frac{1}{|G|}$$ (advantage_feistel3HashIdealGame_randomFunctionGame_le).
2. Classical three-round information-theoretic bound: a uniform random function on G is |G|⁻¹-Δ-universal (isDeltaUniversalHash_uniformOfFintype), so three independent uniform random round functions have distinguishing advantage against a uniform random function on G × G at most $$\frac{2 \binom{Q}{2}}{|G|} = \frac{Q (Q - 1)}{|G|}$$ (advantage_feistel3RandomRoundsGame_randomFunctionGame_le).
3. Computational PRF-to-Feistel hybrid reductions (3-round and 4-round) and PRP switching: replacing keyed round functions F kᵢ with independent uniform random round functions adds at most the sum of the single-round PRF advantages (advantage_feistel3KeyedGame_feistel3RandomRoundsGame_le, advantage_feistel3KeyedGame_randomFunctionGame_le, and the four-round bidirectional chosen-ciphertext hybrid bound advantage_feistel4StrongKeyedGame_feistel4StrongRandomRoundsGame_le). Combining with the PRP/PRF switching bound on G × G (advantage_idealPermGame_randomFunctionGame_le) yields the pseudorandom-permutation bounds against idealPermGame (advantage_feistel3HashIdealGame_idealPermGame_le, advantage_feistel3RandomRoundsGame_idealPermGame_le, advantage_feistel3KeyedGame_idealPermGame_le).
4. Three-round chosen-ciphertext separation ([BS23], Section 4.1.3 and Exercise 4.15(b)): with two forward encryption queries and one inverse decryption query, the explicit distinguisher feistel3CCAAttack accepts any three-round Feistel network with probability 1 (eval_feistel3_feistel3CCAAttack). When l₀ = l₁, the third query asks to invert the first ciphertext, so every bidirectional permutation (feistelStrongOracle π) and idealStrongGame also accept with probability 1 (eval_feistelStrongOracle_feistel3CCAAttack_self, idealStrongGame_feistel3CCAAttack_self, advantage_feistel3CCAAttack_self). Whenever l₀ ≠ l₁, coupling idealStrongGame with the forgetful bidirectional lazy sampler shows that idealStrongGame accepts feistel3CCAAttack l₀ l₁ r₀ with probability at most |G|⁻¹ + 4 * |G × G|⁻¹ (idealStrongGame_feistel3CCAAttack_true_le), giving the quantitative nonnegligible chosen-ciphertext advantage lower bound 1 - |G|⁻¹ - 4 * |G|⁻¹ ^ 2 against idealStrongGame (le_advantage_feistel3CCAAttack_idealStrongGame_of_ne). In addition, when G has three distinct elements l₀, l₁, l₂ (|G| ≥ 3), the transposition Equiv.swap (l₀, (l₁ - l₀) + r₀) (l₂, r₀) is rejected deterministically (eval_feistelStrongOracle_swap_feistel3CCAAttack_eq_false, le_advantage_feistel3CCAAttack_idealStrongGame, advantage_feistel3CCAAttack_idealStrongGame_pos), and against the independent-table bidirectional benchmark independentTableStrongGame, feistel3CCAAttack l₀ l₁ r₀ accepts with probability |G|⁻¹ and has exact advantage 1 - |G|⁻¹ (eval_independentTableStrongGame_feistel3CCAAttack, advantage_feistel3CCAAttack_independentTable).
5. Four-round strong PRP Luby–Rackoff theorem ([LR88]; see [BS23], Section 4.1.3 for strongly secure block ciphers): when all four round functions f₁, f₂, f₃, f₄ : G → G are independent uniform random functions, coupling the inner rounds f₂, f₃ to the forgetful bidirectional lazy sampler on G × G and bounding outer-round collisions for f₁ (Round 1) and -f₄ (Round 4 on the swapped cache) shows that any Q-query adaptive chosen-ciphertext distinguisher has advantage against idealStrongGame at most $$2 \binom{Q}{2} \cdot \frac{1}{|G|} + 2 \binom{Q}{2} \cdot \frac{1}{|G|^2}$$ (with the concrete constant coming from this proof; feistel4StrongRandomRoundsGame_apply_le, idealStrongGame_apply_le_feistel4StrongRandomRoundsGame, advantage_feistel4StrongRandomRoundsGame_idealStrongGame_le, advantage_feistel4StrongRandomRoundsGame_bitString_le). Combined with the four-round PRF hybrid reduction, this gives the full four-round strong PRP theorem advantage_feistel4StrongKeyedGame_idealStrongGame_le.

Main definitions

• Cslib.Crypto.LubyRackoff.feistelRound, feistelInvRound, feistelRoundEquiv: single Feistel round and its bundled equivalence over [AddGroup G].
• Cslib.Crypto.LubyRackoff.feistelNetwork, feistel3, feistel4: multi-round, 3-round, and 4-round Feistel permutations.
• Cslib.Crypto.LubyRackoff.feistel3FixedGame, feistel3HashIdealGame, feistel3RandomRoundsGame, feistel3KeyedGame, randomFunctionGame, idealPermGame: 3-round Feistel, ideal random-function, and ideal random-permutation games.
• Cslib.Crypto.LubyRackoff.feistelStrongOracle, idealStrongGame, independentTableStrongGame, feistel4StrongKeyedGame, feistel4StrongRandomRoundsGame, feistel3CCAAttack: bidirectional (forward + inverse) oracle games and the 3-query CCA attack on 3-round Feistel.

Main results

• Cslib.Crypto.LubyRackoff.prodComm_trans_feistelNetwork_reverse_trans_prodComm: swap-reversal conjugation identity for Feistel decryption over groups of exponent two.
• Cslib.Probability.isDeltaUniversalHash_uniformOfFintype, Cslib.Probability.isDeltaUniversalHash_neg_uniformOfFintype: a uniform random function into G and its negation are |G|⁻¹-Δ-universal.
• Cslib.Crypto.LubyRackoff.feistel3HashIdealGame_apply_le, Cslib.Crypto.LubyRackoff.randomFunctionGame_apply_le_feistel3HashIdealGame: two-sided probability comparisons for 3-round Luby–Rackoff with Δ-universal Round 1.
• Cslib.Crypto.LubyRackoff.advantage_feistel3HashIdealGame_randomFunctionGame_le, Cslib.Crypto.LubyRackoff.advantage_feistel3HashIdealGame_idealPermGame_le: 3-round Luby–Rackoff bounds with Δ-universal Round 1 against randomFunctionGame and idealPermGame.
• Cslib.Crypto.LubyRackoff.advantage_feistel3RandomRoundsGame_randomFunctionGame_le, Cslib.Crypto.LubyRackoff.advantage_feistel3RandomRoundsGame_idealPermGame_le: 3-round Luby–Rackoff bounds with three uniform random round functions.
• Cslib.Crypto.LubyRackoff.advantage_feistel3KeyedGame_randomFunctionGame_le, Cslib.Crypto.LubyRackoff.advantage_feistel3KeyedGame_idealPermGame_le: Boneh–Shoup Theorem 4.9 combining the 3-round PRF hybrid reduction with the information-theoretic PRF and PRP bounds.
• Cslib.Crypto.LubyRackoff.advantage_feistel4StrongKeyedGame_feistel4StrongRandomRoundsGame_le, Cslib.Crypto.LubyRackoff.feistel4StrongRandomRoundsGame_apply_le, Cslib.Crypto.LubyRackoff.idealStrongGame_apply_le_feistel4StrongRandomRoundsGame, Cslib.Crypto.LubyRackoff.advantage_feistel4StrongRandomRoundsGame_idealStrongGame_le, Cslib.Crypto.LubyRackoff.advantage_feistel4StrongKeyedGame_idealStrongGame_le, Cslib.Crypto.LubyRackoff.advantage_feistel4StrongRandomRoundsGame_bitString_le: 4-round bidirectional PRF hybrid reduction, information-theoretic random-round collision bound, and full 4-round strong PRP Luby–Rackoff theorem.
• Cslib.Crypto.LubyRackoff.eval_feistel3_feistel3CCAAttack, Cslib.Crypto.LubyRackoff.advantage_feistel3CCAAttack_self, Cslib.Crypto.LubyRackoff.idealStrongGame_feistel3CCAAttack_true_le, Cslib.Crypto.LubyRackoff.le_advantage_feistel3CCAAttack_idealStrongGame_of_ne, Cslib.Crypto.LubyRackoff.le_advantage_feistel3CCAAttack_idealStrongGame, Cslib.Crypto.LubyRackoff.advantage_feistel3CCAAttack_independentTable: the 3-query CCA distinguisher against 3-round Feistel.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Sections 4.1.3 and 4.5 (Theorem 4.9 and Exercise 4.15(b)).
• M. Luby, C. Rackoff, How to Construct Pseudorandom Permutations from Pseudorandom Functions.

Algebraic Feistel permutations

def Cslib.Crypto.LubyRackoff.feistelRound {G : Type u_1} [AddGroup G] (f : G → G) (p : G × G) : G × G

One Feistel round (L, R) ↦ (R, L + f R) over an additive group G.

def Cslib.Crypto.LubyRackoff.feistelInvRound {G : Type u_1} [AddGroup G] (f : G → G) (p : G × G) : G × G

The inverse of one Feistel round (L', R') ↦ (R' - f L', L'), requiring no invertibility of f.

@[simp]

theorem Cslib.Crypto.LubyRackoff.feistelRound_fst {G : Type u_1} [AddGroup G] (f : G → G) (p : G × G) : (feistelRound f p).1 = p.2

@[simp]

theorem Cslib.Crypto.LubyRackoff.feistelRound_snd {G : Type u_1} [AddGroup G] (f : G → G) (p : G × G) : (feistelRound f p).2 = p.1 + f p.2

@[simp]

theorem Cslib.Crypto.LubyRackoff.feistelInvRound_fst {G : Type u_1} [AddGroup G] (f : G → G) (p : G × G) : (feistelInvRound f p).1 = p.2 - f p.1

@[simp]

theorem Cslib.Crypto.LubyRackoff.feistelInvRound_snd {G : Type u_1} [AddGroup G] (f : G → G) (p : G × G) : (feistelInvRound f p).2 = p.1

@[simp]

theorem Cslib.Crypto.LubyRackoff.feistelInvRound_feistelRound {G : Type u_1} [AddGroup G] (f : G → G) (p : G × G) : feistelInvRound f (feistelRound f p) = p

@[simp]

theorem Cslib.Crypto.LubyRackoff.feistelRound_feistelInvRound {G : Type u_1} [AddGroup G] (f : G → G) (p : G × G) : feistelRound f (feistelInvRound f p) = p

def Cslib.Crypto.LubyRackoff.feistelRoundEquiv {G : Type u_1} [AddGroup G] (f : G → G) : G × G ≃ G × G

A single Feistel round as a permutation of G × G.

@[simp]

theorem Cslib.Crypto.LubyRackoff.feistelRoundEquiv_apply {G : Type u_1} [AddGroup G] (f : G → G) (p : G × G) : (feistelRoundEquiv f) p = feistelRound f p

@[simp]

theorem Cslib.Crypto.LubyRackoff.feistelRoundEquiv_symm_apply {G : Type u_1} [AddGroup G] (f : G → G) (p : G × G) : (feistelRoundEquiv f).symm p = feistelInvRound f p

def Cslib.Crypto.LubyRackoff.feistelNetwork {G : Type u_1} [AddGroup G] (fs : List (G → G)) : G × G ≃ G × G

Multi-round Feistel network composing a list of round functions from left to right.

@[simp]

theorem Cslib.Crypto.LubyRackoff.feistelNetwork_nil {G : Type u_1} [AddGroup G] : feistelNetwork [] = Equiv.refl (G × G)

@[simp]

theorem Cslib.Crypto.LubyRackoff.feistelNetwork_singleton {G : Type u_1} [AddGroup G] (f : G → G) : feistelNetwork [f] = feistelRoundEquiv f

@[simp]

theorem Cslib.Crypto.LubyRackoff.feistelNetwork_cons {G : Type u_1} [AddGroup G] (f : G → G) (fs : List (G → G)) : feistelNetwork (f :: fs) = (feistelRoundEquiv f).trans (feistelNetwork fs)

theorem Cslib.Crypto.LubyRackoff.feistelNetwork_append {G : Type u_1} [AddGroup G] (fs₁ fs₂ : List (G → G)) : feistelNetwork (fs₁ ++ fs₂) = (feistelNetwork fs₁).trans (feistelNetwork fs₂)

theorem Cslib.Crypto.LubyRackoff.prodComm_trans_feistelRoundEquiv_trans_prodComm {G : Type u_1} [AddGroup G] (hneg : ∀ (x : G), -x = x) (f : G → G) : (Equiv.prodComm G G).trans ((feistelRoundEquiv f).trans (Equiv.prodComm G G)) = (feistelRoundEquiv f).symm

Over any group of exponent two (∀ x : G, -x = x), swapping the two halves conjugates one Feistel round to its inverse.

theorem Cslib.Crypto.LubyRackoff.prodComm_trans_feistelNetwork_reverse_trans_prodComm {G : Type u_1} [AddGroup G] (hneg : ∀ (x : G), -x = x) (fs : List (G → G)) : (Equiv.prodComm G G).trans ((feistelNetwork fs.reverse).trans (Equiv.prodComm G G)) = (feistelNetwork fs).symm

Over any group of exponent two (∀ x : G, -x = x), Feistel decryption is Feistel encryption with the round functions in reverse order, conjugated by swapping the two halves.

def Cslib.Crypto.LubyRackoff.feistel3 {G : Type u_1} [AddGroup G] (f₁ f₂ f₃ : G → G) : G × G ≃ G × G

The three-round Feistel permutation (feistelRoundEquiv f₁).trans ((feistelRoundEquiv f₂).trans (feistelRoundEquiv f₃)).

def Cslib.Crypto.LubyRackoff.feistel4 {G : Type u_1} [AddGroup G] (f₁ f₂ f₃ f₄ : G → G) : G × G ≃ G × G

The four-round Feistel permutation (feistel3 f₁ f₂ f₃).trans (feistelRoundEquiv f₄).

theorem Cslib.Crypto.LubyRackoff.feistelNetwork_three {G : Type u_1} [AddGroup G] (f₁ f₂ f₃ : G → G) : feistelNetwork [f₁, f₂, f₃] = feistel3 f₁ f₂ f₃

theorem Cslib.Crypto.LubyRackoff.feistelNetwork_four {G : Type u_1} [AddGroup G] (f₁ f₂ f₃ f₄ : G → G) : feistelNetwork [f₁, f₂, f₃, f₄] = feistel4 f₁ f₂ f₃ f₄

theorem Cslib.Crypto.LubyRackoff.feistel3_apply {G : Type u_1} [AddGroup G] (f₁ f₂ f₃ : G → G) (p : G × G) : (feistel3 f₁ f₂ f₃) p = (p.2 + f₂ (p.1 + f₁ p.2), p.1 + f₁ p.2 + f₃ (p.2 + f₂ (p.1 + f₁ p.2)))

theorem Cslib.Crypto.LubyRackoff.feistel3_symm_apply {G : Type u_1} [AddGroup G] (f₁ f₂ f₃ : G → G) (vw : G × G) : (feistel3 f₁ f₂ f₃).symm vw = (vw.2 - f₃ vw.1 - f₁ (vw.1 - f₂ (vw.2 - f₃ vw.1)), vw.1 - f₂ (vw.2 - f₃ vw.1))

theorem Cslib.Crypto.LubyRackoff.feistel4_apply {G : Type u_1} [AddGroup G] (f₁ f₂ f₃ f₄ : G → G) (p : G × G) : (feistel4 f₁ f₂ f₃ f₄) p = feistelRound f₄ ((feistel3 f₁ f₂ f₃) p)

theorem Cslib.Crypto.LubyRackoff.feistel4_symm_apply {G : Type u_1} [AddGroup G] (f₁ f₂ f₃ f₄ : G → G) (wz : G × G) : (feistel4 f₁ f₂ f₃ f₄).symm wz = (feistel3 f₁ f₂ f₃).symm (feistelInvRound f₄ wz)

The 3-round Luby–Rackoff theorem

noncomputable def Cslib.Crypto.LubyRackoff.feistel3FixedGame {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (f₁ : G → G) (program : OracleComp (fun (x : G × G) => G × G) Bool) : Game

The 3-round Feistel game with a fixed first round function f₁ and independent uniform random second and third round functions f₂, f₃ : G → G.

noncomputable def Cslib.Crypto.LubyRackoff.feistel3HashIdealGame {K₁ G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (seed₁ : PMF K₁) (h₁ : K₁ → G → G) (program : OracleComp (fun (x : G × G) => G × G) Bool) : Game

The 3-round Feistel game where the first round function is drawn from a keyed hash family (seed₁, h₁) and the second and third round functions are independent uniform random functions.

noncomputable def Cslib.Crypto.LubyRackoff.feistel3RandomRoundsGame {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (program : OracleComp (fun (x : G × G) => G × G) Bool) : Game

The 3-round Feistel game with three independent uniform random round functions f₁, f₂, f₃ : G → G.

noncomputable def Cslib.Crypto.LubyRackoff.randomFunctionGame {G : Type} [Fintype G] [DecidableEq G] [Nonempty G] (program : OracleComp (fun (x : G × G) => G × G) Bool) : Game

The ideal random-function game on G × G: sample a uniform table (G × G) → (G × G) and answer every query from it.

noncomputable def Cslib.Crypto.LubyRackoff.idealPermGame {G : Type} [Fintype G] [DecidableEq G] (program : OracleComp (fun (x : G × G) => G × G) Bool) : Game

The ideal random-permutation game on G × G: sample a uniform permutation π ← PMF.uniformOfFintype (Equiv.Perm (G × G)) and answer every query via π p.

theorem Cslib.Crypto.LubyRackoff.feistel3HashIdealGame_apply_le {K₁ G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {seed₁ : PMF K₁} {h₁ : K₁ → G → G} {ε : ENNReal} (hh₁ : Probability.IsDeltaUniversalHash seed₁ h₁ ε) {program : OracleComp (fun (x : G × G) => G × G) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) (b : Bool) : (feistel3HashIdealGame seed₁ h₁ program) b ≤ (randomFunctionGame program) b + (↑(Q.choose 2) * ε + ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹)

3-round Luby–Rackoff theorem in ℝ≥0∞ (with Δ-universal Round 1): for any adaptive program making at most Q queries, feistel3HashIdealGame accepts with probability at most randomFunctionGame plus Q.choose 2 * ε + Q.choose 2 * |G|⁻¹.

theorem Cslib.Crypto.LubyRackoff.randomFunctionGame_apply_le_feistel3HashIdealGame {K₁ G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {seed₁ : PMF K₁} {h₁ : K₁ → G → G} {ε : ENNReal} (hh₁ : Probability.IsDeltaUniversalHash seed₁ h₁ ε) {program : OracleComp (fun (x : G × G) => G × G) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) (b : Bool) : (randomFunctionGame program) b ≤ (feistel3HashIdealGame seed₁ h₁ program) b + (↑(Q.choose 2) * ε + ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹)

Reverse inequality for the 3-round Luby–Rackoff bound with Δ-universal Round 1: randomFunctionGame accept probability is bounded by feistel3HashIdealGame plus the collision term.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel3HashIdealGame_randomFunctionGame_le {K₁ G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {seed₁ : PMF K₁} {h₁ : K₁ → G → G} {ε : ENNReal} (hh₁ : Probability.IsDeltaUniversalHash seed₁ h₁ ε) (hε : ε ≠ ⊤) {program : OracleComp (fun (x : G × G) => G × G) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) : ↑((feistel3HashIdealGame seed₁ h₁ program).advantage (randomFunctionGame program)) ≤ ↑(Q.choose 2) * ε.toReal + ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹

3-round Luby–Rackoff theorem with Δ-universal Round 1 ([BS23], Section 4.5.1; [LR88]): when Round 1 is drawn from an ε-almost-Δ-universal hash family and Rounds 2 and 3 are independent uniform random functions on G, any Q-query adaptive adversary has distinguishing advantage against a uniform random function on G × G at most Q.choose 2 * ε.toReal + Q.choose 2 / |G|.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel3RandomRoundsGame_randomFunctionGame_le {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {program : OracleComp (fun (x : G × G) => G × G) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) : ↑((feistel3RandomRoundsGame program).advantage (randomFunctionGame program)) ≤ 2 * ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹

Classical 3-round Luby–Rackoff theorem ([BS23], Section 4.5, Theorem 4.9; [LR88]): three Feistel rounds with independent uniform random round functions on G are indistinguishable from a uniform random function on G × G up to 2 * Q.choose 2 / |G| = Q * (Q - 1) / |G| for any Q-query adaptive adversary.

theorem Cslib.Crypto.LubyRackoff.advantage_idealPermGame_randomFunctionGame_le {G : Type} [Fintype G] [DecidableEq G] [Nonempty G] {program : OracleComp (fun (x : G × G) => G × G) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) : ↑((idealPermGame program).advantage (randomFunctionGame program)) ≤ ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹ ^ 2

PRP/PRF switching bound on G × G: for any Q-query adaptive adversary, idealPermGame and randomFunctionGame have distinguishing advantage at most Q.choose 2 / |G| ^ 2.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel3HashIdealGame_idealPermGame_le {K₁ G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {seed₁ : PMF K₁} {h₁ : K₁ → G → G} {ε : ENNReal} (hh₁ : Probability.IsDeltaUniversalHash seed₁ h₁ ε) (hε : ε ≠ ⊤) {program : OracleComp (fun (x : G × G) => G × G) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) : ↑((feistel3HashIdealGame seed₁ h₁ program).advantage (idealPermGame program)) ≤ ↑(Q.choose 2) * ε.toReal + ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹ + ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹ ^ 2

3-round Luby–Rackoff PRP bound with Δ-universal Round 1: against a uniform random permutation on G × G (idealPermGame), the distinguishing advantage of a Q-query adversary is at most Q.choose 2 * ε.toReal + Q.choose 2 / |G| + Q.choose 2 / |G| ^ 2.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel3RandomRoundsGame_idealPermGame_le {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {program : OracleComp (fun (x : G × G) => G × G) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) : ↑((feistel3RandomRoundsGame program).advantage (idealPermGame program)) ≤ 2 * ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹ + ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹ ^ 2

Classical 3-round Luby–Rackoff PRP bound: three Feistel rounds with independent uniform random round functions on G are indistinguishable from a uniform random permutation on G × G (idealPermGame) up to 2 * Q.choose 2 / |G| + Q.choose 2 / |G| ^ 2.

3-round PRF-to-Feistel hybrid reductions (Boneh–Shoup Theorem 4.9)

noncomputable def Cslib.Crypto.LubyRackoff.prfSingleRealGame {K G : Type} (keyGen : PMF K) (F : K → G → G) (B : OracleComp (fun (x : G) => G) Bool) : Game

Single-round PRF real game: sample k ← keyGen and answer queries with F k.

noncomputable def Cslib.Crypto.LubyRackoff.prfSingleIdealGame {G : Type} [Fintype G] [DecidableEq G] [Nonempty G] (B : OracleComp (fun (x : G) => G) Bool) : Game

Single-round PRF ideal game: sample a uniform random function f : G → G.

noncomputable def Cslib.Crypto.LubyRackoff.feistel3KeyedGame {K G : Type} [AddGroup G] (keyGen : PMF K) (F : K → G → G) (program : OracleComp (fun (x : G × G) => G × G) Bool) : Game

The 3-round Feistel game with three independent keyed round functions F k₁, F k₂, F k₃.

def Cslib.Crypto.LubyRackoff.feistel3Reduction₁ {G : Type} [AddGroup G] (f₂ f₃ : G → G) (program : OracleComp (fun (x : G × G) => G × G) Bool) : OracleComp (fun (x : G) => G) Bool

Round-1 PRF reduction distinguisher for fixed f₂, f₃ : G → G.

def Cslib.Crypto.LubyRackoff.feistel3Reduction₂ {G : Type} [AddGroup G] (f₁ f₃ : G → G) (program : OracleComp (fun (x : G × G) => G × G) Bool) : OracleComp (fun (x : G) => G) Bool

Round-2 PRF reduction distinguisher for fixed f₁, f₃ : G → G.

def Cslib.Crypto.LubyRackoff.feistel3Reduction₃ {G : Type} [AddGroup G] (f₁ f₂ : G → G) (program : OracleComp (fun (x : G × G) => G × G) Bool) : OracleComp (fun (x : G) => G) Bool

Round-3 PRF reduction distinguisher for fixed f₁, f₂ : G → G.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel3KeyedGame_feistel3RandomRoundsGame_le {K G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {keyGen : PMF K} {F : K → G → G} {program : OracleComp (fun (x : G × G) => G × G) Bool} {ε₁ ε₂ ε₃ : ℝ} (h₁ : ∀ (f₂ f₃ : G → G), ↑((prfSingleRealGame keyGen F (feistel3Reduction₁ f₂ f₃ program)).advantage (prfSingleIdealGame (feistel3Reduction₁ f₂ f₃ program))) ≤ ε₁) (h₂ : ∀ (f₁ f₃ : G → G), ↑((prfSingleRealGame keyGen F (feistel3Reduction₂ f₁ f₃ program)).advantage (prfSingleIdealGame (feistel3Reduction₂ f₁ f₃ program))) ≤ ε₂) (h₃ : ∀ (f₁ f₂ : G → G), ↑((prfSingleRealGame keyGen F (feistel3Reduction₃ f₁ f₂ program)).advantage (prfSingleIdealGame (feistel3Reduction₃ f₁ f₂ program))) ≤ ε₃) : ↑((feistel3KeyedGame keyGen F program).advantage (feistel3RandomRoundsGame program)) ≤ ε₁ + ε₂ + ε₃

Replacing the three keyed round functions F k₁, F k₂, F k₃ with independent uniform random round functions adds at most the sum of the three single-round PRF advantages.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel3KeyedGame_randomFunctionGame_le {K G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {keyGen : PMF K} {F : K → G → G} {program : OracleComp (fun (x : G × G) => G × G) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) {ε₁ ε₂ ε₃ : ℝ} (h₁ : ∀ (f₂ f₃ : G → G), ↑((prfSingleRealGame keyGen F (feistel3Reduction₁ f₂ f₃ program)).advantage (prfSingleIdealGame (feistel3Reduction₁ f₂ f₃ program))) ≤ ε₁) (h₂ : ∀ (f₁ f₃ : G → G), ↑((prfSingleRealGame keyGen F (feistel3Reduction₂ f₁ f₃ program)).advantage (prfSingleIdealGame (feistel3Reduction₂ f₁ f₃ program))) ≤ ε₂) (h₃ : ∀ (f₁ f₂ : G → G), ↑((prfSingleRealGame keyGen F (feistel3Reduction₃ f₁ f₂ program)).advantage (prfSingleIdealGame (feistel3Reduction₃ f₁ f₂ program))) ≤ ε₃) : ↑((feistel3KeyedGame keyGen F program).advantage (randomFunctionGame program)) ≤ ε₁ + ε₂ + ε₃ + 2 * ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹

The Luby–Rackoff theorem ([BS23], Section 4.5, Theorem 4.9; [LR88]): a 3-round Feistel cipher built from three independently keyed instances of a round function F has distinguishing advantage against a uniform random function on G × G at most ε₁ + ε₂ + ε₃ + 2 * Q.choose 2 / |G|.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel3KeyedGame_idealPermGame_le {K G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {keyGen : PMF K} {F : K → G → G} {program : OracleComp (fun (x : G × G) => G × G) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) {ε₁ ε₂ ε₃ : ℝ} (h₁ : ∀ (f₂ f₃ : G → G), ↑((prfSingleRealGame keyGen F (feistel3Reduction₁ f₂ f₃ program)).advantage (prfSingleIdealGame (feistel3Reduction₁ f₂ f₃ program))) ≤ ε₁) (h₂ : ∀ (f₁ f₃ : G → G), ↑((prfSingleRealGame keyGen F (feistel3Reduction₂ f₁ f₃ program)).advantage (prfSingleIdealGame (feistel3Reduction₂ f₁ f₃ program))) ≤ ε₂) (h₃ : ∀ (f₁ f₂ : G → G), ↑((prfSingleRealGame keyGen F (feistel3Reduction₃ f₁ f₂ program)).advantage (prfSingleIdealGame (feistel3Reduction₃ f₁ f₂ program))) ≤ ε₃) : ↑((feistel3KeyedGame keyGen F program).advantage (idealPermGame program)) ≤ ε₁ + ε₂ + ε₃ + 2 * ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹ + ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹ ^ 2

The Luby–Rackoff PRP theorem ([BS23], Section 4.5, Theorem 4.9; [LR88]): a 3-round Feistel cipher built from three independently keyed instances of a round function F has distinguishing advantage against a uniform random permutation on G × G (idealPermGame) at most ε₁ + ε₂ + ε₃ + 2 * Q.choose 2 / |G| + Q.choose 2 / |G| ^ 2.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel3RandomRoundsGame_bitString_le (n : ℕ) {program : OracleComp (fun (x : BitString n × BitString n) => BitString n × BitString n) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) : ↑((feistel3RandomRoundsGame program).advantage (randomFunctionGame program)) ≤ 2 * ↑(Q.choose 2) * (2 ^ n)⁻¹

Concrete instantiation of the 3-round Luby–Rackoff theorem on BitString n (block size 2n): the information-theoretic collision error is at most 2 * Q.choose 2 / 2 ^ n.

Chosen-ciphertext separation for 3 rounds and 4-round bidirectional hybrid security

noncomputable def Cslib.Crypto.LubyRackoff.feistelStrongOracle {G : Type} (π : G × G ≃ G × G) (q : Bool × G × G) : PMF (G × G)

Bidirectional permutation oracle on G × G: (false, p) evaluates forward encryption π p, and (true, q) evaluates inverse decryption π.symm q.

noncomputable def Cslib.Crypto.LubyRackoff.idealStrongGame {G : Type} [Fintype G] [DecidableEq G] (program : OracleComp (fun (x : Bool × G × G) => G × G) Bool) : Game

Ideal bidirectional random-permutation game on G × G: sample a uniform permutation π ← PMF.uniformOfFintype (Equiv.Perm (G × G)) and answer forward and inverse queries via feistelStrongOracle π.

noncomputable def Cslib.Crypto.LubyRackoff.independentTableStrongGame {G : Type} [Fintype G] [DecidableEq G] [Nonempty G] (program : OracleComp (fun (x : Bool × G × G) => G × G) Bool) : Game

Bidirectional independent-table game on Bool × (G × G) → G × G, where forward and inverse queries are answered by two independent uniform random functions.

def Cslib.Crypto.LubyRackoff.feistel3CCAAttack {G : Type} [AddGroup G] [DecidableEq G] (l₀ l₁ r₀ : G) : OracleComp (fun (x : Bool × G × G) => G × G) Bool

The 3-query chosen-ciphertext distinguisher against 3-round Feistel ([BS23], Exercise 4.15(b)):

1. Query encryption at (l₀, r₀) to obtain (v₀, w₀).
2. Query encryption at (l₁, r₀) to obtain (v₁, w₁).
3. Query decryption at (v₀, (l₁ - l₀) + w₀) to obtain (l₂, r₂).
4. Accept iff -v₀ + r₂ = -v₁ + r₀.

theorem Cslib.Crypto.LubyRackoff.isQueryBounded_feistel3CCAAttack {G : Type} [AddGroup G] [DecidableEq G] (l₀ l₁ r₀ : G) : (feistel3CCAAttack l₀ l₁ r₀).IsQueryBounded 3

feistel3CCAAttack makes at most 3 oracle queries.

theorem Cslib.Crypto.LubyRackoff.eval_feistel3_feistel3CCAAttack {G : Type} [AddGroup G] [DecidableEq G] (f₁ f₂ f₃ : G → G) (l₀ l₁ r₀ : G) : OracleComp.interpret (feistelStrongOracle (feistel3 f₁ f₂ f₃)) (feistel3CCAAttack l₀ l₁ r₀) = PMF.pure true

Every 3-round Feistel network feistel3 f₁ f₂ f₃ is accepted with probability 1 by feistel3CCAAttack ([BS23], Exercise 4.15(b)), for any round functions f₁, f₂, f₃ and any l₀, l₁, r₀ : G.

theorem Cslib.Crypto.LubyRackoff.eval_feistelStrongOracle_feistel3CCAAttack_self {G : Type} [AddGroup G] [DecidableEq G] (π : G × G ≃ G × G) (l₀ r₀ : G) : OracleComp.interpret (feistelStrongOracle π) (feistel3CCAAttack l₀ l₀ r₀) = PMF.pure true

When l₀ = l₁, the third query of feistel3CCAAttack l₀ l₀ r₀ asks to invert the first ciphertext, so every bidirectional permutation π : G × G ≃ G × G is accepted with probability 1.

theorem Cslib.Crypto.LubyRackoff.idealStrongGame_feistel3CCAAttack_self {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] (l₀ r₀ : G) : idealStrongGame (feistel3CCAAttack l₀ l₀ r₀) = PMF.pure true

At l₀ = l₁, the permutation-ideal game idealStrongGame accepts feistel3CCAAttack l₀ l₀ r₀ with probability 1.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel3CCAAttack_self {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] (f₁ f₂ f₃ : G → G) (l₀ r₀ : G) : Game.advantage (OracleComp.interpret (feistelStrongOracle (feistel3 f₁ f₂ f₃)) (feistel3CCAAttack l₀ l₀ r₀)) (idealStrongGame (feistel3CCAAttack l₀ l₀ r₀)) = 0

At l₀ = l₁, feistel3CCAAttack l₀ l₀ r₀ has zero advantage between any 3-round Feistel network and the true bidirectional random-permutation game idealStrongGame.

theorem Cslib.Crypto.LubyRackoff.eval_feistelStrongOracle_swap_feistel3CCAAttack_eq_false {G : Type} [AddGroup G] [DecidableEq G] {l₀ l₁ l₂ r₀ : G} (h01 : l₀ ≠ l₁) (h02 : l₀ ≠ l₂) (h12 : l₁ ≠ l₂) : OracleComp.interpret (feistelStrongOracle (Equiv.swap (l₀, l₁ - l₀ + r₀) (l₂, r₀))) (feistel3CCAAttack l₀ l₁ r₀) = PMF.pure false

When l₀, l₁, l₂ : G are pairwise distinct (|G| ≥ 3), the transposition Equiv.swap (l₀, (l₁ - l₀) + r₀) (l₂, r₀) fixes (l₀, r₀) and (l₁, r₀) while mapping (l₀, (l₁ - l₀) + r₀) to (l₂, r₀), so feistel3CCAAttack l₀ l₁ r₀ rejects it with probability 1.

theorem Cslib.Crypto.LubyRackoff.le_idealStrongGame_feistel3CCAAttack_false {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] {l₀ l₁ l₂ r₀ : G} (h01 : l₀ ≠ l₁) (h02 : l₀ ≠ l₂) (h12 : l₁ ≠ l₂) : (↑(Fintype.card (Equiv.Perm (G × G))))⁻¹ ≤ (idealStrongGame (feistel3CCAAttack l₀ l₁ r₀)) false

When l₀, l₁, l₂ : G are pairwise distinct, idealStrongGame (feistel3CCAAttack l₀ l₁ r₀) rejects (false) with probability at least |Equiv.Perm (G × G)|⁻¹.

theorem Cslib.Crypto.LubyRackoff.le_advantage_feistel3CCAAttack_idealStrongGame {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] (f₁ f₂ f₃ : G → G) {l₀ l₁ l₂ r₀ : G} (h01 : l₀ ≠ l₁) (h02 : l₀ ≠ l₂) (h12 : l₁ ≠ l₂) : (↑(Fintype.card (Equiv.Perm (G × G))))⁻¹ ≤ ↑(Game.advantage (OracleComp.interpret (feistelStrongOracle (feistel3 f₁ f₂ f₃)) (feistel3CCAAttack l₀ l₁ r₀)) (idealStrongGame (feistel3CCAAttack l₀ l₁ r₀)))

When l₀, l₁, l₂ : G are pairwise distinct (|G| ≥ 3), feistel3CCAAttack l₀ l₁ r₀ distinguishes any 3-round Feistel network from the true bidirectional random-permutation game idealStrongGame with advantage at least |Equiv.Perm (G × G)|⁻¹.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel3CCAAttack_idealStrongGame_pos {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] (f₁ f₂ f₃ : G → G) {l₀ l₁ l₂ r₀ : G} (h01 : l₀ ≠ l₁) (h02 : l₀ ≠ l₂) (h12 : l₁ ≠ l₂) : 0 < ↑(Game.advantage (OracleComp.interpret (feistelStrongOracle (feistel3 f₁ f₂ f₃)) (feistel3CCAAttack l₀ l₁ r₀)) (idealStrongGame (feistel3CCAAttack l₀ l₁ r₀)))

When l₀, l₁, l₂ : G are pairwise distinct (|G| ≥ 3), feistel3CCAAttack l₀ l₁ r₀ has strictly positive distinguishing advantage against the true bidirectional random-permutation game idealStrongGame.

theorem Cslib.Crypto.LubyRackoff.eval_independentTableStrongGame_feistel3CCAAttack {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (l₀ l₁ r₀ : G) : (independentTableStrongGame (feistel3CCAAttack l₀ l₁ r₀)) true = (↑(Fintype.card G))⁻¹

Against the independent-table game independentTableStrongGame, feistel3CCAAttack l₀ l₁ r₀ accepts with probability |G|⁻¹.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel3CCAAttack_independentTable {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (f₁ f₂ f₃ : G → G) (l₀ l₁ r₀ : G) : ↑(Game.advantage (OracleComp.interpret (feistelStrongOracle (feistel3 f₁ f₂ f₃)) (feistel3CCAAttack l₀ l₁ r₀)) (independentTableStrongGame (feistel3CCAAttack l₀ l₁ r₀))) = 1 - (↑(Fintype.card G))⁻¹

The 3-query CCA attack feistel3CCAAttack distinguishes any 3-round Feistel network from the independent-table game independentTableStrongGame with exact advantage 1 - |G|⁻¹.

theorem Cslib.Crypto.LubyRackoff.idealStrongGame_feistel3CCAAttack_true_le {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {l₀ l₁ : G} (r₀ : G) (h01 : l₀ ≠ l₁) : (idealStrongGame (feistel3CCAAttack l₀ l₁ r₀)) true ≤ (↑(Fintype.card G))⁻¹ + 4 * (↑(Fintype.card (G × G)))⁻¹

When l₀ ≠ l₁, the true bidirectional random-permutation game idealStrongGame accepts feistel3CCAAttack l₀ l₁ r₀ with probability at most |G|⁻¹ + 4 * |G × G|⁻¹.

theorem Cslib.Crypto.LubyRackoff.le_advantage_feistel3CCAAttack_idealStrongGame_of_ne {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (f₁ f₂ f₃ : G → G) {l₀ l₁ r₀ : G} (h01 : l₀ ≠ l₁) : 1 - (↑(Fintype.card G))⁻¹ - 4 * (↑(Fintype.card G))⁻¹ ^ 2 ≤ ↑(Game.advantage (OracleComp.interpret (feistelStrongOracle (feistel3 f₁ f₂ f₃)) (feistel3CCAAttack l₀ l₁ r₀)) (idealStrongGame (feistel3CCAAttack l₀ l₁ r₀)))

Quantitative nonnegligible CCA advantage lower bound against idealStrongGame ([BS23], Section 4.1.3 and Exercise 4.15(b)): whenever l₀ ≠ l₁, the 3-query chosen-ciphertext distinguisher feistel3CCAAttack l₀ l₁ r₀ distinguishes any 3-round Feistel network feistel3 f₁ f₂ f₃ from a uniform random permutation on G × G (idealStrongGame) with advantage at least 1 - |G|⁻¹ - 4 * |G|⁻¹ ^ 2.

noncomputable def Cslib.Crypto.LubyRackoff.feistel4StrongKeyedGame {K G : Type} [AddGroup G] (keyGen : PMF K) (F : K → G → G) (program : OracleComp (fun (x : Bool × G × G) => G × G) Bool) : Game

4-round Feistel strong (bidirectional) game with four independent keyed round functions F k₁, F k₂, F k₃, F k₄.

noncomputable def Cslib.Crypto.LubyRackoff.feistel4StrongRandomRoundsGame {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (program : OracleComp (fun (x : Bool × G × G) => G × G) Bool) : Game

4-round Feistel strong (bidirectional) game with four independent uniform random round functions f₁, f₂, f₃, f₄ : G → G.

def Cslib.Crypto.LubyRackoff.feistel4StrongReduction₁ {G : Type} [AddGroup G] (f₂ f₃ f₄ : G → G) (program : OracleComp (fun (x : Bool × G × G) => G × G) Bool) : OracleComp (fun (x : G) => G) Bool

Round-1 bidirectional PRF reduction distinguisher for 4-round Feistel.

def Cslib.Crypto.LubyRackoff.feistel4StrongReduction₂ {G : Type} [AddGroup G] (f₁ f₃ f₄ : G → G) (program : OracleComp (fun (x : Bool × G × G) => G × G) Bool) : OracleComp (fun (x : G) => G) Bool

Round-2 bidirectional PRF reduction distinguisher for 4-round Feistel.

def Cslib.Crypto.LubyRackoff.feistel4StrongReduction₃ {G : Type} [AddGroup G] (f₁ f₂ f₄ : G → G) (program : OracleComp (fun (x : Bool × G × G) => G × G) Bool) : OracleComp (fun (x : G) => G) Bool

Round-3 bidirectional PRF reduction distinguisher for 4-round Feistel.

def Cslib.Crypto.LubyRackoff.feistel4StrongReduction₄ {G : Type} [AddGroup G] (f₁ f₂ f₃ : G → G) (program : OracleComp (fun (x : Bool × G × G) => G × G) Bool) : OracleComp (fun (x : G) => G) Bool

Round-4 bidirectional PRF reduction distinguisher for 4-round Feistel.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel4StrongKeyedGame_feistel4StrongRandomRoundsGame_le {K G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {keyGen : PMF K} {F : K → G → G} {program : OracleComp (fun (x : Bool × G × G) => G × G) Bool} {ε₁ ε₂ ε₃ ε₄ : ℝ} (h₁ : ∀ (f₂ f₃ f₄ : G → G), ↑((prfSingleRealGame keyGen F (feistel4StrongReduction₁ f₂ f₃ f₄ program)).advantage (prfSingleIdealGame (feistel4StrongReduction₁ f₂ f₃ f₄ program))) ≤ ε₁) (h₂ : ∀ (f₁ f₃ f₄ : G → G), ↑((prfSingleRealGame keyGen F (feistel4StrongReduction₂ f₁ f₃ f₄ program)).advantage (prfSingleIdealGame (feistel4StrongReduction₂ f₁ f₃ f₄ program))) ≤ ε₂) (h₃ : ∀ (f₁ f₂ f₄ : G → G), ↑((prfSingleRealGame keyGen F (feistel4StrongReduction₃ f₁ f₂ f₄ program)).advantage (prfSingleIdealGame (feistel4StrongReduction₃ f₁ f₂ f₄ program))) ≤ ε₃) (h₄ : ∀ (f₁ f₂ f₃ : G → G), ↑((prfSingleRealGame keyGen F (feistel4StrongReduction₄ f₁ f₂ f₃ program)).advantage (prfSingleIdealGame (feistel4StrongReduction₄ f₁ f₂ f₃ program))) ≤ ε₄) : ↑((feistel4StrongKeyedGame keyGen F program).advantage (feistel4StrongRandomRoundsGame program)) ≤ ε₁ + ε₂ + ε₃ + ε₄

4-round bidirectional PRF-to-Feistel hybrid theorem: because Feistel inversion only evaluates the round functions in the forward direction, replacing four keyed round functions F k₁, F k₂, F k₃, F k₄ with independent uniform random round functions against any bidirectional (chosen-ciphertext) adversary adds at most ε₁ + ε₂ + ε₃ + ε₄.

4-round bidirectional random-round collision analysis and strong PRP Luby–Rackoff theorem

theorem Cslib.Crypto.LubyRackoff.feistel4StrongRandomRoundsGame_apply_le {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {program : OracleComp (fun (x : Bool × G × G) => G × G) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) (b : Bool) : (feistel4StrongRandomRoundsGame program) b ≤ (idealStrongGame program) b + (2 * ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹ + 2 * ↑(Q.choose 2) * (↑(Fintype.card (G × G)))⁻¹)

4-round strong Luby–Rackoff theorem in ℝ≥0∞ (one-sided): for any adaptive bidirectional program making at most Q forward or inverse queries, feistel4StrongRandomRoundsGame accepts with probability at most idealStrongGame plus 2 * Q.choose 2 * |G|⁻¹ + 2 * Q.choose 2 * |G × G|⁻¹.

theorem Cslib.Crypto.LubyRackoff.idealStrongGame_apply_le_feistel4StrongRandomRoundsGame {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {program : OracleComp (fun (x : Bool × G × G) => G × G) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) (b : Bool) : (idealStrongGame program) b ≤ (feistel4StrongRandomRoundsGame program) b + (2 * ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹ + 2 * ↑(Q.choose 2) * (↑(Fintype.card (G × G)))⁻¹)

Reverse 4-round strong Luby–Rackoff inequality in ℝ≥0∞: for any adaptive bidirectional program making at most Q forward or inverse queries, idealStrongGame accepts with probability at most feistel4StrongRandomRoundsGame plus 2 * Q.choose 2 * |G|⁻¹ + 2 * Q.choose 2 * |G × G|⁻¹.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel4StrongRandomRoundsGame_idealStrongGame_le {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {program : OracleComp (fun (x : Bool × G × G) => G × G) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) : ↑((feistel4StrongRandomRoundsGame program).advantage (idealStrongGame program)) ≤ 2 * ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹ + 2 * ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹ ^ 2

4-round strong Luby–Rackoff theorem with random round functions ([LR88]; see [BS23], Section 4.1.3 for strongly secure block ciphers; the concrete constant comes from this proof): when all four round functions f₁, f₂, f₃, f₄ : G → G are independent uniform random functions, any Q-query adaptive chosen-ciphertext distinguisher has distinguishing advantage against a uniform random permutation on G × G (idealStrongGame) at most 2 * Q.choose 2 * |G|⁻¹ + 2 * Q.choose 2 * (|G|⁻¹) ^ 2.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel4StrongKeyedGame_idealStrongGame_le {K G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] {keyGen : PMF K} {F : K → G → G} {program : OracleComp (fun (x : Bool × G × G) => G × G) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) {ε₁ ε₂ ε₃ ε₄ : ℝ} (h₁ : ∀ (f₂ f₃ f₄ : G → G), ↑((prfSingleRealGame keyGen F (feistel4StrongReduction₁ f₂ f₃ f₄ program)).advantage (prfSingleIdealGame (feistel4StrongReduction₁ f₂ f₃ f₄ program))) ≤ ε₁) (h₂ : ∀ (f₁ f₃ f₄ : G → G), ↑((prfSingleRealGame keyGen F (feistel4StrongReduction₂ f₁ f₃ f₄ program)).advantage (prfSingleIdealGame (feistel4StrongReduction₂ f₁ f₃ f₄ program))) ≤ ε₂) (h₃ : ∀ (f₁ f₂ f₄ : G → G), ↑((prfSingleRealGame keyGen F (feistel4StrongReduction₃ f₁ f₂ f₄ program)).advantage (prfSingleIdealGame (feistel4StrongReduction₃ f₁ f₂ f₄ program))) ≤ ε₃) (h₄ : ∀ (f₁ f₂ f₃ : G → G), ↑((prfSingleRealGame keyGen F (feistel4StrongReduction₄ f₁ f₂ f₃ program)).advantage (prfSingleIdealGame (feistel4StrongReduction₄ f₁ f₂ f₃ program))) ≤ ε₄) : ↑((feistel4StrongKeyedGame keyGen F program).advantage (idealStrongGame program)) ≤ ε₁ + ε₂ + ε₃ + ε₄ + 2 * ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹ + 2 * ↑(Q.choose 2) * (↑(Fintype.card G))⁻¹ ^ 2

Full 4-round strong PRP Luby–Rackoff theorem ([LR88]; see [BS23], Section 4.1.3 for strongly secure block ciphers; the concrete constant comes from this proof): combining the 4-round bidirectional PRF hybrid reduction with the random-round collision bound shows that a 4-round Feistel network instantiated with four independent keys from a PRF F : K → G → G is a strong (chosen-ciphertext secure) pseudorandom permutation on G × G, with distinguishing advantage at most ε₁ + ε₂ + ε₃ + ε₄ + 2 * Q.choose 2 * |G|⁻¹ + 2 * Q.choose 2 * (|G|⁻¹) ^ 2.

theorem Cslib.Crypto.LubyRackoff.advantage_feistel4StrongRandomRoundsGame_bitString_le (n : ℕ) {program : OracleComp (fun (x : Bool × BitString n × BitString n) => BitString n × BitString n) Bool} {Q : ℕ} (hQ : program.IsQueryBounded Q) : ↑((feistel4StrongRandomRoundsGame program).advantage (idealStrongGame program)) ≤ 2 * ↑(Q.choose 2) * (2 ^ n)⁻¹ + 2 * ↑(Q.choose 2) * (2 ^ n)⁻¹ ^ 2

Concrete instantiation of the 4-round strong Luby–Rackoff theorem on BitString n (block size 2n): the information-theoretic chosen-ciphertext collision error is at most 2 * Q.choose 2 / 2 ^ n + 2 * Q.choose 2 / (2 ^ n) ^ 2.