Chosen-ciphertext security for public-key encryption (1CCA / IND-CCA2)

This module defines the single-challenge adaptive chosen-ciphertext security experiment (1CCA, also called IND-CCA2) for public-key encryption over an arbitrary message type Msg and decryption output type Out, following Boneh and Shoup, Section 12.1, Attack Game 12.1 and Definition 12.2, printed pp. 467–469.

Source Statements ([BS23], Section 12.1, printed pp. 467–469)

Verbatim from [BS23], Section 12.1 (printed pp. 467–468):

Attack Game 12.1 (CCA security). For a given public-key encryption scheme $\mathcal{E} = (G, E, D)$, defined over $(\mathcal{M}, \mathcal{C})$, and for a given adversary $\mathcal{A}$, we define two experiments. Experiment $b$ ($b = 0, 1$):

• The challenger computes $(pk, sk) \xleftarrow{R} G()$ and sends $pk$ to the adversary.
• $\mathcal{A}$ then makes a series of queries to the challenger. Each query can be one of two types:
  • Encryption query: for $i = 1, 2, \ldots$, the $i$th encryption query consists of a pair of messages $(m_{i0}, m_{i1}) \in \mathcal{M}^2$, of the same length. The challenger computes $c_i \xleftarrow{R} E(pk, m_{ib})$ and sends $c_i$ to $\mathcal{A}$.
  • Decryption query: for $j = 1, 2, \ldots$, the $j$th decryption query consists of a ciphertext $\hat{c}_j \in \mathcal{C}$ that is not among the responses to the previous encryption queries, i.e., $$\hat{c}_j \notin \{c_1, c_2, \ldots\}.$$ The challenger computes $\hat{m}_j \leftarrow D(sk, \hat{c}_j)$, and sends $\hat{m}_j$ to $\mathcal{A}$.
• At the end of the game, the adversary outputs a bit $\hat{b} \in \{0, 1\}$.

Let $W_b$ be the event that $\mathcal{A}$ outputs $1$ in Experiment $b$ and define $\mathcal{A}$'s advantage with respect to $\mathcal{E}$ as $$\text{CCAadv}[\mathcal{A}, \mathcal{E}] := |\Pr[W_0] - \Pr[W_1]|.$$

Definition 12.1 (CCA Security). A public-key encryption scheme $\mathcal{E}$ is called semantically secure against a chosen ciphertext attack, or simply CCA secure, if for all efficient adversaries $\mathcal{A}$, the value $\text{CCAadv}[\mathcal{A}, \mathcal{E}]$ is negligible.

Just as we did in the symmetric-key setting, we can consider a restricted attack game in which the adversary makes only a single encryption query:

Definition 12.2 (1CCA security). In Attack Game 12.1, if the adversary $\mathcal{A}$ is restricted to making a single encryption query, we denote its advantage by $\text{1CCAadv}[\mathcal{A}, \mathcal{E}]$. A public-key encryption scheme $\mathcal{E}$ is one-time semantically secure against chosen ciphertext attack, or simply, 1CCA secure, if for all efficient adversaries $\mathcal{A}$, the value $\text{1CCAadv}[\mathcal{A}, \mathcal{E}]$ is negligible.

And the two-phase decomposition of the 1CCA experiment (printed pp. 468–469):

Initialization phase: the challenger generates $(pk, sk) \xleftarrow{R} G()$ and sends $pk$ to the adversary. Phase 1: the adversary submits a series of decryption queries to the challenger; each such query is a ciphertext $\hat{c} \in \mathcal{C}$, to which the challenger responds with $\hat{m} \leftarrow D(sk, \hat{c})$. Encryption query: the adversary submits a single encryption query $(m_0, m_1)$ to the challenger; in Experiment $b$ (where $b = 0, 1$), the challenger responds with $c \xleftarrow{R} E(pk, m_b)$. Phase 2: the adversary again submits a series of decryption queries to the challenger; each such query is a ciphertext $\hat{c} \in \mathcal{C}$, subject to the restriction that $\hat{c} \ne c$, to which the challenger responds with $\hat{m} \leftarrow D(sk, \hat{c})$. Finish: at the end of the game, the adversary outputs a bit $\hat{b} \in \{0, 1\}$.

