Chosen-message security for bit encryption

The adversary receives the public key, chooses two bits and saves a finite state, then receives an encryption of the selected bit. Both stages are single uniform strict PPT algorithms. Their clocks charge the unary security parameter and the complete encoded input, including the saved state. The adversary may retain the public key in that state.

This is the single-challenge public-key experiment of Boneh and Shoup, Section 11.2, Attack Game 11.1, specialized to bit messages. For public-key encryption, further encryptions can be computed from the public key. The separate multi-challenge equivalence of their Theorem 11.1 is not formalized here. Encryption correctness and efficiency of the honest algorithms remain separate properties.

Main definitions

• Cslib.Crypto.Encryption.Adversary: message selection and guessing with explicit saved state.
• Cslib.Crypto.Encryption.Adversary.IsPPT: native uniform admissibility of both stages.
• Cslib.Crypto.Encryption.game: the actual key-generation and challenge-encryption experiment.
• Cslib.Crypto.Encryption.INDCPA: negligible distinguishing advantage for every admissible adversary, fixed before the security parameter.

Main results

• Cslib.Crypto.Encryption.eval_game: the experiment depends only on the public-key marginal.
• Cslib.Crypto.Encryption.INDCPA.congr: distributionally equal honest algorithms have the same security guarantee.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 11.2 and Section 11.3.2.

structure Cslib.Crypto.Encryption.Adversary : Type

A chosen-message adversary. The saved word contains all data retained between stages.

• choose : ℕ → List Bool → ProbComp ((Bool × Bool) × List Bool)

  Receive the public key, choose the two challenge messages, and save a state.

• guess : ℕ → List Bool → List Bool → ProbComp Bool

  Receive the saved state and challenge ciphertext, then return a distinguishing bit.

structure Cslib.Crypto.Encryption.Adversary.IsPPT (adversary : Adversary) : Prop

One finite-machine certificate for each whole stage, including the full saved-state cost. There is no parameter-dependent advice or separate algorithm for each security parameter.

• choose : Probability.IsPPT (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encBits) adversary.choose

  Message selection is uniform strict PPT on the parameter and public key.

• guess : Probability.IsPPTOn (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

  Guessing is uniform strict PPT on the parameter, saved state, and challenge ciphertext.

def Cslib.Crypto.Encryption.game (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) (adversary : Adversary) (bit : Bool) (n : ℕ) : ProbComp Bool

Sample the key pair and the chosen challenge encryption using the honest algorithms. The secret key is never passed to the adversary.

def Cslib.Crypto.Encryption.INDCPA (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) : Prop

Single-challenge IND-CPA for bit encryption against every uniform strict PPT adversary. The negligible bound may depend on the adversary, which is fixed before the parameter.

theorem Cslib.Crypto.Encryption.eval_game (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) (adversary : Adversary) (bit : Bool) (n : ℕ) : (game keyGen encrypt adversary bit n).eval = do let pk ← PMF.map Prod.fst (keyGen n).eval let choice ← (adversary.choose n pk).eval let ciphertext ← (encrypt n pk (if bit = true then choice.1.2 else choice.1.1)).eval (adversary.guess n choice.2 ciphertext).eval

Only the public-key marginal of key generation is observed by the experiment.

theorem Cslib.Crypto.Encryption.INDCPA.congr {keyGen keyGen' : ℕ → ProbComp (List Bool × List Bool)} {encrypt encrypt' : ℕ → List Bool → Bool → ProbComp (List Bool)} (h : INDCPA keyGen encrypt) (hkeyGen : ∀ (n : ℕ), PMF.map Prod.fst (keyGen n).eval = PMF.map Prod.fst (keyGen' n).eval) (hencrypt : ∀ (n : ℕ) (pk : List Bool) (bit : Bool), (encrypt n pk bit).eval = (encrypt' n pk bit).eval) : INDCPA keyGen' encrypt'

Equal public-key marginals and equal encryption laws preserve security.