Game-Based Security Proof Methodology

Overview

This skill provides systematic guidance for constructing security proofs using the sequence-of-games technique. The methodology transforms complex security arguments into manageable sequences of small, analyzable transitions between games.

Core Principle: Security proofs proceed by constructing Game 0 (original attack game), then transforming it through Games 1, 2, ..., n until reaching a game where the target probability is easily computed. Each transition changes only one aspect, making analysis tractable.

When to Use This Skill

• Proving semantic security (IND-CPA, IND-CCA) of encryption schemes
• Proving unforgeability (EUF-CMA) of signatures/MACs
• Proving pseudorandomness of PRFs/PRPs
• Reducing security to computational assumptions (DDH, CDH, RSA, LWE)
• Writing formal proofs for cryptography papers

Proof Structure Template

1. Setup Phase

Define the attack game (Game 0) precisely:

Game 0:
  Challenger computes keys: (pk, sk) ← KeyGen()
  Challenger selects: b ←$ {0,1}
  Adversary A interacts with Challenger (queries, challenges)
  Adversary outputs: b̂
  Define S₀ := event that b = b̂
  Adversary's advantage: |Pr[S₀] - 1/2|

2. Game Sequence

For each transition Game i → Game i+1, use exactly ONE of three types:

Type 1: Indistinguishability Transition

• Make a small change that, if detected, breaks a computational assumption
• Construct distinguisher D that interpolates between games
• Conclude: |Pr[Sᵢ] - Pr[Sᵢ₊₁]| = ε_assumption

Type 2: Failure Event Transition (Difference Lemma)

• Games proceed identically unless failure event F occurs
• Ensure: Sᵢ ∧ ¬F ⟺ Sᵢ₊₁ ∧ ¬F
• Apply Difference Lemma: |Pr[Sᵢ] - Pr[Sᵢ₊₁]| ≤ Pr[F]
• Bound Pr[F] (via assumption or information-theoretic argument)

Type 3: Bridging Step

• Purely conceptual restatement (e.g., "lazy sampling" / "gnome" technique)
• Pr[Sᵢ] = Pr[Sᵢ₊₁] exactly

3. Final Game Analysis

In Game n, show that Pr[Sₙ] equals the target probability (typically 1/2 for encryption, or 0 for unforgeability).

4. Advantage Bound

Combine all transitions:

Adv[A] = |Pr[S₀] - target| ≤ Σ |Pr[Sᵢ] - Pr[Sᵢ₊₁]| ≤ ε₁ + ε₂ + ... + εₙ

The Difference Lemma

Lemma (Difference Lemma): Let A, B, F be events in a probability space. If A ∧ ¬F ⟺ B ∧ ¬F, then |Pr[A] - Pr[B]| ≤ Pr[F].

Proof sketch: |Pr[A] - Pr[B]| = |Pr[A∧F] + Pr[A∧¬F] - Pr[B∧F] - Pr[B∧¬F]| = |Pr[A∧F] - Pr[B∧F]| (since Pr[A∧¬F] = Pr[B∧¬F]) ≤ Pr[F]

Critical practice: Define games on the same underlying probability space so failure event F is literally one event, not corresponding events across spaces.

Key Techniques

Lazy Sampling ("Gnome" Technique)

Replace eager random function evaluation with lazy/on-demand sampling:

# Eager (conceptual random function f)
y ← f(x)

# Lazy (equivalent "gnome" implementation)
if x ∈ Table then y ← Table[x]
else Y ←$ Range; Table[x] ← Y; y ← Y

Use this to bridge between "random function" and explicit table-based computation.

Forgetful Gnome

After lazy sampling setup, remove consistency checks to create independent random variables:

# Faithful gnome (with checks)
if x = xⱼ for some j < i then y ← yⱼ else y ← Yᵢ

# Forgetful gnome (no checks)  
y ← Yᵢ

Games differ only when collision occurs (failure event).

One-Time Pad Argument

When a value h is used only once as h ⊕ m:

• If h is uniformly random and independent of m
• Then h ⊕ m is uniformly random regardless of m
• Adversary learns nothing about which message was encrypted
• Conclude: Pr[b = b̂] = 1/2

Common Proof Patterns

Writing Guidelines

1. Explicit game descriptions: Write games algorithmically with clear notation
2. One change per transition: Each game should differ minimally from the previous
3. Label transition types: State explicitly "[This is a transition based on X]"
4. Bound immediately: After each transition, state the bound on probability difference
5. Same probability space: Keep all games on the same space when possible

Reference Files

• references/game-transitions.md: Detailed explanation of three transition types with examples
• references/proof-templates.md: Complete proof templates for common schemes
• references/latex-macros.md: LaTeX macros for writing game-based proofs

Quick Reference: Notation