Scope and Specializations

• Single-challenge 1CCA (Definition 12.2) vs. symmetric SymmetricCipher.INDCCA (Definition 9.5): CCA2AdversaryOf Msg, cca2Game, and INDCCA2Of formalize the single-challenge public-key 1CCA experiment (Definition 12.2, printed p. 468). Unlike SymmetricCipher.INDCCA and SymmetricCipher.CCAAdversary in Complexity/Crypto/Computational/Encryption/Authenticated.lean (which model multi-query symmetric-key CCA, Definition 9.5, using a single-stage adversary with a two-channel encryption/decryption oracle Operation = Bool), a public-key 1CCA adversary receives the public key pk directly and interacts with a single-channel decryption oracle (Operation = Unit) across two stages (choose and guess) around one challenge encryption. Because anyone can encrypt under pk, public-key 1CCA is equivalent to multi-challenge CCA by a hybrid argument ([BS23], Theorem 12.1, printed p. 468); that multi-challenge equivalence is not formalized here.
• Phase 2 challenge-rejection convention: in Phase 2, querying the challenge ciphertext (request.2 == ct) returns [] = encOption encOut none (the encoding of decryption rejection none) rather than syntactically restricting the oracle domain to ĉ ≠ c. Because the adversary is given ct as input to guess and could simulate the constant [] reply on ct itself, this convention is equivalent to forbidding ĉ = c and matches SymmetricCipher.ccaOracle in Complexity/Crypto/Computational/Encryption/Authenticated.lean.
• No associated data ($\mathcal{D} = \mathrm{Unit}$): encryption and decryption queries carry no separate associated-data argument (corresponding to $\mathcal{D} = \mathrm{Unit}$ in schemes with associated data such as Exercise 12.27).
• Generic message and output types with challenge-pair admissibility: CCA2AdversaryOf (Msg : Type) is generic in the challenge message type Msg (CCA2Adversary specializes to Bool, and WordCCA2Adversary to List Bool). cca2GameOn and INDCCA2On parameterize the experiment by a challenge-pair admissibility predicate valid : ℕ → List Bool → Msg → Msg → Bool (returning false in both experiments when valid n pk m₀ m₁ = false), while cca2Game and INDCCA2Of specialize to fun _ _ _ _ => true for fixed-length message spaces (such as Bool) and WordINDCCA2 specializes to Attack Game 12.1's equal-length rule fun _ _ m₀ m₁ => m₀.length == m₁.length.

Main definitions

• Cslib.Crypto.Encryption.CCA2AdversaryOf, Cslib.Crypto.Encryption.CCA2Adversary, Cslib.Crypto.Encryption.WordCCA2Adversary: two-stage 1CCA adversaries with WordOracleComp Unit decryption-oracle access in Phase 1 (choose) and Phase 2 (guess).
• Cslib.Crypto.Encryption.CCA2AdversaryOf.IsPPT, Cslib.Crypto.Encryption.CCA2AdversaryOf.IsQueryBounded: uniform strict oracle PPT admissibility and per-stage decryption-query bounds.
• Cslib.Crypto.Encryption.cca2Phase1Oracle, Cslib.Crypto.Encryption.cca2Phase2Oracle, Cslib.Crypto.Encryption.cca2GameOn, Cslib.Crypto.Encryption.cca2Game: Phase 1 and Phase 2 decryption oracles and the 1CCA experiment (with and without an explicit challenge-pair admissibility guard).
• Cslib.Crypto.Encryption.INDCCA2On, Cslib.Crypto.Encryption.INDCCA2Of, Cslib.Crypto.Encryption.INDCCA2, Cslib.Crypto.Encryption.WordINDCCA2: single-challenge 1CCA security (Definition 12.2).
• Cslib.Crypto.Encryption.CCA2AdversaryOf.restrict: embedding of an adversary for the admissibility-restricted cca2GameOn valid inside the unrestricted cca2Game.
• Cslib.Crypto.Encryption.CCA2AdversaryOf.ofCPA, Cslib.Crypto.Encryption.CCA2Adversary.ofCPA: embedding of a chosen-plaintext AdversaryOf Msg as a 0-query CCA2AdversaryOf Msg.

