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_game: the experiment is uniform strict PPT when its inputs are efficiently computed and the honest algorithms and adversary have native certificates.
• 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.

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

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

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.ComputableTidilyInPolyTime (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.