KEM–DEM hybrid public-key encryption

A Key Encapsulation Mechanism (KEM) samples a public/secret key pair (pk, sk) ← keyGen n and encapsulates a symmetric key (k, ctKem) ← encaps n pk ([BS23], Exercise 11.9). Its chosen-plaintext / semantic security (KEMINDCPA, Exercise 11.9) asks that replacing the encapsulated key k with an independent uniform n-bit key BitString.sampleList n is computationally indistinguishable to every uniform strict PPT distinguisher receiving (pk, (k, ctKem)).

A Data Encapsulation Mechanism (DEM) over message space Msg encrypts a single challenge message under a fresh uniform n-bit key ([BS23], Section 2.2, Attack Game 2.1, p. 16, and Definition 2.2). As for public-key encryption (Encryption.gameOn), the experiment demGameOn takes a challenge-pair admissibility predicate valid, and an inadmissible pair makes it output false in both experiments. demGame and DEMOneTimeINDCPAOf are the always-true case, DEMOneTimeINDCPA specializes to single-bit messages, and DEMOneTimeWordINDCPA imposes Attack Game 2.1's equal-length rule on bit words.

Combining encaps with encryptSym produces the hybrid public-key encryption scheme hybridEncrypt encaps encryptSym (hybridDecrypt decaps decryptSym, Exercise 11.9(a)). By Boneh and Shoup's Exercise 11.9(b), if the KEM is IND-CPA secure and the DEM is one-time IND-CPA secure, then hybridEncrypt encaps encryptSym is IND-CPA secure: KEMINDCPA.hybrid_indcpa for unrestricted challenge pairs, and KEMINDCPA.hybrid_indcpaOn under an admissibility predicate that ignores the public key, such as the equal-length rule. We formalize both the single hidden-bit KEM distinguisher bound of Exercise 11.9(b) (advantage_hybridGame_le_two_mul) and its two-distinguisher triangle-inequality variant (advantage_hybridGame_le), together with non-vacuous single-bit and n-bit word one-time pad DEM instantiations (otpEncrypt, otpDecrypt, demOneTimeINDCPA_otpEncrypt, KEMINDCPA.hybrid_otpEncrypt_indcpa, otpWordEncrypt, otpWordDecrypt, demOneTimeINDCPA_otpWordEncrypt, demOneTimeWordINDCPA_otpWordEncrypt, KEMINDCPA.hybrid_otpWordEncrypt_indcpa).

Relative to Boneh and Shoup, Exercise 11.9, this development has the following representation conventions:

• Plaintext messages are parameterized by Msg : Type (with message encoding encMsg : Msg ↪ List Bool for PPT admissibility), matching Encryption.gameOn and Encryption.INDCPAOn in Complexity/Crypto/Computational/Encryption/Basic.lean.
• The DEM adversary receives the empty public key [], and demGameOn valid evaluates valid at it. KEMINDCPA.hybrid_indcpaOn therefore asks that valid ignore the public key.
• Both the ideal KEM key distribution and the one-time DEM key distribution at security parameter n are fixed to uniform n-bit strings (BitString.sampleList n). Because encaps returns arbitrary bit lists and KEMINDCPA requires only negligible distinguishing advantage, finitely many or negligibly probable length deviations remain compatible with KEMINDCPA, whereas non-negligible length deviations are detectable (as in not_kemINDCPA_leaking).
• Decapsulation decaps and hybrid decryption hybridDecrypt are total deterministic functions without a separate reject symbol; hybridDecrypt_hybridEncrypt states exact recovery on supported ciphertexts when decaps and decryptSym are correct on supported outputs.
• In kemRealGame and kemIdealGame, the KEM distinguisher receives the public key pk explicitly alongside (k, ctKem) (encoded as (pk, (k, ctKem))). Although the prose of Exercise 11.9 writes that the challenger sends (k_b, c_kem), the public key pk is public in a public-key KEM experiment and is required by the reduction distinguisher to run adversary.choose n pk.

Main definitions

