Chosen-message security for public-key encryption

The adversary receives the public key, chooses two messages of type Msg and saves a finite state, then receives an encryption of the selected message. 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, p. 436. That game requires the two challenge messages to have the same length. Here admissibility is a Boolean predicate valid : ℕ → List Bool → Msg → Msg → Bool on the security parameter, the public key and the challenge pair: gameOn valid outputs false in both experiments when the pair is invalid, so an invalid pair contributes no advantage. The unrestricted experiment game and notion INDCPAOf are the always-true case. Single-bit messages (Adversary, INDCPA) are unrestricted, and bit-word messages (WordAdversary, WordINDCPA) use the equal-length predicate fun _ _ m₀ m₁ => m₀.length == m₁.length. 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.AdversaryOf, Cslib.Crypto.Encryption.Adversary, Cslib.Crypto.Encryption.WordAdversary: message selection and guessing with explicit saved state, for typed, bit, and bit-word messages.
• Cslib.Crypto.Encryption.AdversaryOf.IsPPT, Cslib.Crypto.Encryption.Adversary.IsPPT, Cslib.Crypto.Encryption.WordAdversary.IsPPT: native uniform admissibility of both stages.
• Cslib.Crypto.Encryption.gameOn, Cslib.Crypto.Encryption.game: the key-generation and challenge-encryption experiment, with and without a challenge-pair admissibility predicate.
• Cslib.Crypto.Encryption.INDCPAOn, Cslib.Crypto.Encryption.INDCPAOf, Cslib.Crypto.Encryption.INDCPA, Cslib.Crypto.Encryption.WordINDCPA: negligible distinguishing advantage for every admissible adversary, fixed before the security parameter.
• Cslib.Crypto.Encryption.AdversaryOf.restrict: the adversary that plays gameOn valid inside the unrestricted game, by recording validity in its saved state.

Main results

• Cslib.Crypto.Encryption.eval_gameOn, Cslib.Crypto.Encryption.eval_game: the experiments depend only on the public-key marginal.
• Cslib.Crypto.Encryption.eval_game_restrict: game on adversary.restrict valid has the same output distribution as gameOn valid on adversary.
• Cslib.Crypto.Encryption.INDCPAOn.congr, Cslib.Crypto.Encryption.INDCPAOf.congr, 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 (Attack Game 11.1, p. 436) and Section 11.3.2.

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

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

• choose : ℕ → List Bool → ProbComp ((Msg × Msg) × 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.AdversaryOf.IsPPT {Msg : Type} (encMsg : Msg ↪ List Bool) (adversary : AdversaryOf Msg) : Prop

One finite-machine certificate for each whole stage over message encoding encMsg, 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 encMsg encMsg) 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.

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.Adversary : Type

A chosen-message adversary for single-bit messages (Bool).

@[reducible, inline]

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

Native uniform strict PPT admissibility for a bit chosen-message adversary.

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.WordAdversary : Type

A chosen-message adversary for bit-word messages (List Bool).

@[reducible, inline]

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

Native uniform strict PPT admissibility for a bit-word chosen-message adversary.

def Cslib.Crypto.Encryption.gameOn {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : ProbComp Bool

The single-challenge chosen-message experiment with challenge-pair admissibility predicate valid ([BS23], Section 11.2, Attack Game 11.1, p. 436). Sample the key pair and pass the public key to adversary.choose. If valid n pk m₀ m₁ holds for the chosen pair, encrypt the selected message with the honest algorithm and return the adversary's guess; otherwise return false, in both experiments. The secret key is never passed to the adversary.

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.game {Msg : Type} (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : ProbComp Bool

The unrestricted chosen-message experiment: gameOn with every challenge pair admissible.

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

Single-challenge IND-CPA for encryption over message encoding encMsg with challenge-pair admissibility predicate valid, against every uniform strict PPT adversary. The negligible bound may depend on the adversary, which is fixed before the parameter.

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.INDCPAOf {Msg : Type} (encMsg : Msg ↪ List Bool) (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)) : Prop

Single-challenge IND-CPA with every challenge pair admissible. For message types whose messages all have one length, such as Bool, this is the textbook notion; for List Bool it is stronger than the textbook notion, which WordINDCPA states.

@[reducible, inline]

abbrev 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.

@[reducible, inline]

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

Single-challenge IND-CPA for bit-word encryption under Attack Game 11.1's equal-length rule ([BS23], Section 11.2, p. 436): challenge pairs with m₀.length ≠ m₁.length are inadmissible.

theorem Cslib.Crypto.Encryption.eval_gameOn {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : (gameOn valid keyGen encrypt adversary bit n).eval = do let pk ← PMF.map Prod.fst (keyGen n).eval let choice ← (adversary.choose n pk).eval if valid n pk choice.1.1 choice.1.2 = true then do let ciphertext ← (encrypt n pk (if bit = true then choice.1.2 else choice.1.1)).eval (adversary.guess n choice.2 ciphertext).eval else pure false

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

theorem Cslib.Crypto.Encryption.eval_game {Msg : Type} (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (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 unrestricted experiment.

theorem Cslib.Crypto.Encryption.INDCPAOn.congr {Msg : Type} {valid : ℕ → List Bool → Msg → Msg → Bool} {encMsg : Msg ↪ List Bool} {keyGen keyGen' : ℕ → ProbComp (List Bool × List Bool)} {encrypt encrypt' : ℕ → List Bool → Msg → ProbComp (List Bool)} (h : INDCPAOn valid encMsg keyGen encrypt) (hkeyGen : ∀ (n : ℕ), PMF.map Prod.fst (keyGen n).eval = PMF.map Prod.fst (keyGen' n).eval) (hencrypt : ∀ (n : ℕ) (pk : List Bool) (msg : Msg), (encrypt n pk msg).eval = (encrypt' n pk msg).eval) : INDCPAOn valid encMsg keyGen' encrypt'

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

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

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

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 bit-encryption laws preserve security.

Playing a restricted game inside the unrestricted one

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

The adversary that plays gameOn valid inside the unrestricted game. 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_game_restrict {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : (game keyGen encrypt (AdversaryOf.restrict valid adversary) bit n).eval = (gameOn valid keyGen encrypt adversary bit n).eval

Running the unrestricted game on adversary.restrict valid has the same output distribution as running gameOn valid on adversary.