Native runtime of the chosen-message experiment

The actual experiment composes key generation, message selection, encryption and guessing. Native certificates charge the complete sampled public key, saved adversary state and challenge ciphertext; no independent bound on those intermediate values is assumed.

Main results

• Cslib.Crypto.Encryption.isPPTOn_gameOn, Cslib.Crypto.Encryption.isPPTOn_game: the experiments are uniform strict PPT when their inputs are efficiently computed, the admissibility predicate is computable in polynomial time, and the honest algorithms and adversary have native certificates.
• Cslib.Crypto.Encryption.AdversaryOf.IsPPT.restrict: restricting a uniform strict PPT adversary by a polynomial-time admissibility predicate keeps it uniform strict PPT.
• Cslib.Crypto.Encryption.INDCPAOf.indcpaOn, Cslib.Crypto.Encryption.INDCPAOf.wordINDCPA: unrestricted IND-CPA implies IND-CPA under every polynomial-time admissibility predicate, in particular WordINDCPA for bit-word encryption.
• Cslib.Crypto.Encryption.exists_keyLength_bound: key generation supplies an executable unary polynomial bounding all supported public and secret keys.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 11.2, Attack Game 11.1, p. 436.

theorem Cslib.Crypto.Encryption.isPPTOn_gameOn {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) {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)} (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) {adversary : AdversaryOf Msg} (hadversary : AdversaryOf.IsPPT encMsg adversary) {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {bit : α → Bool} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hbit : Turing.MultiTapeTM.ComputableInPolyTime bit input Turing.MultiTapeTM.encBool) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => gameOn valid keyGen encrypt adversary (bit a) (n a)

The chosen-message experiment gameOn valid has a strict clock in the full encoded caller input when valid is computable in polynomial time.

theorem Cslib.Crypto.Encryption.isPPTOn_game {Msg : Type} {encMsg : Msg ↪ List Bool} {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)} (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) {adversary : AdversaryOf Msg} (hadversary : AdversaryOf.IsPPT encMsg adversary) {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {bit : α → Bool} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hbit : Turing.MultiTapeTM.ComputableInPolyTime bit input Turing.MultiTapeTM.encBool) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => game keyGen encrypt adversary (bit a) (n a)

The unrestricted chosen-message experiment has a strict clock in the full encoded caller input.

theorem Cslib.Crypto.Encryption.AdversaryOf.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 : AdversaryOf Msg} (hadversary : IsPPT encMsg adversary) : IsPPT encMsg (AdversaryOf.restrict valid adversary)

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

theorem Cslib.Crypto.Encryption.INDCPAOf.indcpaOn {Msg : Type} {encMsg : Msg ↪ List Bool} {valid : ℕ → List Bool → Msg → Msg → Bool} {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)} (h : INDCPAOf encMsg keyGen encrypt) (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) : INDCPAOn valid encMsg keyGen encrypt

Unrestricted IND-CPA implies IND-CPA under every polynomial-time admissibility predicate.

theorem Cslib.Crypto.Encryption.INDCPAOf.wordINDCPA {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encrypt : ℕ → List Bool → List Bool → ProbComp (List Bool)} (h : INDCPAOf Turing.MultiTapeTM.encBits keyGen encrypt) : WordINDCPA keyGen encrypt

Unrestricted bit-word IND-CPA implies WordINDCPA.

theorem Cslib.Crypto.Encryption.exists_keyLength_bound {keyGen : ℕ → ProbComp (List Bool × List Bool)} (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) keyGen) : ∃ (c : ℕ) (d : ℕ), Turing.MultiTapeTM.ComputableInPolyTime (fun (n : ℕ) => c * (n + 1) ^ d) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary ∧ ∀ (n : ℕ), ∀ keys ∈ (keyGen n).eval.support, keys.1.length + keys.2.length ≤ c * (n + 1) ^ d

Strict PPT key generation supplies an executable unary polynomial bounding the total public and secret key material on every supported execution. No width function is assumed computable.