Hybrid Argument for XOR Encryption

This file carries out the hybrid argument for two and three instances of one-bit XOR encryption, after ProofFrog's Hybrid protocol. The games are shallow SPComp computations.

Overview

Hybrid Arguments: A standard technique for proving security reductions. If a single instance of a primitive is secure, then n instances are secure with advantage at most n times the single-instance advantage.

Core Idea: We construct a sequence of hybrid games:

• Game₀ = real game (all n instances use the real primitive)
• Gameᵢ = first i instances are ideal, remaining (n-i) are real
• Gameₙ = ideal game (all instances are ideal)

Each adjacent pair of hybrids differs in exactly one position, enabling a reduction to single-instance security.

Main Results

• single_oracle_zero_advantage - one XOR encryption has advantage 0 against a uniform ciphertext
• twoReal / twoHybrid / twoIdeal and threeHybrid - the hybrid ladders for two and three instances
• two_instance_advantage_bound, three_instance_triangle - the real-to-ideal advantage is at most the sum of the adjacent-step advantages
• hybrid_step_zero_advantage - every adjacent step of the three-instance ladder has advantage 0

ProofFrog Comparison

ProofFrog's Hybrid protocol (for PubEnc):

• Automatically generates hybrid sequence
• Uses Z3 for equivalence checking

This file:

• Explicit hybrid games as SPComp computations (selectOracle, threeHybrid)
• Advantage bounds via the triangle inequality
• Step couplings via pRHL

References

• ProofFrog: https://github.com/ProofFrog/ProofFrog
• [Bellare-Rogaway, Code-Based Game-Playing Proofs]
• [Rosulek, The Joy of Cryptography, Chapter 5]

Type Definitions

@[reducible, inline]

abbrev CatCrypt.Examples.DeepHybrid.Word : Type

Message/key/ciphertext type (simplified to Bool)

Equations

• CatCrypt.Examples.DeepHybrid.Word = Bool

@[instance_reducible]

instance CatCrypt.Examples.DeepHybrid.instFintypeWord : Fintype Word

Equations

• CatCrypt.Examples.DeepHybrid.instFintypeWord = inferInstance

instance CatCrypt.Examples.DeepHybrid.instNonemptyWord : Nonempty Word

@[instance_reducible]

instance CatCrypt.Examples.DeepHybrid.instDecidableEqWord : DecidableEq Word

Equations

• CatCrypt.Examples.DeepHybrid.instDecidableEqWord = inferInstance

Single-Instance Oracles

The hybrid argument is based on two oracles:

• Real oracle: uses the actual cryptographic primitive
• Ideal oracle: returns random/ideal output

noncomputable def CatCrypt.Examples.DeepHybrid.realOracle (m : Word) : Core.SPComp Word

Real oracle: XOR encryption (CPA$ secure)

Equations

• CatCrypt.Examples.DeepHybrid.realOracle m = do let k ← CatCrypt.Core.SPComp.sample CatCrypt.Examples.DeepHybrid.Word CatCrypt.Core.SPComp.pure (k ^^ m)

noncomputable def CatCrypt.Examples.DeepHybrid.idealOracle (_m : Word) : Core.SPComp Word

Ideal oracle: random ciphertext

Equations

• CatCrypt.Examples.DeepHybrid.idealOracle _m = CatCrypt.Core.SPComp.sample CatCrypt.Examples.DeepHybrid.Word

Single-Instance Security

The key property: XOR encryption is perfectly secure (zero advantage)

theorem CatCrypt.Examples.DeepHybrid.single_oracle_coupling (m : Word) : Relational.rHoare Relational.eqPre (realOracle m) (idealOracle m) Relational.eqPost

XOR encryption produces indistinguishable outputs for any two messages.

The proof uses bijection coupling: for uniform k, xor k m is uniformly distributed, so realOracle m and idealOracle m produce the same distribution.

theorem CatCrypt.Examples.DeepHybrid.single_oracle_zero_advantage (m : Word) (A : Word → Core.SPComp Bool) : Crypto.AdvantageA (realOracle m) (idealOracle m) A = 0

XOR encryption has zero distinguishing advantage

Hybrid Game Structure

For n oracle calls, we define:

• Hybrid i: first i calls use ideal oracle, rest use real oracle
• Hybrid 0 = all real (real game)
• Hybrid n = all ideal (ideal game)

noncomputable def CatCrypt.Examples.DeepHybrid.selectOracle (i pos : ℕ) : Word → Core.SPComp Word

Select oracle based on position relative to hybrid index

Equations

• CatCrypt.Examples.DeepHybrid.selectOracle i pos = if pos < i then CatCrypt.Examples.DeepHybrid.idealOracle else CatCrypt.Examples.DeepHybrid.realOracle