• Cslib.Crypto.Encryption.kemRealGame, Cslib.Crypto.Encryption.kemIdealGame, Cslib.Crypto.Encryption.KEMINDCPA: real and ideal KEM IND-CPA experiments and security.
• Cslib.Crypto.Encryption.demGameOn, Cslib.Crypto.Encryption.demGame, Cslib.Crypto.Encryption.DEMOneTimeINDCPAOn, Cslib.Crypto.Encryption.DEMOneTimeINDCPAOf, Cslib.Crypto.Encryption.DEMOneTimeINDCPA, Cslib.Crypto.Encryption.DEMOneTimeWordINDCPA: one-time symmetric encryption experiments and security, with and without an admissibility predicate.
• Cslib.Crypto.Encryption.hybridEncrypt, Cslib.Crypto.Encryption.hybridDecrypt: KEM–DEM hybrid encryption and deterministic decryption.
• Cslib.Crypto.Encryption.hybridIdealGame: intermediate game replacing the encapsulated key with an independent uniform n-bit key.
• Cslib.Crypto.Encryption.hybridToKEMDistinguisher, Cslib.Crypto.Encryption.hybridToKEMHiddenBitDistinguisher, Cslib.Crypto.Encryption.hybridToDEMAdversary: the certified uniform reductions.
• Cslib.Crypto.Encryption.otpEncrypt, Cslib.Crypto.Encryption.otpDecrypt, Cslib.Crypto.Encryption.otpWordEncrypt, Cslib.Crypto.Encryption.otpWordDecrypt: one-time pad single-bit and n-bit word DEMs.

Main results

• Cslib.Crypto.Encryption.isPPTOn_kemRealGame, Cslib.Crypto.Encryption.isPPTOn_kemIdealGame, Cslib.Crypto.Encryption.isPPTOn_demGameOn, Cslib.Crypto.Encryption.isPPTOn_demGame, Cslib.Crypto.Encryption.isPPTOn_hybridEncrypt, Cslib.Crypto.Encryption.computableInPolyTime_hybridDecrypt: polynomial-time certificates.
• Cslib.Crypto.Encryption.hybridDecrypt_encPair, Cslib.Crypto.Encryption.hybridDecrypt_hybridEncrypt: exact decryption correctness (Exercise 11.9(a)).
• Cslib.Crypto.Encryption.advantage_hybridGame_le_two_mul, Cslib.Crypto.Encryption.advantage_hybridGame_le: quantitative Boneh–Shoup Exercise 11.9(b) reduction and its two-distinguisher variant.
• Cslib.Crypto.Encryption.eval_demGame_restrict, Cslib.Crypto.Encryption.DEMOneTimeINDCPAOf.demOneTimeINDCPAOn: unrestricted one-time security implies one-time security under every polynomial-time admissibility predicate.
• Cslib.Crypto.Encryption.KEMINDCPA.hybrid_indcpa, Cslib.Crypto.Encryption.KEMINDCPA.hybrid_indcpaOn: asymptotic Boneh–Shoup Exercise 11.9(b), without and with an admissibility predicate.
• Cslib.Crypto.Encryption.demOneTimeINDCPA_otpEncrypt, Cslib.Crypto.Encryption.KEMINDCPA.hybrid_otpEncrypt_indcpa, Cslib.Crypto.Encryption.demOneTimeINDCPA_otpWordEncrypt, Cslib.Crypto.Encryption.demOneTimeWordINDCPA_otpWordEncrypt, Cslib.Crypto.Encryption.KEMINDCPA.hybrid_otpWordEncrypt_indcpa: unconditional one-time pad DEM security and the KEM-to-PKE corollaries.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 2.2 (Attack Game 2.1 and Definition 2.2, p. 16) and Exercise 11.9 (pp. 460–461).

Key Encapsulation Mechanisms

