Oblivious Transfer with Information-Theoretic Sender-Message Privacy

An oblivious-transfer protocol over an abstract discrete-log group in which the sender encrypts each of its two messages under a public key and the receiver recovers only the chosen one. Encryption is ElGamal-style: dualEnc pk m r = pk ^ r · m.

Scope of the security statement

The UC statement here covers corrupt-receiver / sender-message privacy only. The ideal functionality dualOT_ideal reveals the choice bit: it hands the simulator (choice, chosen-ciphertext), so it does not hide which message the receiver selected. Receiver privacy — hiding the choice bit from a corrupt sender — is out of scope; see the closing note.

The simulator dualOT_sim reconstructs the two ciphertexts the real world leaks from (choice, chosen-ciphertext) by sampling a uniform group element for the unchosen slot. It does not use any CRS trapdoor.

Why the unchosen ciphertext is uniform (information-theoretic)

For a public key pk = g ^ s with s ≠ 0 — equivalently, any non-identity element of the prime-order group — the map r ↦ pk ^ r · m is a bijection Scalar ≃ G: it composes r ↦ s · r (a bijection because s ≠ 0), generator exponentiation x ↦ g ^ x (a bijection by exp_surj/exp_inj), and right translation y ↦ y · m (a bijection). Hence for uniform r, dualEnc pk m r is exactly uniform on G. dualEnc_uniform proves this as an equality of distributions, with no computational assumption and no DDH reduction; dualOT_uc_secure_zero threads it into a perfect (ε = 0) UC statement whenever both public keys are non-identity.

Interface types

• leak = G × G — the real world leaks the two ciphertexts.
• sim_if = Bool × G — the ideal hands the simulator the choice bit and the chosen message's ciphertext; the simulator fakes the other ciphertext.

Public Keys and Encryption

structure CatCrypt.Crypto.OT.DualModeOT.DualModeCRS (gp : Examples.GroupParam) : Type

Public keys for the two message slots. mode, sk, and pk_eq record the trapdoor of a full dual-mode CRS (messy vs. decryption mode); they are not used by the sender-message-privacy statement below, which relies only on the two public keys being non-identity, and are retained for the future receiver-privacy extension (see the closing note).

• pk₀ : gp.G

  First public key.

• pk₁ : gp.G

  Second public key.

• mode : Bool

  Mode selector.

• sk : gp.Scalar

  Secret key of the decryptable public key.

• pk_eq : (if self.mode = true then self.pk₀ else self.pk₁) = gp.exp self.sk

  The selected public key is g ^ sk.

def CatCrypt.Crypto.OT.DualModeOT.dualEnc (gp : Examples.GroupParam) (pk m : gp.G) (r : gp.Scalar) : gp.G

Encrypt a group element m under a public key pk with randomness r: pk ^ r · m.

Equations

• CatCrypt.Crypto.OT.DualModeOT.dualEnc gp pk m r = gp.groupMul (gp.groupExp pk r) m

OT Input

structure CatCrypt.Crypto.OT.DualModeOT.OTInput (gp : Examples.GroupParam) : Type

OT input: the sender's two messages and the receiver's choice bit.

• m₀ : gp.G

  The sender's first message.

• m₁ : gp.G

  The sender's second message.

• choice : Bool

  The receiver's choice bit.

Protocol

noncomputable def CatCrypt.Crypto.OT.DualModeOT.dualOT_real (gp : Examples.GroupParam) (crs : DualModeCRS gp) : OTInput gp → Core.SPComp (Unit ⊕ gp.G × gp.G)

Real OT protocol: encrypt both messages under the two public keys.

Equations

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

noncomputable def CatCrypt.Crypto.OT.DualModeOT.dualOT_ideal (gp : Examples.GroupParam) (crs : DualModeCRS gp) : OTInput gp → Core.SPComp (Unit ⊕ Bool × gp.G)

Ideal OT: returns only the chosen message; the simulator interface provides the choice bit and the chosen message's ciphertext.

Equations

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

Simulator

noncomputable def CatCrypt.Crypto.OT.DualModeOT.dualOT_sim (gp : Examples.GroupParam) (_crs : DualModeCRS gp) (V : Type) (A : gp.G × gp.G → Core.SPComp V) : Bool × gp.G → Core.SPComp V

