game-based-security-proof

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].

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

Scheme Type	Typical Game Sequence
Public-key encryption	Game 0 → (DDH/CDH transition) → ... → one-time-pad game
PRF security	Game 0 → (replace PRF with random) → lazy sampling → forgetful gnome
PRP security	Similar to PRF, bound RF/RP distinguishing advantage
CCA encryption	Game 0 → (reject all decryption queries) → semantic security game
Random oracle	Game 0 → (program random oracle) → reduction to CDH/other

Writing Guidelines

Explicit game descriptions: Write games algorithmically with clear notation
One change per transition: Each game should differ minimally from the previous
Label transition types: State explicitly "[This is a transition based on X]"
Bound immediately: After each transition, state the bound on probability difference
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

Symbol	Meaning
x ←$ S	Sample x uniformly from set S
A^O()	Adversary A with oracle access to O
Pr[E]	Probability of event E
negl(λ)	Negligible function in security parameter λ
Sᵢ	Success event in Game i
F	Failure event
ε	Advantage bound (should be negligible)