One-Time Pad: Perfect IND-CPA Security

The one-time pad has perfect IND-CPA security. Following Rosulek, The Joy of Cryptography, §2 (one-time secrecy).

This file defines the one-time pad over Bool as a core EncScheme, proves it correct, and shows it achieves perfect IND-CPA security: the IND-CPA advantage of every adversary is exactly 0.

Overview

The one-time pad is the symmetric scheme with Key = Plaintext = Ciphertext = Bool, key generation sampling a uniform bit, and both encryption and decryption given by XOR:

Enc(k, m) = k ⊕ m      Dec(k, c) = k ⊕ c

The security argument is the bijection-coupling technique. For any fixed message m, XOR-by-m is a bijection of the uniform key, so k ⊕ m is uniformly distributed and independent of m. Consequently the two IND-CPA games (encrypting m₀ vs m₁) are each equidistributed with a uniform sample; by transitivity they couple with one another, and INDCPA_Adv_zero_of_rHoare collapses the advantage to 0.

Main definitions

• BoolOTP — the one-time pad as a core EncScheme over Bool.

Main results

• otp_correct — the one-time pad is correct (decrypt (encrypt m k) k = m).
• otp_perfect_indcpa — the one-time pad has perfect IND-CPA security: INDCPA_Adv BoolOTP m₀ m₁ A = 0 for every adversary A.

References

• [Rosulek, The Joy of Cryptography, §2 (one-time secrecy)]
• [Shannon, Communication Theory of Secrecy Systems, 1949]

One-Time Pad Definition

noncomputable def CatCrypt.Examples.OTP.BoolOTP : Crypto.EncScheme

The one-time pad encryption scheme over Bool.

• Key = Plaintext = Ciphertext = Bool
• keyGen samples a uniform bit
• encrypt k m = k ⊕ m
• decrypt k c = some (k ⊕ c)

Equations

• One or more equations did not get rendered due to their size.

Correctness

theorem CatCrypt.Examples.OTP.otp_correct : BoolOTP.Correct

The one-time pad is correct: decryption recovers the message.

Perfect IND-CPA Security

theorem CatCrypt.Examples.OTP.otp_indcpa_coupling (m₀ m₁ : Bool) : Relational.rHoare Relational.eqPre (Crypto.SecurityDefs.INDCPA_Game BoolOTP m₀ m₁ true) (Crypto.SecurityDefs.INDCPA_Game BoolOTP m₀ m₁ false) Relational.eqPost

Coupling: the two IND-CPA games for the one-time pad are equidistributed.

Both encrypt k m₀ and encrypt k m₁ over a uniform key k are equidistributed with a plain uniform sample (XOR-by-a-fixed-message is a bijection of the key), so the real and ideal games couple by transitivity through the uniform sample.

theorem CatCrypt.Examples.OTP.otp_perfect_indcpa (m₀ m₁ : Bool) (A : BoolOTP.Ciphertext → Core.SPComp Bool) : Crypto.SecurityDefs.INDCPA_Adv BoolOTP m₀ m₁ A = 0

The one-time pad has perfect IND-CPA security: every adversary has IND-CPA advantage exactly 0.

Reflection into the Package / UC Stack

The shallow result otp_perfect_indcpa is an empty-heap statement about a single distinguisher applied to the two IND-CPA game bodies. This section lifts it to a composable statement about deep nominal packages linked with an arbitrary adversary package, following the stack shallow game → rawCode% → NomPackage.ofOracle → DeepNomAdvantage → sdist → UC.

The two IND-CPA game bodies INDCPA_Game BoolOTP m₀ m₁ true/false are, after unfolding BoolOTP, the single family k ← sample Bool; pure (k ⊕ m) at the messages m₀ and m₁. Reflecting this family with rawCode% and exporting it as the oracle (1, Unit, Bool) yields the real/ideal package pair. Because XOR-by-m is a bijection of the uniform key, every reflected body evaluates to the same uniform sample, so the two games are indistinguishable against any adversary package — the package-level form of one-time secrecy.

noncomputable def CatCrypt.Examples.OTP.otpGameRaw (m : Bool) : Deep.RawCode Bool

The reflected IND-CPA oracle body for message m: sample a uniform key and return the one-time-pad ciphertext k ⊕ m. Instantiated at m₀ for bit true and m₁ for bit false, this is the whole IND-CPA game family.

Equations

• CatCrypt.Examples.OTP.otpGameRaw m = (CatCrypt.Deep.RawCode.sample Bool).bind fun (k : Bool) => CatCrypt.Deep.RawCode.ret (k ^^ m)

instance CatCrypt.Examples.OTP.instValidOtpGameRaw (m : Bool) : Deep.IsValid ∅ (otpGameRaw m)

theorem CatCrypt.Examples.OTP.otpGameRaw_eval (m : Bool) : (otpGameRaw m).eval = (Core.SPComp.sample Bool).bind fun (k : Bool) => Core.SPComp.pure (k ^^ m)

The reflected body evaluates back to the shallow IND-CPA game body.