Main results

• Cslib.Crypto.Encryption.CCA2AdversaryOf.IsPPT.query_bounds: polynomial query and saved-state length bounds for every strict oracle PPT CCA2AdversaryOf Msg.
• Cslib.Crypto.Encryption.isPPTOn_run_cca2Phase1Oracle, Cslib.Crypto.Encryption.isPPTOn_run_cca2Phase2Oracle, Cslib.Crypto.Encryption.isPPTOn_cca2GameOn, Cslib.Crypto.Encryption.isPPTOn_cca2Game: closed strict PPT compilation of Phase 1, Phase 2, and the complete 1CCA experiment via IsOraclePPTOn.run_interpret_preprocess.
• Cslib.Crypto.Encryption.eval_cca2Game_restrict, Cslib.Crypto.Encryption.CCA2AdversaryOf.IsPPT.restrict, Cslib.Crypto.Encryption.INDCCA2Of.indcca2On, Cslib.Crypto.Encryption.INDCCA2Of.wordINDCCA2: unrestricted 1CCA security (INDCCA2Of) implies admissibility-restricted 1CCA security (INDCCA2On, including WordINDCCA2).
• Cslib.Crypto.Encryption.CCA2AdversaryOf.isPPT_ofCPA, Cslib.Crypto.Encryption.CCA2AdversaryOf.isQueryBounded_ofCPA, Cslib.Crypto.Encryption.eval_cca2GameOn_ofCPA, Cslib.Crypto.Encryption.eval_cca2Game_ofCPA, Cslib.Crypto.Encryption.INDCCA2On.indcpaOn, Cslib.Crypto.Encryption.INDCCA2Of.indcpaOf, Cslib.Crypto.Encryption.INDCCA2Of.indcpa, Cslib.Crypto.Encryption.INDCCA2.indcpa, Cslib.Crypto.Encryption.WordINDCCA2.wordINDCPA: 1CCA security implies IND-CPA security under any challenge-pair admissibility predicate.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 12.1 (Attack Game 12.1, Definitions 12.1–12.2, printed pp. 467–469).

structure Cslib.Crypto.Encryption.CCA2AdversaryOf (Msg : Type) : Type

A single-challenge adaptive chosen-ciphertext (1CCA, [BS23], Section 12.1, Attack Game 12.1 and Definition 12.2, printed pp. 467–469) adversary over message space Msg. Both stages have access to the single-channel decryption oracle (Operation = Unit).

• choose : ℕ → List Bool → Probability.WordOracleComp Unit ((Msg × Msg) × List Bool)

  Phase 1: given the unary security parameter n and encoded public key pk, make decryption queries, choose two challenge messages (m₀, m₁) : Msg × Msg, and save a state word.

• guess : ℕ → List Bool → List Bool → Probability.WordOracleComp Unit Bool

  Phase 2: given n, the saved state word, and the challenge ciphertext ct, make decryption queries (where querying ct is rejected) and output a guess bit.

structure Cslib.Crypto.Encryption.CCA2AdversaryOf.IsPPT {Msg : Type} (encMsg : Msg ↪ List Bool) (adversary : CCA2AdversaryOf Msg) : Prop

Uniform strict oracle PPT admissibility of both stages of a CCA2AdversaryOf Msg with respect to message encoding encMsg.