def Cslib.Crypto.Encryption.kemRealGame (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (distinguisher : Distinguisher) (n : ℕ) : ProbComp Bool

The real KEM IND-CPA experiment ([BS23], Exercise 11.9, Experiment 0): sample (pk, sk) ← keyGen n and (k, ctKem) ← encaps n pk, and pass the encoded triple (pk, (k, ctKem)) to distinguisher n.

noncomputable def Cslib.Crypto.Encryption.kemIdealGame (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (distinguisher : Distinguisher) (n : ℕ) : ProbComp Bool

The ideal KEM IND-CPA experiment ([BS23], Exercise 11.9, Experiment 1): sample (pk, sk) ← keyGen n, (k, ctKem) ← encaps n pk, and an independent uniform n-bit key kIdeal ← BitString.sampleList n, and pass (pk, (kIdeal, ctKem)) to distinguisher n.

theorem Cslib.Crypto.Encryption.isPPTOn_kemRealGame {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)} (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) keyGen) (hencaps : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × List Bool) => encaps p.1 p.2) {distinguisher : Distinguisher} (hdist : Probability.IsPPT Turing.MultiTapeTM.encBool distinguisher) {α : Type} {input : α ↪ List Bool} {n : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => kemRealGame keyGen encaps distinguisher (n a)

The real KEM IND-CPA experiment is uniform strict PPT when key generation, encapsulation, and the distinguisher have native certificates.

theorem Cslib.Crypto.Encryption.isPPTOn_kemIdealGame {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)} (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) keyGen) (hencaps : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × List Bool) => encaps p.1 p.2) {distinguisher : Distinguisher} (hdist : Probability.IsPPT Turing.MultiTapeTM.encBool distinguisher) {α : Type} {input : α ↪ List Bool} {n : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => kemIdealGame keyGen encaps distinguisher (n a)

The ideal KEM IND-CPA experiment is uniform strict PPT when key generation, encapsulation, and the distinguisher have native certificates.

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

IND-CPA / semantic security for a Key Encapsulation Mechanism ([BS23], Exercise 11.9): every uniform strict PPT distinguisher has negligible advantage between kemRealGame and kemIdealGame.

One-Time Symmetric Encryption (DEM)

noncomputable def Cslib.Crypto.Encryption.demGameOn {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : ProbComp Bool

The one-time symmetric chosen-plaintext experiment over message space Msg with challenge-pair admissibility predicate valid ([BS23], Section 2.2, Attack Game 2.1, p. 16): sample a uniform n-bit key k ← BitString.sampleList n and invoke adversary.choose n []; the adversary receives the empty public key [], and valid is evaluated at it. If the chosen pair is valid, encrypt the selected message under encryptSym n k and pass the saved state and challenge ciphertext to adversary.guess n; otherwise return false, in both experiments.

@[reducible, inline]

noncomputable abbrev Cslib.Crypto.Encryption.demGame {Msg : Type} (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : ProbComp Bool

The unrestricted one-time symmetric experiment: demGameOn with every challenge pair admissible.

theorem Cslib.Crypto.Encryption.eval_demGame_restrict {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : (demGame encryptSym (AdversaryOf.restrict valid adversary) bit n).eval = (demGameOn valid encryptSym adversary bit n).eval

Running the unrestricted demGame on adversary.restrict valid has the same output distribution as running demGameOn valid on adversary.

theorem Cslib.Crypto.Encryption.isPPTOn_demGameOn {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) {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} (hencrypt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym 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 : α) => demGameOn valid encryptSym adversary (bit a) (n a)

The one-time symmetric experiment demGameOn valid has a strict polynomial clock when valid is computable in polynomial time and symmetric encryption and both adversary stages have native certificates.

theorem Cslib.Crypto.Encryption.isPPTOn_demGame {Msg : Type} {encMsg : Msg ↪ List Bool} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} (hencrypt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym 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 : α) => demGame encryptSym adversary (bit a) (n a)

The unrestricted one-time symmetric experiment has a strict polynomial clock when symmetric encryption and both adversary stages have native certificates.

def Cslib.Crypto.Encryption.DEMOneTimeINDCPAOn {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (encMsg : Msg ↪ List Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) : Prop

One-time symmetric IND-CPA / semantic security over message encoding encMsg with challenge-pair admissibility predicate valid ([BS23], Section 2.2, Attack Game 2.1, p. 16, and Definition 2.2): every uniform strict PPT Encryption.AdversaryOf Msg has negligible distinguishing advantage between demGameOn valid encryptSym adversary false and demGameOn valid encryptSym adversary true.

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.DEMOneTimeINDCPAOf {Msg : Type} (encMsg : Msg ↪ List Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) : Prop

One-time symmetric IND-CPA with every challenge pair admissible. For List Bool messages this is stronger than the textbook notion, which DEMOneTimeWordINDCPA states.

theorem Cslib.Crypto.Encryption.DEMOneTimeINDCPAOf.demOneTimeINDCPAOn {Msg : Type} {encMsg : Msg ↪ List Bool} {valid : ℕ → List Bool → Msg → Msg → Bool} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} (h : DEMOneTimeINDCPAOf encMsg encryptSym) (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) : DEMOneTimeINDCPAOn valid encMsg encryptSym

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

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.DEMOneTimeINDCPA (encryptSym : ℕ → List Bool → Bool → ProbComp (List Bool)) : Prop

One-time symmetric IND-CPA / semantic security for single-bit encryption.

@[reducible, inline]

abbrev Cslib.Crypto.Encryption.DEMOneTimeWordINDCPA (encryptSym : ℕ → List Bool → List Bool → ProbComp (List Bool)) : Prop

One-time symmetric IND-CPA / semantic security for bit-word encryption under Attack Game 2.1's equal-length rule ([BS23], Section 2.2, p. 16): challenge pairs with m₀.length ≠ m₁.length are inadmissible.

Hybrid Encryption Construction and Correctness

def Cslib.Crypto.Encryption.hybridEncrypt {Msg : Type} (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (n : ℕ) (pk : List Bool) (msg : Msg) : ProbComp (List Bool)

KEM–DEM hybrid encryption ([BS23], Exercise 11.9): encapsulate a symmetric key (k, ctKem) ← encaps n pk, encrypt the plaintext message under k via ctDem ← encryptSym n k msg, and encode (ctKem, ctDem) using encPair encBits encBits.

def Cslib.Crypto.Encryption.hybridDecrypt {Msg : Type} (decaps : ℕ → List Bool → List Bool → List Bool) (decryptSym : ℕ → List Bool → List Bool → Msg) (n : ℕ) (sk ct : List Bool) : Msg

Deterministic KEM–DEM hybrid decryption ([BS23], Exercise 11.9): decode the hybrid ciphertext ct into ctKem = unframe ct and ctDem = dropFrame ct, decapsulate k = decaps n sk ctKem, and return decryptSym n k ctDem.

theorem Cslib.Crypto.Encryption.isPPTOn_hybridEncrypt {Msg : Type} {encMsg : Msg ↪ List Bool} {encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} (hencaps : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × List Bool) => encaps p.1 p.2) (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => hybridEncrypt encaps encryptSym p.1 p.2.1 p.2.2

Hybrid encryption is uniform strict PPT when encapsulation and symmetric encryption are.

theorem Cslib.Crypto.Encryption.computableInPolyTime_hybridDecrypt {Msg : Type} {encMsg : Msg ↪ List Bool} {decaps : ℕ → List Bool → List Bool → List Bool} {decryptSym : ℕ → List Bool → List Bool → Msg} (hdecaps : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => decaps p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hdecryptSym : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => decryptSym p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) encMsg) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hybridDecrypt decaps decryptSym p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) encMsg

Hybrid decryption is computable in polynomial time when decapsulation and symmetric decryption are computable in polynomial time.

theorem Cslib.Crypto.Encryption.hybridDecrypt_encPair {Msg : Type} (decaps : ℕ → List Bool → List Bool → List Bool) (decryptSym : ℕ → List Bool → List Bool → Msg) (n : ℕ) (sk ctKem ctDem : List Bool) : hybridDecrypt decaps decryptSym n sk ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (ctKem, ctDem)) = decryptSym n (decaps n sk ctKem) ctDem

Hybrid decryption on an encoded ciphertext pair (ctKem, ctDem) decapsulates ctKem and decrypts ctDem under the resulting key.

theorem Cslib.Crypto.Encryption.hybridDecrypt_hybridEncrypt {Msg : Type} {encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)} {decaps : ℕ → List Bool → List Bool → List Bool} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} {decryptSym : ℕ → List Bool → List Bool → Msg} {n : ℕ} {pk sk ct : List Bool} {msg : Msg} (hkem : ∀ (k ctKem : List Bool), (k, ctKem) ∈ (encaps n pk).eval.support → decaps n sk ctKem = k) (hdem : ∀ (k ctDem : List Bool), (∃ (ctKem : List Bool), (k, ctKem) ∈ (encaps n pk).eval.support) → ctDem ∈ (encryptSym n k msg).eval.support → decryptSym n k ctDem = msg) (hct : ct ∈ (hybridEncrypt encaps encryptSym n pk msg).eval.support) : hybridDecrypt decaps decryptSym n sk ct = msg