OT simulator: from (choice, ct_chosen) produce a fake pair of ciphertexts, sampling a uniform group element for the unchosen slot.

Equations

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

UC Specification

noncomputable def CatCrypt.Crypto.OT.DualModeOT.dualOTSpec (gp : Examples.GroupParam) (V : Type) : UCSpec

UC spec for the OT: honest input is an OTInput, the real world leaks the two ciphertexts, and the ideal hands the simulator (choice, ciphertext).

Equations

• CatCrypt.Crypto.OT.DualModeOT.dualOTSpec gp V = { hon := CatCrypt.Crypto.OT.DualModeOT.OTInput gp, out := Unit, leak := gp.G × gp.G, sim_if := Bool × gp.G, view := V }

Information-Theoretic Ciphertext Uniformity

For a non-identity public key, encryption with uniform randomness is exactly uniform on the group — an equality of distributions, not a computational bound. The witness is the bijection Scalar ≃ G sending r to pk ^ r · m.

theorem CatCrypt.Crypto.OT.DualModeOT.exists_exp_of_ne_identity (gp : Examples.GroupParam) (pk : gp.G) (h : pk ≠ gp.identity) : ∃ (s : gp.Scalar), s ≠ gp.scalarZero ∧ pk = gp.exp s

In a prime-order group every non-identity element is a generator: any pk ≠ 1 equals g ^ s for some s ≠ 0.

noncomputable def CatCrypt.Crypto.OT.DualModeOT.dualEncEquiv (gp : Examples.GroupParam) (s : gp.Scalar) (m : gp.G) (hs : s ≠ gp.scalarZero) : gp.Scalar ≃ gp.G

The encryption map r ↦ pk ^ r · m as a bijection Scalar ≃ G, for a generator pk = g ^ s with s ≠ 0. It is the composite of r ↦ s · r, generator exponentiation, and right translation by m, each a bijection.

Equations

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

@[simp]

theorem CatCrypt.Crypto.OT.DualModeOT.dualEncEquiv_apply (gp : Examples.GroupParam) (s : gp.Scalar) (m : gp.G) (hs : s ≠ gp.scalarZero) (r : gp.Scalar) : (dualEncEquiv gp s m hs) r = gp.groupMul (gp.exp (gp.scalarMul s r)) m

theorem CatCrypt.Crypto.OT.DualModeOT.dualEnc_uniform (gp : Examples.GroupParam) (pk m : gp.G) (h : pk ≠ gp.identity) : ((Core.SPComp.sample gp.Scalar).bind fun (r : gp.Scalar) => Core.SPComp.pure (dualEnc gp pk m r)) = Core.SPComp.sample gp.G

Ciphertext uniformity. For a non-identity public key pk, encrypting m with uniform randomness is exactly the uniform distribution on the group. Information-theoretic: no assumption, no reduction.

theorem CatCrypt.Crypto.OT.DualModeOT.sdist_dualEnc_uniform (gp : Examples.GroupParam) (pk m : gp.G) (h : pk ≠ gp.identity) : (sdist (fun (x : Unit) => (Core.SPComp.sample gp.Scalar).bind fun (r : gp.Scalar) => Core.SPComp.pure (dualEnc gp pk m r)) fun (x : Unit) => Core.SPComp.sample gp.G) = 0

The sdist form of dualEnc_uniform: encryption under a non-identity key is at statistical distance 0 from a uniform group element.

Ciphertext Pseudorandomness (parametric form)

CiphertextPseudorandom ε is the sdist statement that encryption with uniform randomness is ε-close to a uniform group element, for every key. It is an information-theoretic hiding statement, not a DDH reduction: for any non-identity key it holds at ε = 0 (sdist_dualEnc_uniform). This parametric predicate lets downstream compositions quantify over an abstract bound; the honest, discharged instance is dualOT_uc_secure_zero below.

noncomputable def CatCrypt.Crypto.OT.DualModeOT.CiphertextPseudorandom (gp : Examples.GroupParam) (ε : ENNReal) : Prop

Encryption of m under pk with uniform randomness is sdist-close to a uniform group element, within error ε.

Equations

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

Security Reduction