• choose : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encMsg encMsg) Turing.MultiTapeTM.encBits) adversary.choose

  Phase 1 message selection is uniform strict oracle PPT on (n, pk).

• guess : Probability.IsOraclePPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBool fun (p : ℕ × List Bool × List Bool) => adversary.guess p.1 p.2.1 p.2.2

  Phase 2 guessing is uniform strict oracle PPT on (n, state, ct).

def Cslib.Crypto.Encryption.CCA2AdversaryOf.IsQueryBounded {Msg : Type} (adversary : CCA2AdversaryOf Msg) (Q₁ Q₂ : ℕ → ℕ) : Prop

Per-stage decryption-query bound (Q₁ n, Q₂ n) for a CCA2AdversaryOf Msg.

theorem Cslib.Crypto.Encryption.CCA2AdversaryOf.IsPPT.query_bounds {Msg : Type} {encMsg : Msg ↪ List Bool} {adversary : CCA2AdversaryOf Msg} (hA : IsPPT encMsg adversary) : ∃ (c₁ : ℕ) (d₁ : ℕ) (c₂ : ℕ) (d₂ : ℕ) (cs : ℕ) (ds : ℕ), (∀ (n : ℕ) (pk : List Bool), ProbOracleComp.IsQueryBounded (adversary.choose n pk) (c₁ * (n + pk.length + 2) ^ d₁)) ∧ (∀ (n : ℕ) (state ct : List Bool), ProbOracleComp.IsQueryBounded (adversary.guess n state ct) (c₂ * (n + state.length + ct.length + 2) ^ d₂)) ∧ ∀ (n : ℕ) (pk : List Bool) (State : Type) (oracle : Unit × List Bool → StateT State PMF (List Bool)) (s s' : State) (choice : (Msg × Msg) × List Bool), (choice, s') ∈ ((OracleComp.interpret (ProbOracleComp.handler (fun (m : ℕ) => StateT.lift (ProbComp.unifOracle m)) oracle) (adversary.choose n pk)).run s).support → choice.2.length ≤ cs * (n + pk.length + 2) ^ ds

Every strict oracle PPT CCA2AdversaryOf Msg has polynomial bounds on its Phase 1 queries, Phase 2 queries, and saved-state length in terms of (n, pk.length, ct.length).

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.CCA2Adversary : Type

Single-bit 1CCA adversary (Msg = Bool).

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.CCA2Adversary.IsPPT (adversary : CCA2Adversary) : Prop

Native uniform strict oracle PPT admissibility for a bit 1CCA adversary.

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.WordCCA2Adversary : Type

Bit-string 1CCA adversary (Msg = List Bool).

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.WordCCA2Adversary.IsPPT (adversary : WordCCA2Adversary) : Prop

Native uniform strict oracle PPT admissibility for a bit-string 1CCA adversary.

def Cslib.Crypto.Encryption.cca2Phase1Oracle {Out : Type} (encOut : Out ↪ List Bool) (decrypt : ℕ → List Bool → List Bool → Option Out) (n : ℕ) (sk : List Bool) (request : Unit × List Bool) : StateT Unit ProbComp (List Bool)

Phase 1 decryption oracle ([BS23], Section 12.1, Attack Game 12.1 and Definition 12.2, printed pp. 467–468): answer every decryption query request.2 with encOption encOut (decrypt n sk request.2).

def Cslib.Crypto.Encryption.cca2Phase2Oracle {Out : Type} (encOut : Out ↪ List Bool) (decrypt : ℕ → List Bool → List Bool → Option Out) (n : ℕ) (sk ct : List Bool) (request : Unit × List Bool) : StateT Unit ProbComp (List Bool)