Two-Instance Hybrid Games

For concrete demonstration, we define hybrid games for two encryption instances.

noncomputable def CatCrypt.Examples.DeepHybrid.twoReal (m₀ m₁ : Word) : Core.SPComp (Word × Word)

Real game: both encryptions use real oracle

Equations

• CatCrypt.Examples.DeepHybrid.twoReal m₀ m₁ = do let c₀ ← CatCrypt.Examples.DeepHybrid.realOracle m₀ let c₁ ← CatCrypt.Examples.DeepHybrid.realOracle m₁ CatCrypt.Core.SPComp.pure (c₀, c₁)

noncomputable def CatCrypt.Examples.DeepHybrid.twoHybrid (m₀ m₁ : Word) : Core.SPComp (Word × Word)

Hybrid 1: first encryption ideal, second real

Equations

• CatCrypt.Examples.DeepHybrid.twoHybrid m₀ m₁ = do let c₀ ← CatCrypt.Examples.DeepHybrid.idealOracle m₀ let c₁ ← CatCrypt.Examples.DeepHybrid.realOracle m₁ CatCrypt.Core.SPComp.pure (c₀, c₁)

noncomputable def CatCrypt.Examples.DeepHybrid.twoIdeal (m₀ m₁ : Word) : Core.SPComp (Word × Word)

Ideal game: both encryptions use ideal oracle

Equations

• CatCrypt.Examples.DeepHybrid.twoIdeal m₀ m₁ = do let c₀ ← CatCrypt.Examples.DeepHybrid.idealOracle m₀ let c₁ ← CatCrypt.Examples.DeepHybrid.idealOracle m₁ CatCrypt.Core.SPComp.pure (c₀, c₁)

Hybrid Step Couplings

theorem CatCrypt.Examples.DeepHybrid.step_0_1_coupling (m₀ m₁ : Word) : Relational.rHoare Relational.eqPre (twoReal m₀ m₁) (twoHybrid m₀ m₁) fun (p₁ : Word × Word) (h₁ : Core.Heap) (p₂ : Word × Word) (h₂ : Core.Heap) => p₁.2 = p₂.2 ∧ Relational.eqPre h₁ h₂

Coupling between twoReal and twoHybrid (differ in position 0)

The key insight: both games use the same second oracle call (realOracle m₁), so the second components will match. The first components differ but we don't need them to match for this postcondition.

theorem CatCrypt.Examples.DeepHybrid.step_1_2_coupling (m₀ m₁ : Word) : Relational.rHoare Relational.eqPre (twoHybrid m₀ m₁) (twoIdeal m₀ m₁) fun (p₁ : Word × Word) (h₁ : Core.Heap) (p₂ : Word × Word) (h₂ : Core.Heap) => p₁.1 = p₂.1 ∧ Relational.eqPre h₁ h₂

Coupling between twoHybrid and twoIdeal (differ in position 1)

The key insight: both games use the same first oracle call (idealOracle m₀), so the first components will match.

Triangle Inequality for Advantage

The total advantage is bounded by the sum of step advantages.

theorem CatCrypt.Examples.DeepHybrid.two_instance_advantage_bound (m₀ m₁ : Word) (A : Word × Word → Core.SPComp Bool) : Crypto.AdvantageA (twoReal m₀ m₁) (twoIdeal m₀ m₁) A ≤ Crypto.AdvantageA (twoReal m₀ m₁) (twoHybrid m₀ m₁) A + Crypto.AdvantageA (twoHybrid m₀ m₁) (twoIdeal m₀ m₁) A

Advantage bound: Real to Ideal via Hybrid

N-Instance Generalization

For the general case with n instances, we use a simpler fixed-size structure.

@[reducible, inline]

abbrev CatCrypt.Examples.DeepHybrid.ThreeOutput : Type

Three-instance output type

Equations

• CatCrypt.Examples.DeepHybrid.ThreeOutput = (CatCrypt.Examples.DeepHybrid.Word × CatCrypt.Examples.DeepHybrid.Word × CatCrypt.Examples.DeepHybrid.Word)

noncomputable def CatCrypt.Examples.DeepHybrid.threeHybrid (i : ℕ) (m₀ m₁ m₂ : Word) : Core.SPComp ThreeOutput

Hybrid games for 3 instances

Equations

• One or more equations did not get rendered due to their size.

theorem CatCrypt.Examples.DeepHybrid.threeHybrid_0_is_real (m₀ m₁ m₂ : Word) : threeHybrid 0 m₀ m₁ m₂ = do let c₀ ← realOracle m₀ let c₁ ← realOracle m₁ let c₂ ← realOracle m₂ Core.SPComp.pure (c₀, c₁, c₂)