Hybrid decryption correctness: if decaps n sk recovers the encapsulated key k on every supported output (k, ctKem) of encaps n pk, and decryptSym n k recovers msg on every supported output of encryptSym n k msg, then hybridDecrypt recovers msg on every supported ciphertext of hybridEncrypt.

Boneh–Shoup Exercise 11.9(b) Reductions and Asymptotic Security

noncomputable def Cslib.Crypto.Encryption.hybridIdealGame {Msg : Type} (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : ProbComp Bool

The intermediate hybrid game $G_1$ for the standard hybrid argument of [BS23], Exercise 11.9(b): identical to Encryption.game keyGen (hybridEncrypt encaps encryptSym) except that the symmetric key passed to encryptSym is an independent uniform n-bit key kIdeal ← BitString.sampleList n rather than encapsulated.1.

def Cslib.Crypto.Encryption.hybridToKEMDistinguisher {Msg : Type} (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (bit : Bool) : Distinguisher

Direct per-bit KEM distinguisher $D_{\mathrm{kem}, b}$ constructed from an Encryption.AdversaryOf Msg and DEM encryption encryptSym (for the two-distinguisher variant of [BS23], Exercise 11.9(b)): given an encoded KEM challenge (pk, (k, ctKem)), run adversary.choose n pk, encrypt the bit-selected message under k, and run adversary.guess on (ctKem, ctDem).

noncomputable def Cslib.Crypto.Encryption.hybridToKEMHiddenBitDistinguisher {Msg : Type} (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) : Distinguisher

Single hidden-bit KEM distinguisher $\mathcal{B}_{\mathrm{kem}}$ for [BS23], Exercise 11.9(b): given an encoded KEM challenge (pk, (k, ctKem)), run adversary.choose n pk, sample a fair challenge bit bit ← ProbComp.uniform Bool, encrypt the selected message under k, run adversary.guess, and return guess ^^ bit.

def Cslib.Crypto.Encryption.hybridToDEMAdversary {Msg : Type} (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (adversary : AdversaryOf Msg) : AdversaryOf Msg

Two-stage DEM adversary $\mathcal{B}_{\mathrm{s}}$ constructed from keyGen, encaps, and a hybrid Encryption.AdversaryOf Msg for [BS23], Exercise 11.9(b): stage 1 samples (pk, sk) ← keyGen n and (k, ctKem) ← encaps n pk, runs adversary.choose n pk, and saves encPair encBits encBits (ctKem, choice.2); stage 2 combines ctKem with the DEM challenge ciphertext ctDem and runs adversary.guess.

theorem Cslib.Crypto.Encryption.isPPT_hybridToKEMDistinguisher {Msg : Type} {encMsg : Msg ↪ List Bool} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} {adversary : AdversaryOf Msg} (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) (hadversary : AdversaryOf.IsPPT encMsg adversary) (bit : Bool) : Probability.IsPPT Turing.MultiTapeTM.encBool (hybridToKEMDistinguisher encryptSym adversary bit)

hybridToKEMDistinguisher is uniform strict PPT whenever symmetric encryption and the hybrid adversary are.

theorem Cslib.Crypto.Encryption.isPPT_hybridToKEMHiddenBitDistinguisher {Msg : Type} {encMsg : Msg ↪ List Bool} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} {adversary : AdversaryOf Msg} (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) (hadversary : AdversaryOf.IsPPT encMsg adversary) : Probability.IsPPT Turing.MultiTapeTM.encBool (hybridToKEMHiddenBitDistinguisher encryptSym adversary)

hybridToKEMHiddenBitDistinguisher is uniform strict PPT whenever symmetric encryption and the hybrid adversary are.

theorem Cslib.Crypto.Encryption.isPPT_hybridToDEMAdversary {Msg : Type} {encMsg : Msg ↪ List Bool} {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)} {adversary : AdversaryOf Msg} (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) keyGen) (hencaps : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × List Bool) => encaps p.1 p.2) (hadversary : AdversaryOf.IsPPT encMsg adversary) : AdversaryOf.IsPPT encMsg (hybridToDEMAdversary keyGen encaps adversary)