Phase 2 decryption oracle ([BS23], Section 12.1, Attack Game 12.1 and Definition 12.2, printed pp. 467–468): reject the challenge ciphertext (request.2 == ct) with [] (encOption encOut none), and answer all other queries request.2 ≠ ct with encOption encOut (decrypt n sk request.2). Since the adversary receives ct as input to guess and can simulate the constant [] reply on ct itself, returning [] on ct is equivalent to forbidding the query ĉ = c (matching SymmetricCipher.ccaOracle in Complexity/Crypto/Computational/Encryption/Authenticated.lean).

noncomputable def Cslib.Crypto.Encryption.cca2GameOn {Msg Out : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (encOut : Out ↪ List Bool) (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)) (decrypt : ℕ → List Bool → List Bool → Option Out) (adversary : CCA2AdversaryOf Msg) (bit : Bool) (n : ℕ) : ProbComp Bool

Single-challenge 1CCA experiment ([BS23], Section 12.1, Attack Game 12.1 and Definition 12.2, printed pp. 467–468) with challenge-pair admissibility predicate valid : ℕ → List Bool → Msg → Msg → Bool: sample (pk, sk) ← keyGen n, run Phase 1 (choose) against cca2Phase1Oracle, check valid n pk m₀ m₁ (returning false in both experiments when invalid), encrypt if bit then m₁ else m₀ to obtain ct, and run Phase 2 (guess) against cca2Phase2Oracle rejecting ct.

@[reducible, inline]

noncomputable abbrev Cslib.Crypto.Encryption.cca2Game {Msg Out : Type} (encOut : Out ↪ List Bool) (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)) (decrypt : ℕ → List Bool → List Bool → Option Out) (adversary : CCA2AdversaryOf Msg) (bit : Bool) (n : ℕ) : ProbComp Bool

Unconditional single-challenge 1CCA experiment (valid := fun _ _ _ _ => true), for fixed-length message spaces Msg where every pair (m₀, m₁) : Msg × Msg is admissible.

def Cslib.Crypto.Encryption.INDCCA2On {Msg Out : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (encMsg : Msg ↪ List Bool) (encOut : Out ↪ List Bool) (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)) (decrypt : ℕ → List Bool → List Bool → Option Out) : Prop

Single-challenge 1CCA security ([BS23], Section 12.1, Definition 12.2, printed p. 468) with respect to challenge-pair admissibility predicate valid, message encoding encMsg, and decryption output encoding encOut.

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.INDCCA2Of {Msg Out : Type} (encMsg : Msg ↪ List Bool) (encOut : Out ↪ List Bool) (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)) (decrypt : ℕ → List Bool → List Bool → Option Out) : Prop

Single-challenge 1CCA security ([BS23], Section 12.1, Definition 12.2, printed p. 468) over a fixed-length message space Msg (valid := fun _ _ _ _ => true).

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.INDCCA2 (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) (decrypt : ℕ → List Bool → List Bool → Option Bool) : Prop

Single-challenge 1CCA security for bit encryption (Msg = Bool, Out = Bool).

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.WordINDCCA2 (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → List Bool → ProbComp (List Bool)) (decrypt : ℕ → List Bool → List Bool → Option (List Bool)) : Prop

Single-challenge 1CCA security for bit-string encryption (Msg = List Bool, Out = List Bool) under Attack Game 12.1's equal-length challenge rule m₀.length == m₁.length.

theorem Cslib.Crypto.Encryption.isPPTOn_run_cca2Phase1Oracle {Msg Out : Type} {encMsg : Msg ↪ List Bool} {encOut : Out ↪ List Bool} {decrypt : ℕ → List Bool → List Bool → Option Out} {adversary : CCA2AdversaryOf Msg} (hdec : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => decrypt p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encOption encOut)) (hA : CCA2AdversaryOf.IsPPT encMsg adversary) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encMsg encMsg) Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encFinEnum Unit)) fun (caller : ℕ × List Bool × List Bool) => (OracleComp.interpret (ProbOracleComp.handler (fun (m : ℕ) => StateT.lift (ProbComp.unifFin m)) (cca2Phase1Oracle encOut decrypt caller.1 caller.2.2)) (adversary.choose caller.1 caller.2.1)).run ()

