Asymmetric Encryption Schemes: IND-CPA Oracle Games

This file contains the oracle-based IND-CPA interface together with the counted left/right hybrid machinery used in generic multi-query proofs.

def AsymmEncAlg.IND_CPA_oracleSpec {M PK SK C : Type} (_encAlg : AsymmEncAlg ProbComp M PK SK C) : OracleSpec (ℕ ⊕ M × M)

Oracle-based multi-query IND-CPA game. The adversary gets oracle access to an encryption oracle that encrypts one of two challenge messages depending on a hidden bit.

def AsymmEncAlg.IND_CPA_adversary {M PK SK C : Type} (encAlg : AsymmEncAlg ProbComp M PK SK C) : Type

An oracle IND-CPA adversary chooses challenge messages by querying the LR oracle and returns a final Boolean guess.

def AsymmEncAlg.IND_CPA_adversary.MakesAtMostQueries {M PK SK C : Type} {encAlg : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg.IND_CPA_adversary) (q : ℕ) : Prop

An IND-CPA adversary MakesAtMostQueries q when it issues at most q total fresh queries to the challenge oracle, regardless of public key. Uniform-sampling queries are unrestricted.

@[reducible, inline]

abbrev AsymmEncAlg.IND_CPA_Cache {M PK SK C : Type} (_encAlg : AsymmEncAlg ProbComp M PK SK C) : Type

Cache state for the cached left/right oracle implementations.

def AsymmEncAlg.IND_CPA_queryImpl' {M PK SK C : Type} [DecidableEq M] (encAlg : AsymmEncAlg ProbComp M PK SK C) (pk : PK) (b : Bool) : QueryImpl encAlg.IND_CPA_oracleSpec (StateT encAlg.IND_CPA_Cache ProbComp)

Cached LR-oracle implementation for IND-CPA: repeated challenge queries are answered from the cache, and fresh ones encrypt the selected branch.

def AsymmEncAlg.IND_CPA_experiment {M PK SK C : Type} [DecidableEq M] {encAlg : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg.IND_CPA_adversary) : ProbComp Bool

Oracle IND-CPA experiment with caching on the LR oracle.

def AsymmEncAlg.IND_CPA_LR_experiment {M PK SK C : Type} [DecidableEq M] {encAlg : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg.IND_CPA_adversary) (b : Bool) : ProbComp Bool

Deterministic left/right endpoint IND-CPA experiment: all fresh LR queries use the branch selected by b, and the adversary's final guess is returned directly.

@[reducible, inline]

abbrev AsymmEncAlg.IND_CPA_CountedState {M PK SK C : Type} (_encAlg : AsymmEncAlg ProbComp M PK SK C) : Type

Cached IND-CPA state extended with a query counter.

def AsymmEncAlg.IND_CPA_challengeOracle'_counted {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (pk : PK) (b : Bool) : QueryImpl (OracleSpec.ofFn fun (x : M × M) => C) (StateT encAlg'.IND_CPA_CountedState ProbComp)

The real IND-CPA challenge oracle, but with an explicit counter that increments on cache misses.