theorem CatCrypt.Crypto.OT.DualModeOT.dualOT_reduction (gp : Examples.GroupParam) (crs : DualModeCRS gp) (V : Type) (ε : ENNReal) (hb0 : ∀ (m : gp.G), (sdist (fun (x : Unit) => (Core.SPComp.sample gp.Scalar).bind fun (r : gp.Scalar) => Core.SPComp.pure (dualEnc gp crs.pk₀ m r)) fun (x : Unit) => Core.SPComp.sample gp.G) ≤ ε) (hb1 : ∀ (m : gp.G), (sdist (fun (x : Unit) => (Core.SPComp.sample gp.Scalar).bind fun (r : gp.Scalar) => Core.SPComp.pure (dualEnc gp crs.pk₁ m r)) fun (x : Unit) => Core.SPComp.sample gp.G) ≤ ε) : UCEmulates ε (dualOTSpec gp V) (dualOT_real gp crs) (dualOT_ideal gp crs)

The core reduction: given per-key bounds on the statistical distance between a real ciphertext and a uniform group element, the real and ideal OT views are within that bound. The two branches (choice = false/true) share the final step through the local final helper; they differ only in which slot carries the unchosen ciphertext.

Security Proof

theorem CatCrypt.Crypto.OT.DualModeOT.dualOT_uc_secure (gp : Examples.GroupParam) (crs : DualModeCRS gp) (ε : ENNReal) (hcpr : CiphertextPseudorandom gp ε) (V : Type) : UCEmulates ε (dualOTSpec gp V) (dualOT_real gp crs) (dualOT_ideal gp crs)

Sender-message privacy, parametric. For any per-key ciphertext-hiding bound ε (CiphertextPseudorandom), the OT is UC-secure with error ε against a corrupt receiver: the simulator dualOT_sim fakes the unchosen ciphertext with a uniform group element, and the gap between the real unchosen ciphertext and a uniform one is bounded by ε. For concrete non-identity keys this discharges at ε = 0 — see dualOT_uc_secure_zero. (genuine UC)

theorem CatCrypt.Crypto.OT.DualModeOT.dualOT_uc_secure_zero (gp : Examples.GroupParam) (crs : DualModeCRS gp) (h0 : crs.pk₀ ≠ gp.identity) (h1 : crs.pk₁ ≠ gp.identity) (V : Type) : UCEmulates 0 (dualOTSpec gp V) (dualOT_real gp crs) (dualOT_ideal gp crs)

Sender-message privacy, perfect. When both public keys are non-identity (in a prime-order group, both are generators), the OT is perfectly UC-secure against a corrupt receiver: the simulator's uniform group element is exactly the distribution of the real unchosen ciphertext (dualEnc_uniform), so real and ideal views coincide. No assumption, no reduction. (genuine UC)

Nice-to-have: the full dual-mode construction

The statement above is corrupt-receiver / sender-message privacy only, and its simulator ignores the DualModeCRS trapdoor. The genuine Peikert–Vaikuntanathan– Waters dual-mode OT would make the CRS load-bearing and additionally cover the corrupt-sender / receiver-privacy direction:

• Two indistinguishable CRS modes. In messy mode one public key produces ciphertexts statistically independent of the plaintext (enabling extraction of the receiver's choice bit); in decryption mode both keys decrypt correctly (enabling extraction of both sender messages). The two modes are computationally indistinguishable under DDH — this is where a real DDH reduction enters, in contrast to the information-theoretic hiding used here.
• Corrupt receiver (messy CRS). The simulator reads off which key is messy, extracts the choice bit, forwards it to F_OT, and simulates the other ciphertext — using the trapdoor, rather than the dualOT_ideal leak of the choice bit assumed here.
• Corrupt sender (decryption CRS). The simulator decrypts both ciphertexts via sk, extracts both messages, and forwards them to F_OT — the case the present ideal functionality does not model at all.

Realizing this needs a genuine dualOT_ideal that hides the choice bit, a CRS-mode-indistinguishability game, and per-mode simulators; it is not attempted here.

This full account is developed in the larger CatCrypt UC development built on top of this basis (outside this minimal-basis release): an OT/ tree with the F_OT functionality capturing both sender and receiver privacy (FOT), the extraction machinery, and the plain-model impossibility (PlainModelOTImpossibility). This file is the self-contained corrupt-receiver / sender-privacy exemplar.