Running Phase 1 (adversary.choose) against cca2Phase1Oracle is uniformly strict PPT in (n, pk, sk) whenever decrypt is computable in polynomial time.

theorem Cslib.Crypto.Encryption.isPPTOn_run_cca2Phase2Oracle {Msg Out : Type} {encMsg : Msg ↪ List Bool} {encOut : Out ↪ List Bool} {decrypt : ℕ → List Bool → List Bool → Option Out} {adversary : CCA2AdversaryOf Msg} (hdec : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => decrypt p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encOption encOut)) (hA : CCA2AdversaryOf.IsPPT encMsg adversary) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool (Turing.MultiTapeTM.encFinEnum Unit)) fun (caller : ℕ × List Bool × List Bool × List Bool) => (OracleComp.interpret (ProbOracleComp.handler (fun (m : ℕ) => StateT.lift (ProbComp.unifFin m)) (cca2Phase2Oracle encOut decrypt caller.1 caller.2.1 caller.2.2.2)) (adversary.guess caller.1 caller.2.2.1 caller.2.2.2)).run ()

Running Phase 2 (adversary.guess) against cca2Phase2Oracle is uniformly strict PPT in (n, sk, state, ct) whenever decrypt is computable in polynomial time.

theorem Cslib.Crypto.Encryption.isPPTOn_cca2GameOn {Msg Out : Type} {encMsg : Msg ↪ List Bool} {encOut : Out ↪ List Bool} {valid : ℕ → List Bool → Msg → Msg → Bool} {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)} {decrypt : ℕ → List Bool → List Bool → Option Out} {adversary : CCA2AdversaryOf Msg} (hvalid : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × Msg × Msg) => valid p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair encMsg encMsg))) Turing.MultiTapeTM.encBool) (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) keyGen) (hencrypt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encrypt p.1 p.2.1 p.2.2) (hdecrypt : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => decrypt p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encOption encOut)) (hA : CCA2AdversaryOf.IsPPT encMsg adversary) (bit : Bool) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (cca2GameOn valid encOut keyGen encrypt decrypt adversary bit)

The complete cca2GameOn experiment is uniformly strict PPT on the unary security parameter whenever valid, keyGen, encrypt, decrypt, and adversary are admissible.

theorem Cslib.Crypto.Encryption.isPPTOn_cca2Game {Msg Out : Type} {encMsg : Msg ↪ List Bool} {encOut : Out ↪ List Bool} {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)} {decrypt : ℕ → List Bool → List Bool → Option Out} {adversary : CCA2AdversaryOf Msg} (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) keyGen) (hencrypt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encrypt p.1 p.2.1 p.2.2) (hdecrypt : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => decrypt p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encOption encOut)) (hA : CCA2AdversaryOf.IsPPT encMsg adversary) (bit : Bool) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (cca2Game encOut keyGen encrypt decrypt adversary bit)

The complete cca2Game experiment is uniformly strict PPT on the unary security parameter whenever keyGen, encrypt, decrypt, and adversary are admissible.

Playing a restricted 1CCA game inside the unrestricted one

