Documentation

VCVio.CryptoFoundations.AsymmEncAlg.INDCPA.GenericLift

Asymmetric Encryption Schemes: Generic IND-CPA Lifts #

This file contains the generic step-adversary extraction and the planned one-time-to-many-time IND-CPA lift.

source
def AsymmEncAlg.IND_CPA_stepAdversary {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} [Inhabited M] (adversary : encAlg'.IND_CPA_adversary) (k : ℕ) :
encAlg'.IND_CPA_Adv

Generic extraction of the one-time adversary for the k-th fresh LR query.

Instances For
    source
    theorem AsymmEncAlg.IND_CPA_stepAdversary_signedAdvantageReal_eq_hybridDiff_half {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} [Inhabited M] (adversary : encAlg'.IND_CPA_adversary) (k : ℕ) :
    encAlg'.IND_CPA_OneTime_signedAdvantageReal (IND_CPA_stepAdversary adversary k) = (Pr[= true | IND_CPA_LR_hybridGame adversary (k + 1)].toReal - Pr[= true | IND_CPA_LR_hybridGame adversary k].toReal) / 2

    Planned adjacent-gap characterization for the extracted step adversary. Once IND_CPA_stepAdversary_game_eq_hybridBranch is proved, this is just the one-time analogue of IND_CPA_signedAdvantageReal_eq_lrDiff_half.

    source
    theorem AsymmEncAlg.IND_CPA_advantage_toReal_le_sum_step_signedAdvantageReal_abs {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} [Inhabited M] (adversary : encAlg'.IND_CPA_adversary) (q : ℕ) (hq : adversary.MakesAtMostQueries q) :
    (IND_CPA_advantage adversary).toReal ≤ ∑ k ∈ Finset.range q, |encAlg'.IND_CPA_OneTime_signedAdvantageReal (IND_CPA_stepAdversary adversary k)|

    Planned generic one-time-to-many-time lift: bounded multi-query IND-CPA advantage is at most the sum of the extracted one-time signed advantages over the first q fresh LR queries.

    source
    theorem AsymmEncAlg.IND_CPA_advantage_toReal_le_q_mul_of_oneTime_signedAdvantageReal_bound {M PK SK C : Type} [DecidableEq M] {encAlg' : AsymmEncAlg ProbComp M PK SK C} [Inhabited M] (adversary : encAlg'.IND_CPA_adversary) (q : ℕ) (ε : ℝ) (hq : adversary.MakesAtMostQueries q) (hstep : ∀ (adv : encAlg'.IND_CPA_Adv), |encAlg'.IND_CPA_OneTime_signedAdvantageReal adv| ≤ ε) :
    (IND_CPA_advantage adversary).toReal ≤ ↑q * ε

    Planned uniform corollary of the generic lift. If every extracted one-time adversary has signed real advantage at most ε, then any q-query oracle adversary has IND-CPA advantage at most q * ε.