Replacing the public-key distribution in chosen-message security

One uniform distinguisher samples a hidden fair challenge bit after the adversary has chosen its messages and saved state. It runs the actual encryption and guessing stages, then returns the guess XOR the hidden bit. Comparing this same distinguisher on two public-key distributions controls the change in their chosen-message gaps, with an exact factor of two.

Main definitions

• publicKeyGame: the chosen-message experiment for a specified public-key law.
• keyDistinguisher: the single reduction, preserving the adversary's saved state.

Main results

• eval_game_eq_publicKeyGame: the actual encryption game uses its public-key marginal.
• isPPT_keyDistinguisher: native strict PPT composition of the actual reduction.
• probability_keyDistinguisher: the exact affine identity for the signed chosen-message gap.
• advantage_publicKeyGame_le: quantitative public-key replacement with loss two.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 11.2, for the chosen-message experiment and game-reduction method.

noncomputable def Cslib.Crypto.Encryption.publicKeyGame (keys : PMF (List Bool)) (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) (adversary : Adversary) (bit : Bool) (security : ℕ) : Game

Run the chosen-message experiment with a specified public-key distribution. The complete state returned by message selection is passed unchanged to guessing.

theorem Cslib.Crypto.Encryption.eval_game_eq_publicKeyGame (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) (adversary : Adversary) (bit : Bool) (security : ℕ) : (game keyGen encrypt adversary bit security).eval = publicKeyGame (PMF.map Prod.fst (keyGen security).eval) encrypt adversary bit security

An honest key generator contributes precisely its public-key marginal.

noncomputable def Cslib.Crypto.Encryption.keyDistinguisher (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) (adversary : Adversary) : Distinguisher

A single uniform distinguisher with its own hidden fair challenge bit. The adversary sees only the supplied public key and the actual challenge ciphertext, with its saved state retained.

theorem Cslib.Crypto.Encryption.isPPT_keyDistinguisher {encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)} {adversary : Adversary} (hencrypt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBits fun (input : ℕ × List Bool × Bool) => encrypt input.1 input.2.1 input.2.2) (hadversary : adversary.IsPPT) : Probability.IsPPT Turing.MultiTapeTM.encBool (keyDistinguisher encrypt adversary)

The reduction is one uniform strict PPT program when encryption and both adversary stages are certified on their complete inputs.

theorem Cslib.Crypto.Encryption.distinguishingGame_keyDistinguisher (keys : PMF (List Bool)) (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) (adversary : Adversary) (security : ℕ) : distinguishingGame keys (keyDistinguisher encrypt adversary security) = do let bit ← Probability.PMF.uniformOfFintype Bool PMF.map (fun (guess : Bool) => guess ^^ bit) (publicKeyGame keys encrypt adversary bit security)

The hidden-bit experiment averages the two chosen-message games, complementing the second. No finiteness or independence assumption is imposed on the saved state.

theorem Cslib.Crypto.Encryption.probability_keyDistinguisher (keys : PMF (List Bool)) (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) (adversary : Adversary) (security : ℕ) : ↑(distinguishingGame keys (keyDistinguisher encrypt adversary security)).succProbability = (1 + ↑(publicKeyGame keys encrypt adversary false security).succProbability - ↑(publicKeyGame keys encrypt adversary true security).succProbability) / 2

Acceptance is one half plus half the signed chosen-message gap.

theorem Cslib.Crypto.Encryption.advantage_publicKeyGame_le (real ideal : PMF (List Bool)) (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) (adversary : Adversary) (security : ℕ) : (publicKeyGame real encrypt adversary false security).advantage (publicKeyGame real encrypt adversary true security) ≤ 2 * (distinguishingGame real (keyDistinguisher encrypt adversary security)).advantage (distinguishingGame ideal (keyDistinguisher encrypt adversary security)) + (publicKeyGame ideal encrypt adversary false security).advantage (publicKeyGame ideal encrypt adversary true security)

Replacing the public-key law costs at most twice the advantage of one uniform hidden-bit distinguisher, plus the chosen-message advantage under the replacement law.