def Cslib.Crypto.Encryption.CCA2AdversaryOf.restrict {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (adversary : CCA2AdversaryOf Msg) : CCA2AdversaryOf Msg

The adversary that plays cca2GameOn valid inside the unrestricted cca2Game. Its choose runs adversary.choose n pk and puts the bit valid n pk m₀ m₁ in front of the saved state; its guess returns false when that bit is false and otherwise runs adversary.guess on the rest of the state. The challenge pair itself is passed on unchanged.

theorem Cslib.Crypto.Encryption.eval_cca2Game_restrict {Msg Out : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (encOut : Out ↪ List Bool) (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)) (decrypt : ℕ → List Bool → List Bool → Option Out) (adversary : CCA2AdversaryOf Msg) (bit : Bool) (n : ℕ) : (cca2Game encOut keyGen encrypt decrypt (CCA2AdversaryOf.restrict valid adversary) bit n).eval = (cca2GameOn valid encOut keyGen encrypt decrypt adversary bit n).eval

Running the unrestricted cca2Game on adversary.restrict valid has the same output distribution as running cca2GameOn valid on adversary.

theorem Cslib.Crypto.Encryption.CCA2AdversaryOf.IsPPT.restrict {Msg : Type} {encMsg : Msg ↪ List Bool} {valid : ℕ → List Bool → Msg → Msg → Bool} (hvalid : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × Msg × Msg) => valid p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair encMsg encMsg))) Turing.MultiTapeTM.encBool) {adversary : CCA2AdversaryOf Msg} (hadversary : IsPPT encMsg adversary) : IsPPT encMsg (CCA2AdversaryOf.restrict valid adversary)

Restricting a uniform strict oracle PPT 1CCA adversary by a polynomial-time admissibility predicate keeps it uniform strict oracle PPT: choose additionally evaluates valid and prepends one bit to the saved state, and guess branches on that bit without querying the oracle when it is false.

theorem Cslib.Crypto.Encryption.INDCCA2Of.indcca2On {Msg Out : Type} {encMsg : Msg ↪ List Bool} {encOut : Out ↪ List Bool} {valid : ℕ → List Bool → Msg → Msg → Bool} {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)} {decrypt : ℕ → List Bool → List Bool → Option Out} (h : INDCCA2Of encMsg encOut keyGen encrypt decrypt) (hvalid : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × Msg × Msg) => valid p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair encMsg encMsg))) Turing.MultiTapeTM.encBool) : INDCCA2On valid encMsg encOut keyGen encrypt decrypt

Unrestricted 1CCA security implies 1CCA security under every polynomial-time admissibility predicate.

theorem Cslib.Crypto.Encryption.INDCCA2Of.wordINDCCA2 {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encrypt : ℕ → List Bool → List Bool → ProbComp (List Bool)} {decrypt : ℕ → List Bool → List Bool → Option (List Bool)} (h : INDCCA2Of Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits keyGen encrypt decrypt) : WordINDCCA2 keyGen encrypt decrypt

Unrestricted bit-word 1CCA security implies WordINDCCA2.

1CCA implies IND-CPA

def Cslib.Crypto.Encryption.CCA2AdversaryOf.ofCPA {Msg : Type} (adversary : AdversaryOf Msg) : CCA2AdversaryOf Msg

Lift a chosen-plaintext AdversaryOf Msg to a 0-query CCA2AdversaryOf Msg.

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.CCA2Adversary.ofCPA (adversary : Adversary) : CCA2Adversary

Lift a chosen-plaintext bit Adversary to a 0-query CCA2Adversary.

theorem Cslib.Crypto.Encryption.CCA2AdversaryOf.isPPT_ofCPA {Msg : Type} {encMsg : Msg ↪ List Bool} {adversary : AdversaryOf Msg} (hA : AdversaryOf.IsPPT encMsg adversary) : IsPPT encMsg (ofCPA adversary)

Lifting a strict PPT AdversaryOf Msg yields a strict oracle PPT CCA2AdversaryOf Msg.

theorem Cslib.Crypto.Encryption.CCA2Adversary.isPPT_ofCPA {adversary : Adversary} (hA : adversary.IsPPT) : (ofCPA adversary).IsPPT

Lifting a strict PPT bit Adversary yields a strict oracle PPT CCA2Adversary.

theorem Cslib.Crypto.Encryption.CCA2AdversaryOf.isQueryBounded_ofCPA {Msg : Type} (adversary : AdversaryOf Msg) : (ofCPA adversary).IsQueryBounded (fun (x : ℕ) => 0) fun (x : ℕ) => 0

A lifted CPA adversary makes 0 decryption queries in both stages.