hybridToDEMAdversary is an admissible uniform strict PPT Encryption.AdversaryOf Msg whenever key generation, encapsulation, and the hybrid adversary are.

@[simp]

theorem Cslib.Crypto.Encryption.eval_kemRealGame_hybridToKEMDistinguisher {Msg : Type} (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : (kemRealGame keyGen encaps (hybridToKEMDistinguisher encryptSym adversary bit) n).eval = (game keyGen (hybridEncrypt encaps encryptSym) adversary bit n).eval

In the real KEM experiment, hybridToKEMDistinguisher reproduces the actual hybrid encryption experiment Encryption.game keyGen (hybridEncrypt encaps encryptSym).

@[simp]

theorem Cslib.Crypto.Encryption.eval_kemIdealGame_hybridToKEMDistinguisher {Msg : Type} (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : (kemIdealGame keyGen encaps (hybridToKEMDistinguisher encryptSym adversary bit) n).eval = (hybridIdealGame keyGen encaps encryptSym adversary bit n).eval

In the ideal KEM experiment, hybridToKEMDistinguisher reproduces the intermediate game hybridIdealGame.

@[simp]

theorem Cslib.Crypto.Encryption.eval_demGame_hybridToDEMAdversary {Msg : Type} (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : (demGame encryptSym (hybridToDEMAdversary keyGen encaps adversary) bit n).eval = (hybridIdealGame keyGen encaps encryptSym adversary bit n).eval

In the one-time symmetric DEM experiment, hybridToDEMAdversary reproduces the intermediate game hybridIdealGame.

theorem Cslib.Crypto.Encryption.eval_kemRealGame_hybridToKEMHiddenBitDistinguisher {Msg : Type} (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (n : ℕ) : (kemRealGame keyGen encaps (hybridToKEMHiddenBitDistinguisher encryptSym adversary) n).eval = do let bit ← Probability.PMF.uniformOfFintype Bool PMF.map (fun (guess : Bool) => guess ^^ bit) (game keyGen (hybridEncrypt encaps encryptSym) adversary bit n).eval

In the real KEM experiment, hybridToKEMHiddenBitDistinguisher averages the two hybrid chosen-message games, complementing the second.

theorem Cslib.Crypto.Encryption.eval_kemIdealGame_hybridToKEMHiddenBitDistinguisher {Msg : Type} (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (n : ℕ) : (kemIdealGame keyGen encaps (hybridToKEMHiddenBitDistinguisher encryptSym adversary) n).eval = do let bit ← Probability.PMF.uniformOfFintype Bool PMF.map (fun (guess : Bool) => guess ^^ bit) (hybridIdealGame keyGen encaps encryptSym adversary bit n).eval

In the ideal KEM experiment, hybridToKEMHiddenBitDistinguisher averages the two intermediate games hybridIdealGame, complementing the second.

theorem Cslib.Crypto.Encryption.probability_kemRealGame_hybridToKEMHiddenBitDistinguisher {Msg : Type} (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (n : ℕ) : ↑(Game.succProbability (kemRealGame keyGen encaps (hybridToKEMHiddenBitDistinguisher encryptSym adversary) n).eval) = (1 + ↑(Game.succProbability (game keyGen (hybridEncrypt encaps encryptSym) adversary false n).eval) - ↑(Game.succProbability (game keyGen (hybridEncrypt encaps encryptSym) adversary true n).eval)) / 2

Success probability of hybridToKEMHiddenBitDistinguisher in kemRealGame is one half plus half the signed hybrid chosen-message gap.

theorem Cslib.Crypto.Encryption.probability_kemIdealGame_hybridToKEMHiddenBitDistinguisher {Msg : Type} (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (n : ℕ) : ↑(Game.succProbability (kemIdealGame keyGen encaps (hybridToKEMHiddenBitDistinguisher encryptSym adversary) n).eval) = (1 + ↑(Game.succProbability (hybridIdealGame keyGen encaps encryptSym adversary false n).eval) - ↑(Game.succProbability (hybridIdealGame keyGen encaps encryptSym adversary true n).eval)) / 2

Success probability of hybridToKEMHiddenBitDistinguisher in kemIdealGame is one half plus half the signed hybridIdealGame gap.

theorem Cslib.Crypto.Encryption.advantage_hybridGame_le {Msg : Type} (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (n : ℕ) : Game.advantage (game keyGen (hybridEncrypt encaps encryptSym) adversary false n).eval (game keyGen (hybridEncrypt encaps encryptSym) adversary true n).eval ≤ Game.advantage (kemRealGame keyGen encaps (hybridToKEMDistinguisher encryptSym adversary false) n).eval (kemIdealGame keyGen encaps (hybridToKEMDistinguisher encryptSym adversary false) n).eval + Game.advantage (kemRealGame keyGen encaps (hybridToKEMDistinguisher encryptSym adversary true) n).eval (kemIdealGame keyGen encaps (hybridToKEMDistinguisher encryptSym adversary true) n).eval + Game.advantage (demGame encryptSym (hybridToDEMAdversary keyGen encaps adversary) false n).eval (demGame encryptSym (hybridToDEMAdversary keyGen encaps adversary) true n).eval

Quantitative KEM–DEM reduction via two per-bit KEM distinguishers (two-distinguisher variant of [BS23], Exercise 11.9(b)): the hybrid IND-CPA advantage is bounded by the sum of the KEM advantages of hybridToKEMDistinguisher encryptSym adversary false and hybridToKEMDistinguisher encryptSym adversary true, plus the DEM advantage of hybridToDEMAdversary keyGen encaps adversary.

theorem Cslib.Crypto.Encryption.advantage_hybridGame_le_two_mul {Msg : Type} (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (n : ℕ) : Game.advantage (game keyGen (hybridEncrypt encaps encryptSym) adversary false n).eval (game keyGen (hybridEncrypt encaps encryptSym) adversary true n).eval ≤ 2 * Game.advantage (kemRealGame keyGen encaps (hybridToKEMHiddenBitDistinguisher encryptSym adversary) n).eval (kemIdealGame keyGen encaps (hybridToKEMHiddenBitDistinguisher encryptSym adversary) n).eval + Game.advantage (demGame encryptSym (hybridToDEMAdversary keyGen encaps adversary) false n).eval (demGame encryptSym (hybridToDEMAdversary keyGen encaps adversary) true n).eval

Quantitative KEM–DEM reduction via a single hidden-bit KEM distinguisher ([BS23], Exercise 11.9(b)): the hybrid IND-CPA advantage is at most twice the KEM advantage of hybridToKEMHiddenBitDistinguisher encryptSym adversary, plus the DEM advantage of hybridToDEMAdversary keyGen encaps adversary.

theorem Cslib.Crypto.Encryption.KEMINDCPA.hybrid_indcpa {Msg : Type} {encMsg : Msg ↪ List Bool} {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} (hkem : KEMINDCPA keyGen encaps) (hdem : DEMOneTimeINDCPAOf encMsg encryptSym) (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) keyGen) (hencaps : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × List Bool) => encaps p.1 p.2) (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) : INDCPAOf encMsg keyGen (hybridEncrypt encaps encryptSym)

IND-CPA security of KEM–DEM hybrid encryption ([BS23], Exercise 11.9(b)): if (keyGen, encaps) is an IND-CPA secure KEM and encryptSym is a one-time IND-CPA secure DEM over encMsg (with uniform strict PPT honest algorithms), then hybridEncrypt encaps encryptSym is IND-CPA secure over encMsg.

theorem Cslib.Crypto.Encryption.eval_demGame_hybridToDEMAdversary_restrict {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (hpk : ∀ (n : ℕ) (pk : List Bool) (m₀ m₁ : Msg), valid n pk m₀ m₁ = valid n [] m₀ m₁) (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : (demGame encryptSym (hybridToDEMAdversary keyGen encaps (AdversaryOf.restrict valid adversary)) bit n).eval = (demGameOn valid encryptSym (hybridToDEMAdversary keyGen encaps (AdversaryOf.restrict valid adversary)) bit n).eval

When valid ignores the public key, running the unrestricted demGame on the DEM adversary built from adversary.restrict valid has the same output distribution as running demGameOn valid on it: an invalid pair already makes the restricted adversary's guess false.

theorem Cslib.Crypto.Encryption.KEMINDCPA.hybrid_indcpaOn {Msg : Type} {encMsg : Msg ↪ List Bool} {valid : ℕ → List Bool → Msg → Msg → Bool} {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} (hkem : KEMINDCPA keyGen encaps) (hdem : DEMOneTimeINDCPAOn valid encMsg encryptSym) (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) (hpk : ∀ (n : ℕ) (pk : List Bool) (m₀ m₁ : Msg), valid n pk m₀ m₁ = valid n [] m₀ m₁) (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) keyGen) (hencaps : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × List Bool) => encaps p.1 p.2) (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) : INDCPAOn valid encMsg keyGen (hybridEncrypt encaps encryptSym)

IND-CPA security of KEM–DEM hybrid encryption under an admissibility predicate ([BS23], Exercise 11.9(b)), for a polynomial-time predicate valid that ignores the public key, such as the equal-length rule: if (keyGen, encaps) is an IND-CPA secure KEM and encryptSym satisfies DEMOneTimeINDCPAOn valid encMsg, then hybridEncrypt encaps encryptSym satisfies INDCPAOn valid encMsg.

Non-vacuous One-Time Pad DEMs

def Cslib.Crypto.Encryption.otpEncrypt : ℕ → (k : List Bool) → (bit : Bool) → ProbComp (List Bool)

One-time pad single-bit symmetric encryption: XOR the first key bit k.headD false with the plaintext bit bit.

def Cslib.Crypto.Encryption.otpDecrypt : ℕ → (k ct : List Bool) → Bool

One-time pad single-bit symmetric decryption: XOR the first key bit k.headD false with the first ciphertext bit ct.headD false.

theorem Cslib.Crypto.Encryption.otpDecrypt_otpEncrypt (n : ℕ) (k : List Bool) (bit : Bool) : otpDecrypt n k [k.headD false ^^ bit] = bit

One-time pad decryption inverts one-time pad encryption on every supported ciphertext.

theorem Cslib.Crypto.Encryption.isPPTOn_otpEncrypt : 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) => otpEncrypt p.1 p.2.1 p.2.2

One-time pad encryption is uniform strict PPT.

theorem Cslib.Crypto.Encryption.computableInPolyTime_otpDecrypt : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => otpDecrypt p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBool

One-time pad decryption is computable in polynomial time.

theorem Cslib.Crypto.Encryption.eval_demGame_otpEncrypt_false_eq_true {n : ℕ} (hn : 1 ≤ n) (adversary : Adversary) : (demGame otpEncrypt adversary false n).eval = (demGame otpEncrypt adversary true n).eval

For 1 ≤ n, a uniform n-bit key masks the challenge bit perfectly in demGame otpEncrypt, so the false and true experiment distributions are identical.

theorem Cslib.Crypto.Encryption.advantage_demGame_otpEncrypt_eq_zero {n : ℕ} (hn : 1 ≤ n) (adversary : Adversary) : Game.advantage (demGame otpEncrypt adversary false n).eval (demGame otpEncrypt adversary true n).eval = 0

For 1 ≤ n, every adversary has exact advantage 0 in demGame otpEncrypt.

theorem Cslib.Crypto.Encryption.demOneTimeINDCPA_otpEncrypt : DEMOneTimeINDCPA otpEncrypt

The one-time pad is unconditionally one-time IND-CPA secure (DEMOneTimeINDCPA otpEncrypt).

theorem Cslib.Crypto.Encryption.KEMINDCPA.hybrid_otpEncrypt_indcpa {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)} (hkem : KEMINDCPA keyGen encaps) (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) keyGen) (hencaps : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × List Bool) => encaps p.1 p.2) : INDCPA keyGen (hybridEncrypt encaps otpEncrypt)

KEM-to-PKE corollary: combining any IND-CPA secure KEM with the one-time pad DEM yields an IND-CPA secure public-key bit-encryption scheme.

def Cslib.Crypto.Encryption.otpWordEncrypt (n : ℕ) (k m : List Bool) : ProbComp (List Bool)

One-time pad n-bit word symmetric encryption: XOR the n-bit key k with the plaintext word m at width n using BitString.listXor n [k, m].

def Cslib.Crypto.Encryption.otpWordDecrypt (n : ℕ) (k ct : List Bool) : List Bool

One-time pad n-bit word symmetric decryption: XOR the n-bit key k with the ciphertext word ct at width n using BitString.listXor n [k, ct].

theorem Cslib.Crypto.Encryption.otpWordDecrypt_otpWordEncrypt {n : ℕ} (k : List Bool) {m : List Bool} (hm : m.length = n) : otpWordDecrypt n k (BitString.listXor n [k, m]) = m

One-time pad word decryption inverts one-time pad word encryption on every n-bit plaintext word m.

theorem Cslib.Crypto.Encryption.isPPTOn_otpWordEncrypt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × List Bool) => otpWordEncrypt p.1 p.2.1 p.2.2

One-time pad word encryption is uniform strict PPT.

theorem Cslib.Crypto.Encryption.computableInPolyTime_otpWordDecrypt : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => otpWordDecrypt p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits

One-time pad word decryption is computable in polynomial time.

theorem Cslib.Crypto.Encryption.eval_demGame_otpWordEncrypt_false_eq_true (n : ℕ) (adversary : WordAdversary) : (demGame otpWordEncrypt adversary false n).eval = (demGame otpWordEncrypt adversary true n).eval

A uniform n-bit key masks any challenge word perfectly in demGame otpWordEncrypt, so the false and true experiment distributions are identical for every n.

theorem Cslib.Crypto.Encryption.advantage_demGame_otpWordEncrypt_eq_zero (n : ℕ) (adversary : WordAdversary) : Game.advantage (demGame otpWordEncrypt adversary false n).eval (demGame otpWordEncrypt adversary true n).eval = 0

Every word adversary has exact advantage 0 in demGame otpWordEncrypt.

theorem Cslib.Crypto.Encryption.demOneTimeINDCPA_otpWordEncrypt : DEMOneTimeINDCPAOf Turing.MultiTapeTM.encBits otpWordEncrypt

The n-bit word one-time pad is unconditionally one-time IND-CPA secure (DEMOneTimeINDCPAOf encBits otpWordEncrypt).

theorem Cslib.Crypto.Encryption.demOneTimeWordINDCPA_otpWordEncrypt : DEMOneTimeWordINDCPA otpWordEncrypt

The n-bit word one-time pad satisfies equal-length word DEM security (DEMOneTimeWordINDCPA otpWordEncrypt).

theorem Cslib.Crypto.Encryption.KEMINDCPA.hybrid_otpWordEncrypt_indcpa {keyGen : ℕ → ProbComp (List Bool × List Bool)} {encaps : ℕ → List Bool → ProbComp (List Bool × List Bool)} (hkem : KEMINDCPA keyGen encaps) (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) keyGen) (hencaps : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × List Bool) => encaps p.1 p.2) : WordINDCPA keyGen (hybridEncrypt encaps otpWordEncrypt)

KEM-to-word-PKE corollary: combining any IND-CPA secure KEM with the n-bit word one-time pad DEM yields a public-key word-encryption scheme satisfying WordINDCPA, through the equal-length instance of KEMINDCPA.hybrid_indcpaOn.