def AsymmEncAlg.IND_CPA_queryImpl'_counted {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (pk : PK) (b : Bool) : QueryImpl encAlg'.IND_CPA_oracleSpec (StateT encAlg'.IND_CPA_CountedState ProbComp)

The cached real IND-CPA query implementation, extended with an explicit query counter.

def AsymmEncAlg.IND_CPA_hybridChallengeOracleLR_counted {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (pk : PK) (leftUntil : ℕ) : QueryImpl (OracleSpec.ofFn fun (x : M × M) => C) (StateT encAlg'.IND_CPA_CountedState ProbComp)

Counted left/right hybrid oracle: the first leftUntil fresh LR queries use the left message and all later fresh queries use the right message. Repeated queries are answered from the cache.

def AsymmEncAlg.IND_CPA_queryImpl_hybridLR_counted {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (pk : PK) (leftUntil : ℕ) : QueryImpl encAlg'.IND_CPA_oracleSpec (StateT encAlg'.IND_CPA_CountedState ProbComp)

Full counted query implementation for the generic left-prefix/right-suffix hybrid family.

def AsymmEncAlg.IND_CPA_LR_hybridGame {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg'.IND_CPA_adversary) (leftUntil : ℕ) : ProbComp Bool

The generic left/right hybrid family: the first leftUntil fresh LR queries use the left branch, and all later fresh queries use the right branch.

theorem AsymmEncAlg.IND_CPA_queryImpl'_counted_counter_le_succ {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (pk : PK) (b : Bool) (t : encAlg'.IND_CPA_oracleSpec.Domain) (st : encAlg'.IND_CPA_CountedState) (p : encAlg'.IND_CPA_oracleSpec.Range t × encAlg'.IND_CPA_CountedState) (hp : p ∈ support ((IND_CPA_queryImpl'_counted pk b t).run st)) : p.2.2 ≤ st.2 + 1

One-step counter monotonicity for the counted real IND-CPA implementation.

theorem AsymmEncAlg.IND_CPA_queryImpl'_counted_proj_eq_queryImpl' {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (pk : PK) (b : Bool) (t : encAlg'.IND_CPA_oracleSpec.Domain) (st : encAlg'.IND_CPA_CountedState) : Prod.map id Prod.fst <$> (IND_CPA_queryImpl'_counted pk b t).run st = (encAlg'.IND_CPA_queryImpl' pk b t).run st.1

Projecting away the counter from the counted real IND-CPA implementation recovers the ordinary cached real implementation.

theorem AsymmEncAlg.IND_CPA_queryImpl_hybridLR_counted_proj_eq_queryImpl'_false {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (pk : PK) (t : encAlg'.IND_CPA_oracleSpec.Domain) (st : encAlg'.IND_CPA_CountedState) : Prod.map id Prod.fst <$> (IND_CPA_queryImpl_hybridLR_counted pk 0 t).run st = (encAlg'.IND_CPA_queryImpl' pk false t).run st.1

The leftUntil = 0 left/right hybrid is exactly the all-right endpoint game once the counter is projected away.

theorem AsymmEncAlg.IND_CPA_run'_evalDist_eq_queryImpl'_of_bounded_eq {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (implCounted : PK → Bool → ℕ → QueryImpl encAlg'.IND_CPA_oracleSpec (StateT encAlg'.IND_CPA_CountedState ProbComp)) (hsame : ∀ (pk : PK) (b : Bool) (realUntil : ℕ) (t : encAlg'.IND_CPA_oracleSpec.Domain) (st : encAlg'.IND_CPA_CountedState), (match t with | Sum.inl val => True | Sum.inr val => st.2 < realUntil) → (IND_CPA_queryImpl'_counted pk b t).run st = (implCounted pk b realUntil t).run st) (pk : PK) (b : Bool) (q : ℕ) {α : Type} (comp : OracleComp encAlg'.IND_CPA_oracleSpec α) (budget : ℕ) (hbound : comp.IsQueryBound budget (fun (t : ℕ ⊕ M × M) (n : ℕ) => match t with | Sum.inl val => True | Sum.inr val => 0 < n) fun (t : ℕ ⊕ M × M) (n : ℕ) => match t with | Sum.inl val => n | Sum.inr val => n - 1) (cache : (OracleSpec.ofFn fun (x : M × M) => C).QueryCache) (n : ℕ) (hn : n + budget ≤ q) : evalDist ((simulateQ (implCounted pk b q) comp).run' (cache, n)) = evalDist ((simulateQ (encAlg'.IND_CPA_queryImpl' pk b) comp).run' cache)

If a counted IND-CPA hybrid implementation agrees with the counted real implementation through the first q fresh LR queries, then any adversary making at most q LR queries sees the same output distribution as in the real IND-CPA game.

theorem AsymmEncAlg.IND_CPA_countedGame_eq_game_of_MakesAtMostQueries {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (implCounted : PK → Bool → ℕ → QueryImpl encAlg'.IND_CPA_oracleSpec (StateT encAlg'.IND_CPA_CountedState ProbComp)) (hsame : ∀ (pk : PK) (b : Bool) (realUntil : ℕ) (t : encAlg'.IND_CPA_oracleSpec.Domain) (st : encAlg'.IND_CPA_CountedState), (match t with | Sum.inl val => True | Sum.inr val => st.2 < realUntil) → (IND_CPA_queryImpl'_counted pk b t).run st = (implCounted pk b realUntil t).run st) (adversary : encAlg'.IND_CPA_adversary) (q : ℕ) (hq : adversary.MakesAtMostQueries q) : Pr[= true | do let b ← $ᵗ Bool let __discr ← encAlg'.keygen match __discr with | (pk, _sk) => do let b' ← (simulateQ (implCounted pk b q) (adversary pk)).run' (∅, 0) pure (b == b')].toReal = Pr[= true | IND_CPA_experiment adversary].toReal

A counted IND-CPA hybrid game agrees with the real IND-CPA experiment whenever the hybrid implementation matches the real counted implementation on all states that stay below the query budget.

noncomputable def AsymmEncAlg.IND_CPA_advantage {M PK SK C : Type} [DecidableEq M] {encAlg : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg.IND_CPA_adversary) : ENNReal

ℝ≥0∞-valued IND-CPA signed advantage, aligned with the oracle IND-CPA experiment.

theorem AsymmEncAlg.IND_CPA_LR_hybridGame_zero_evalDist_eq_right {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg'.IND_CPA_adversary) : evalDist (IND_CPA_LR_hybridGame adversary 0) = evalDist (IND_CPA_LR_experiment adversary false)

The leftUntil = 0 LR-hybrid is the all-right endpoint game.

theorem AsymmEncAlg.IND_CPA_LR_hybridGame_q_evalDist_eq_left_of_MakesAtMostQueries {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg'.IND_CPA_adversary) (q : ℕ) (hq : adversary.MakesAtMostQueries q) : evalDist (IND_CPA_LR_hybridGame adversary q) = evalDist (IND_CPA_LR_experiment adversary true)

If an adversary makes at most q fresh LR queries, then the leftUntil = q LR-hybrid is the all-left endpoint game.

theorem AsymmEncAlg.IND_CPA_LR_hybridGame_zero_probOutput_eq_right {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg'.IND_CPA_adversary) : Pr[= true | IND_CPA_LR_hybridGame adversary 0] = Pr[= true | IND_CPA_LR_experiment adversary false]

The leftUntil = 0 LR-hybrid has the same success probability as the all-right endpoint.

theorem AsymmEncAlg.IND_CPA_LR_hybridGame_q_probOutput_eq_left_of_MakesAtMostQueries {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg'.IND_CPA_adversary) (q : ℕ) (hq : adversary.MakesAtMostQueries q) : Pr[= true | IND_CPA_LR_hybridGame adversary q] = Pr[= true | IND_CPA_LR_experiment adversary true]

If an adversary makes at most q fresh LR queries, then the leftUntil = q LR-hybrid has the same success probability as the all-left endpoint.

noncomputable def AsymmEncAlg.IND_CPA_signedAdvantageReal {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg'.IND_CPA_adversary) : ℝ

Signed real IND-CPA advantage Pr[win] - 1/2 for the oracle IND-CPA experiment.

theorem AsymmEncAlg.IND_CPA_signedAdvantageReal_eq_lrDiff_half {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg'.IND_CPA_adversary) : IND_CPA_signedAdvantageReal adversary = (Pr[= true | IND_CPA_LR_experiment adversary true].toReal - Pr[= true | IND_CPA_LR_experiment adversary false].toReal) / 2

The signed real IND-CPA advantage is half the left/right endpoint gap.

theorem AsymmEncAlg.IND_CPA_signedAdvantageReal_eq_sum_hybridDiff {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg'.IND_CPA_adversary) (q : ℕ) (games : ℕ → ProbComp Bool) (h0 : Pr[= true | games 0].toReal = Pr[= true | IND_CPA_experiment adversary].toReal) (hq : Pr[= true | games q].toReal = 1 / 2) : IND_CPA_signedAdvantageReal adversary = ∑ i ∈ Finset.range q, (Pr[= true | games i].toReal - Pr[= true | games (i + 1)].toReal)

Generic telescoping identity for multi-query game-hopping: if games 0 is the target IND-CPA experiment and games q has success probability 1/2, then the signed IND-CPA advantage is the sum of adjacent hybrid differences.

theorem AsymmEncAlg.IND_CPA_abs_signedAdvantageReal_le_sum_hybridDiff_abs {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg'.IND_CPA_adversary) (q : ℕ) (games : ℕ → ProbComp Bool) (h0 : Pr[= true | games 0].toReal = Pr[= true | IND_CPA_experiment adversary].toReal) (hq : Pr[= true | games q].toReal = 1 / 2) : |IND_CPA_signedAdvantageReal adversary| ≤ ∑ i ∈ Finset.range q, |Pr[= true | games i].toReal - Pr[= true | games (i + 1)].toReal|

Generic multi-query bound: absolute signed IND-CPA advantage is at most the sum of absolute adjacent hybrid gaps.

theorem AsymmEncAlg.IND_CPA_advantage_toReal_le_abs_signedAdvantageReal {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (adversary : encAlg'.IND_CPA_adversary) : (IND_CPA_advantage adversary).toReal ≤ |IND_CPA_signedAdvantageReal adversary|

Compatibility bridge to the existing IND_CPA_advantage API: the toReal of the ℝ≥0∞ signed advantage is bounded by the absolute signed real advantage.

theorem AsymmEncAlg.IND_CPA_hybridLR_counted_run_eq_of_ge {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (pk : PK) (k : ℕ) (t : encAlg'.IND_CPA_oracleSpec.Domain) (st : encAlg'.IND_CPA_CountedState) (hst : st.2 ≥ k + 1) : (IND_CPA_queryImpl_hybridLR_counted pk k t).run st = (IND_CPA_queryImpl_hybridLR_counted pk (k + 1) t).run st

When the counter is above both thresholds, two hybrid LR counted oracles agree pointwise.

theorem AsymmEncAlg.IND_CPA_hybridLR_counted_counter_le {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (pk : PK) (k : ℕ) (t : encAlg'.IND_CPA_oracleSpec.Domain) (st : encAlg'.IND_CPA_CountedState) (p : encAlg'.IND_CPA_oracleSpec.Range t × encAlg'.IND_CPA_CountedState) (hp : p ∈ support ((IND_CPA_queryImpl_hybridLR_counted pk k t).run st)) : st.2 ≤ p.2.2

Counter monotonicity for the hybrid LR counted oracle: the counter never decreases.

theorem AsymmEncAlg.IND_CPA_hybridChallengeOracleLR_counted_run_none {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (pk : PK) (k : ℕ) (mm : M × M) (st : encAlg'.IND_CPA_CountedState) (hcache : st.1 mm = none) : (IND_CPA_hybridChallengeOracleLR_counted pk k mm).run st = do let c ← encAlg'.encrypt pk (if st.2 < k then mm.1 else mm.2) pure (c, OracleSpec.QueryCache.cacheQuery st.1 mm c, st.2 + 1)

Behavior of the hybrid challenge oracle on a cache miss.

theorem AsymmEncAlg.IND_CPA_hybridChallengeOracleLR_counted_run_some {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} (pk : PK) (k : ℕ) (mm : M × M) (c : C) (st : encAlg'.IND_CPA_CountedState) (hcache : st.1 mm = some c) : (IND_CPA_hybridChallengeOracleLR_counted pk k mm).run st = pure (c, st)

Behavior of the hybrid challenge oracle on a cache hit.