theorem Cslib.Crypto.Encryption.CCA2Adversary.isQueryBounded_ofCPA (adversary : Adversary) : CCA2AdversaryOf.IsQueryBounded (ofCPA adversary) (fun (x : ℕ) => 0) fun (x : ℕ) => 0

A lifted bit CPA adversary makes 0 decryption queries in both stages.

theorem Cslib.Crypto.Encryption.eval_cca2GameOn_ofCPA {Msg Out : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (encOut : Out ↪ List Bool) (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)) (decrypt : ℕ → List Bool → List Bool → Option Out) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : (cca2GameOn valid encOut keyGen encrypt decrypt (CCA2AdversaryOf.ofCPA adversary) bit n).eval = (gameOn valid keyGen encrypt adversary bit n).eval

Running a lifted CPA adversary in cca2GameOn has the same output distribution as the CPA gameOn with the same challenge-pair admissibility predicate valid.

theorem Cslib.Crypto.Encryption.eval_cca2Game_ofCPA {Msg Out : Type} (encOut : Out ↪ List Bool) (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)) (decrypt : ℕ → List Bool → List Bool → Option Out) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : (cca2Game encOut keyGen encrypt decrypt (CCA2AdversaryOf.ofCPA adversary) bit n).eval = (game keyGen encrypt adversary bit n).eval

Running a lifted CPA adversary in cca2Game has the same output distribution as the CPA game.

theorem Cslib.Crypto.Encryption.INDCCA2On.indcpaOn {Msg Out : Type} {valid : ℕ → List Bool → Msg → Msg → Bool} {encMsg : Msg ↪ List Bool} {encOut : Out ↪ List Bool} {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)} {decrypt : ℕ → List Bool → List Bool → Option Out} (h : INDCCA2On valid encMsg encOut keyGen encrypt decrypt) : INDCPAOn valid encMsg keyGen encrypt

1CCA security implies IND-CPA security under any challenge-pair admissibility predicate valid: any encryption scheme satisfying INDCCA2On valid also satisfies INDCPAOn valid.

theorem Cslib.Crypto.Encryption.INDCCA2Of.indcpaOf {Msg Out : Type} {encMsg : Msg ↪ List Bool} {encOut : Out ↪ List Bool} {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)} {decrypt : ℕ → List Bool → List Bool → Option Out} (h : INDCCA2Of encMsg encOut keyGen encrypt decrypt) : INDCPAOf encMsg keyGen encrypt

Unrestricted 1CCA security implies unrestricted IND-CPA security: any encryption scheme satisfying INDCCA2Of encMsg encOut also satisfies INDCPAOf encMsg.

theorem Cslib.Crypto.Encryption.INDCCA2Of.indcpa {Out : Type} {encOut : Out ↪ List Bool} {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)} {decrypt : ℕ → List Bool → List Bool → Option Out} (h : INDCCA2Of Turing.MultiTapeTM.encBool encOut keyGen encrypt decrypt) : INDCPA keyGen encrypt

1CCA security implies IND-CPA security: any bit encryption scheme satisfying INDCCA2Of also satisfies INDCPA.

theorem Cslib.Crypto.Encryption.INDCCA2.indcpa {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)} {decrypt : ℕ → List Bool → List Bool → Option Bool} (h : INDCCA2 keyGen encrypt decrypt) : INDCPA keyGen encrypt

Specialization of INDCCA2Of.indcpa to INDCCA2.

theorem Cslib.Crypto.Encryption.WordINDCCA2.wordINDCPA {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encrypt : ℕ → List Bool → List Bool → ProbComp (List Bool)} {decrypt : ℕ → List Bool → List Bool → Option (List Bool)} (h : WordINDCCA2 keyGen encrypt decrypt) : WordINDCPA keyGen encrypt

Word 1CCA security implies word IND-CPA security: any bit-string encryption scheme satisfying WordINDCCA2 also satisfies WordINDCPA.