theorem CatCrypt.Examples.OTP.otpGameRaw_eval_eq (m : Bool) : (otpGameRaw m).eval = Core.SPComp.sample Bool

The reflected body's evaluation is the uniform sample, independent of m: XOR-by-m is a bijection of the uniform key. This is the distribution-level core of one-time secrecy, here as an SPComp equality.

theorem CatCrypt.Examples.OTP.otpGameRaw_eval_indcpa_true (m₀ m₁ : Bool) : (otpGameRaw m₀).eval = Crypto.SecurityDefs.INDCPA_Game BoolOTP m₀ m₁ true

The reflected body evaluation is the shallow IND-CPA game (bit true at m₀).

theorem CatCrypt.Examples.OTP.otpGameRaw_eval_indcpa_false (m₀ m₁ : Bool) : (otpGameRaw m₁).eval = Crypto.SecurityDefs.INDCPA_Game BoolOTP m₀ m₁ false

The reflected body evaluation is the shallow IND-CPA game (bit false at m₁).

noncomputable def CatCrypt.Examples.OTP.otpGameTrue (m₀ : Bool) : Deep.NomPackage

Real IND-CPA game as an oracle-exporting nominal package: exports the single oracle (1, Unit, Bool), implemented by the reflected body at m₀.

Equations

• CatCrypt.Examples.OTP.otpGameTrue m₀ = CatCrypt.Deep.NomPackage.ofOracle 1 Unit Bool fun (x : Unit) => CatCrypt.Examples.OTP.otpGameRaw m₀

noncomputable def CatCrypt.Examples.OTP.otpGameFalse (m₁ : Bool) : Deep.NomPackage

Ideal IND-CPA game: the same oracle export, implemented by the body at m₁.

Equations

• CatCrypt.Examples.OTP.otpGameFalse m₁ = CatCrypt.Deep.NomPackage.ofOracle 1 Unit Bool fun (x : Unit) => CatCrypt.Examples.OTP.otpGameRaw m₁

theorem CatCrypt.Examples.OTP.otp_eval_eq (m₀ m₁ : Bool) : (otpGameRaw m₀).eval = (otpGameRaw m₁).eval

The two reflected IND-CPA bodies (encrypting m₀ vs m₁) have equal evaluations: each is the uniform sample by otpGameRaw_eval_eq, so they coincide. This single body-.eval equality is what the ReflectUCHelpers ofOracle combinators consume — the whole perfect stack follows from it with no IsPure/NoFail bridge on the adversary.

theorem CatCrypt.Examples.OTP.otp_deepnom_zero (m₀ m₁ : Bool) (A : Deep.NomPackage) : Crypto.DeepNomAdvantage (otpGameTrue m₀) (otpGameFalse m₁) A = 0

Zero deep-nominal advantage against every adversary package. The reflected real/ideal games are perfectly indistinguishable in the deep package model — the package-level form of otp_perfect_indcpa.

theorem CatCrypt.Examples.OTP.otp_nompkg_secure (m₀ m₁ : Bool) : Crypto.NomPkgSecure (otpGameTrue m₀) (otpGameFalse m₁) fun (x : Deep.NomPackage) => 0

Package-level UC security (NomPkgSecure): the reflected one-time pad games emulate each other with zero adversary-dependent error, so the pair composes via NomPkgSecure_trans.

theorem CatCrypt.Examples.OTP.otp_sdist_zero (m₀ m₁ : Bool) : (Crypto.sdist (fun (A : Deep.NomPackage) => Crypto.runPkg (A.pkg.link (otpGameTrue m₀).pkg)) fun (A : Deep.NomPackage) => Crypto.runPkg (A.pkg.link (otpGameFalse m₁).pkg)) = 0

Statistical distance zero between the two linked-game families: the linked runs coincide against every adversary, so sdist_self collapses the distance — no IsPure/NoFail post-processing bridge is needed.

theorem CatCrypt.Examples.OTP.otp_uc (m₀ m₁ : Bool) : Crypto.UCEmulates 0 { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool } (fun (A : { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (Crypto.runPkg (A.pkg.link (otpGameTrue m₀).pkg))) fun (A : { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (Crypto.runPkg (A.pkg.link (otpGameFalse m₁).pkg))

Perfect UC emulation of the linked-game families, over the trivial-leak interface (out = Bool, leak = Empty): the real game UC-emulates the ideal game with error 0 via the identity simulator (composition plumbing).

theorem CatCrypt.Examples.OTP.otp_deepnom_forward_eq_indcpa (m₀ m₁ : Bool) : Crypto.DeepNomAdvantage (otpGameTrue m₀) (otpGameFalse m₁) Deep.forwardAdv = Crypto.SecurityDefs.INDCPA_Adv BoolOTP m₀ m₁ Core.SPComp.pure

Reflection mirrors the shallow game. Against the forwarding adversary, the deep-nominal advantage of the reflected games equals the shallow IND-CPA advantage of BoolOTP under the identity distinguisher — which is 0 by otp_perfect_indcpa. This certifies that the package construction computes the same quantity the shallow proof bounds.