Hybrid 0 = all real

theorem CatCrypt.Examples.DeepHybrid.threeHybrid_3_is_ideal (m₀ m₁ m₂ : Word) : threeHybrid 3 m₀ m₁ m₂ = do let c₀ ← idealOracle m₀ let c₁ ← idealOracle m₁ let c₂ ← idealOracle m₂ Core.SPComp.pure (c₀, c₁, c₂)

Hybrid 3 = all ideal

theorem CatCrypt.Examples.DeepHybrid.three_instance_triangle (m₀ m₁ m₂ : Word) (A : ThreeOutput → Core.SPComp Bool) : Crypto.AdvantageA (threeHybrid 0 m₀ m₁ m₂) (threeHybrid 3 m₀ m₁ m₂) A ≤ Crypto.AdvantageA (threeHybrid 0 m₀ m₁ m₂) (threeHybrid 1 m₀ m₁ m₂) A + Crypto.AdvantageA (threeHybrid 1 m₀ m₁ m₂) (threeHybrid 2 m₀ m₁ m₂) A + Crypto.AdvantageA (threeHybrid 2 m₀ m₁ m₂) (threeHybrid 3 m₀ m₁ m₂) A

Triangle bound for 3-instance case

Perfect Security for XOR Encryption

For XOR encryption, each single step has zero advantage, so the total advantage is also zero.

theorem CatCrypt.Examples.DeepHybrid.realOracle_eq_idealOracle (m : Word) : realOracle m = idealOracle m

Key lemma: realOracle and idealOracle produce identical distributions.

Since XOR with a uniform random key produces a uniform distribution, both oracles sample from the same distribution. This means all hybrid games are actually identical!

theorem CatCrypt.Examples.DeepHybrid.threeHybrid_simpl (i : ℕ) (m₀ m₁ m₂ : Word) : threeHybrid i m₀ m₁ m₂ = do let c₀ ← idealOracle m₀ let c₁ ← idealOracle m₁ let c₂ ← idealOracle m₂ Core.SPComp.pure (c₀, c₁, c₂)

All threeHybrid games simplify to the same computation.

Since realOracle = idealOracle for XOR encryption, all branches of the hybrid game produce the same result.

theorem CatCrypt.Examples.DeepHybrid.hybrid_step_zero_advantage (i : ℕ) (m₀ m₁ m₂ : Word) (A : ThreeOutput → Core.SPComp Bool) (_hi : i < 3) : Crypto.AdvantageA (threeHybrid i m₀ m₁ m₂) (threeHybrid (i + 1) m₀ m₁ m₂) A ≤ 0

Key observation: Each step in a hybrid ladder for XOR has zero advantage.

This is because realOracle and idealOracle produce identical distributions (both sample uniformly). Therefore consecutive hybrids are actually the same game, giving advantage = 0.

Summary

This file demonstrates the generic hybrid argument pattern:

Structure

1. Single-Instance Security: Prove real and ideal oracles are indistinguishable

   • single_oracle_coupling: XOR encryption couples perfectly with random
   • single_oracle_zero_advantage: Zero distinguishing advantage

2. Hybrid Ladder: Define intermediate games

   • selectOracle i pos: Uses ideal for pos < i, real for pos >= i
   • twoHybrid, threeHybrid: Concrete hybrid game instances

3. Step Bounds: Each adjacent step bounded by single-instance advantage

   • step_0_1_coupling: First step preserves second component
   • step_1_2_coupling: Second step preserves first component

4. Triangle Inequality: Total advantage bounded by sum of steps

   • two_instance_advantage_bound: Concrete 2-instance bound
   • three_instance_triangle: Concrete 3-instance bound

ProofFrog Comparison

ProofFrog	This file
Auto hybrid generation	Explicit selectOracle
Z3 for equivalence	rHoare + coupling
~50 lines	~350 lines
Fast iteration	Machine-checked

Key Insight

For XOR encryption (or any perfectly secure primitive):

• Single-instance advantage = 0
• n × 0 = 0
• Therefore n-fold security is also perfect

For computationally secure primitives, the bound would be:

• Adv(Real, Ideal) ≤ n × Adv(SingleReal, SingleIdeal)

This is the standard "n-factor security loss" of hybrid arguments.

Proved results

• single_oracle_coupling: bijection coupling of one XOR encryption with a uniform ciphertext
• single_oracle_zero_advantage: advantage 0, from the coupling
• step_0_1_coupling, step_1_2_coupling: the two-instance step couplings
• two_instance_advantage_bound: triangle inequality over the two-instance ladder
• three_instance_triangle: triangle inequality over the three-instance ladder
• hybrid_step_zero_advantage: every three-instance step has advantage 0