Naor-Pinkas Oblivious Transfer (OT)

This file formalizes the Naor-Pinkas (2001) DDH-based 1-out-of-2 OT protocol and proves both sender security (information-theoretic) and receiver security (DDH-based).

Protocol

The receiver holds a choice bit σ ∈ {0,1}. The sender holds messages m₀, m₁ ∈ G.

1. Receiver: Sample a, b, c from Exp. Send (g^a, g^b, z₀, z₁) where z_σ = g^{ab} (DDH triple) and z_{1-σ} = g^c (random).

2. Sender: For each i ∈ {0,1}, sample (sᵢ, rᵢ), compute wᵢ = g^{a·sᵢ + rᵢ} and eᵢ = g^{dᵢ·sᵢ + b·rᵢ} · mᵢ where dᵢ is the exponent of zᵢ.

3. Receiver: Decrypt m_σ using s_σ, r_σ (the DDH position is decryptable).

Security

Sender security: When d ≠ ab (non-DDH position), the map (s, r) ↦ (as + r, ds + br) is a bijection on Exp × Exp, so (wᵢ, eᵢ) is uniformly distributed and the message is information-theoretically hidden (otEnc_message_independent). The honest receiver samples c uniformly, so c = ab occurs with probability 1 / |Exp|; ot_sender_secure bounds the real/ideal advantage by that probability.

Receiver security: The receiver's public values (g^a, g^b, z₀, z₁) contain a DDH triple at the choice position. Distinguishing σ=0 from σ=1 reduces to DDH.

References

• Naor & Pinkas, "Efficient Oblivious Transfer Protocols", SODA 2001
• EasyCrypt: beschmi/oblivious_transfer
• CryptHOL: Multi_Party_Computation AFP entry

CyclicGroupRing: Exponent Ring Structure

The sender security proof requires the matrix map (s,r) ↦ (as+r, ds+br) to be a bijection when d ≠ ab. This needs ring structure on exponents (addition, multiplication, distributivity) beyond what CyclicGroup provides.

class CatCrypt.Examples.OT.CyclicGroupRing (G : Type) extends CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup G : Type 1

Extension of CyclicGroup with ring structure on exponents.

The key new operations are expAdd (addition in Z_q) and the distributivity law expMul a (expAdd b c) = expAdd (expMul a b) (expMul a c). The crucial expMul_bij ensures multiplication by a nonzero element is bijective.

• Exp : Type
• finG : Fintype G
• neG : Nonempty G
• finExp : Fintype (Exp G)
• neExp : Nonempty (Exp G)
• gen : G
• pow : Exp G → G
• mul : G → G → G
• inv : G → G
• expMul : Exp G → Exp G → Exp G
• expNeg : Exp G → Exp G
• one : G
• pow_comm (a b : Exp G) : pow (expMul a b) = pow (expMul b a)
• mul_assoc (x y z : G) : mul (mul x y) z = mul x (mul y z)
• mul_comm (x y : G) : mul x y = mul y x
• mul_inv (x : G) : mul x (inv x) = one
• mul_one (x : G) : mul x one = x
• pow_bij : Function.Bijective pow
• expAdd : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G → CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G → CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G

  Addition of exponents

• expZero : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G

  Zero exponent

• pow_add (a b : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.pow (expAdd a b) = CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.mul (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.pow a) (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.pow b)

  g^(a+b) = g^a · g^b

• pow_zero : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.pow expZero = CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.one

  g^0 = 1

• expAdd_comm (a b : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : expAdd a b = expAdd b a

  Addition is commutative

• expAdd_assoc (a b c : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : expAdd (expAdd a b) c = expAdd a (expAdd b c)

  Addition is associative

• expAdd_zero (a : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : expAdd a expZero = a

  Right identity for addition

• expAdd_neg (a : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : expAdd a (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expNeg a) = expZero

  Additive inverse: a + (-a) = 0

• expMul_comm' (a b : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a b = CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul b a

  Multiplication is commutative

• expMul_add (a b c : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a (expAdd b c) = expAdd (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a b) (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a c)

  Left distributivity: a(b+c) = ab + ac

• expMul_assoc (a b c : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a b) c = CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul b c)

  Multiplication is associative

• expMul_bij (d : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : d ≠ expZero → Function.Bijective (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul d)

  Multiplication by nonzero is bijective (prime-order group)

@[reducible, inline]

abbrev CatCrypt.Examples.OT.CyclicGroupRing.expSub {G : Type} [CGR : CyclicGroupRing G] (a b : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G

Subtraction of exponents: a - b := a + (-b)

Equations

• CatCrypt.Examples.OT.CyclicGroupRing.expSub a b = CatCrypt.Examples.OT.CyclicGroupRing.expAdd a (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expNeg b)

theorem CatCrypt.Examples.OT.CyclicGroupRing.expZero_add {G : Type} [CGR : CyclicGroupRing G] (a : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : expAdd expZero a = a

Left identity for addition: 0 + a = a

theorem CatCrypt.Examples.OT.CyclicGroupRing.pow_neg {G : Type} [CGR : CyclicGroupRing G] (a : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.pow (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expNeg a) = CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.inv (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.pow a)

g^(-a) = (g^a)⁻¹

theorem CatCrypt.Examples.OT.CyclicGroupRing.expAdd_cancel_right {G : Type} [CGR : CyclicGroupRing G] (a b c : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) (h : expAdd a c = expAdd b c) : a = b

Additive right cancellation: a + c = b + c → a = b

theorem CatCrypt.Examples.OT.CyclicGroupRing.expAdd_cancel_left {G : Type} [CGR : CyclicGroupRing G] (c a b : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) (h : expAdd c a = expAdd c b) : a = b

Additive left cancellation: c + a = c + b → a = b

theorem CatCrypt.Examples.OT.CyclicGroupRing.expAdd_mul {G : Type} [CGR : CyclicGroupRing G] (a b c : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul (expAdd a b) c = expAdd (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a c) (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul b c)

Right distributivity: (a+b)c = ac + bc

theorem CatCrypt.Examples.OT.CyclicGroupRing.expMul_zero {G : Type} [CGR : CyclicGroupRing G] (a : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul expZero a = expZero

0 · a = 0

theorem CatCrypt.Examples.OT.CyclicGroupRing.expZero_mul {G : Type} [CGR : CyclicGroupRing G] (a : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a expZero = expZero

a · 0 = 0

theorem CatCrypt.Examples.OT.CyclicGroupRing.expMul_neg {G : Type} [CGR : CyclicGroupRing G] (a b : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expNeg b) = CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expNeg (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a b)

a · (-b) = -(a · b)

theorem CatCrypt.Examples.OT.CyclicGroupRing.neg_expMul {G : Type} [CGR : CyclicGroupRing G] (a b : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expNeg a) b = CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expNeg (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a b)

(-a) · b = -(a · b)

theorem CatCrypt.Examples.OT.CyclicGroupRing.expSub_self {G : Type} [CGR : CyclicGroupRing G] (a : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : expSub a a = expZero

expSub a a = 0

theorem CatCrypt.Examples.OT.CyclicGroupRing.expSub_add {G : Type} [CGR : CyclicGroupRing G] (a b : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : expAdd (expSub a b) b = a

Recovering from sub: expAdd (expSub a b) b = a

Protocol Definitions

noncomputable def CatCrypt.Examples.OT.otEnc {G : Type} [CGR : CyclicGroupRing G] (a b d : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) (m : G) : Core.SPComp (G × G)

Sender encryption for one position.

Given exponents (a, b, d) corresponding to (x = g^a, y = g^b, z = g^d), encrypt message m by sampling (s, r) and computing:

• w = g^{as + r} (mask for receiver)
• e = g^{ds + br} · m (encrypted message)

When d = ab (DDH position), the receiver who knows s can compute g^{ds+br} and decrypt. When d ≠ ab, the pair (w, e) is uniform — m is hidden.

Equations

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

@[reducible, inline]

abbrev CatCrypt.Examples.OT.OTTranscript (G : Type) [_CG : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup G] : Type

OT transcript: public keys + two ciphertexts

Equations

• CatCrypt.Examples.OT.OTTranscript G = (G × G × (G × G) × G × G)

noncomputable def CatCrypt.Examples.OT.ot_real {G : Type} [CGR : CyclicGroupRing G] (m0 m1 : G) (sigma : Bool) : Core.SPComp (OTTranscript G)

Real OT game: both messages are encrypted normally (no adversary substitution).

Equations

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

noncomputable def CatCrypt.Examples.OT.ot_ideal {G : Type} [CGR : CyclicGroupRing G] (m0 m1 : G) (sigma : Bool) : Core.SPComp (OTTranscript G)

Ideal OT game: the non-chosen message is replaced by the identity.

Equations

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

theorem CatCrypt.Examples.OT.otEnc_isPure {G : Type} [CGR : CyclicGroupRing G] (a b d : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) (m : G) : (otEnc a b d m).IsPure

The Naor-Pinkas encryption step otEnc does not read or write the heap.

theorem CatCrypt.Examples.OT.ot_real_isPure {G : Type} [CGR : CyclicGroupRing G] (m0 m1 : G) (sigma : Bool) : (ot_real m0 m1 sigma).IsPure

The real OT game ot_real does not read or write the heap.

theorem CatCrypt.Examples.OT.ot_ideal_isPure {G : Type} [CGR : CyclicGroupRing G] (m0 m1 : G) (sigma : Bool) : (ot_ideal m0 m1 sigma).IsPure

The ideal OT game ot_ideal does not read or write the heap.

Matrix Bijection

The key algebraic fact for sender security: the linear map M(s, r) = (as + r, ds + br) on Exp × Exp is a bijection when d - ab ≠ 0.

noncomputable def CatCrypt.Examples.OT.matrixMap {G : Type} [CGR : CyclicGroupRing G] (a b d : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G × CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G → CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G × CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G

The matrix map (s, r) ↦ (as + r, ds + br) on exponents.

Equations

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

theorem CatCrypt.Examples.OT.matrixMap_injective {G : Type} [CGR : CyclicGroupRing G] (a b d : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) (hnd : CyclicGroupRing.expSub d (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a b) ≠ CyclicGroupRing.expZero) : Function.Injective (matrixMap a b d)

The matrix map is injective when d - ab ≠ 0.

theorem CatCrypt.Examples.OT.matrixMap_bijective {G : Type} [CGR : CyclicGroupRing G] (a b d : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) (hnd : CyclicGroupRing.expSub d (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a b) ≠ CyclicGroupRing.expZero) : Function.Bijective (matrixMap a b d)

The matrix map is bijective when d - ab ≠ 0.

Sender Security

The key theorem: when d ≠ ab, the encryption otEnc a b d m produces a distribution independent of m. This is because the matrix map (s,r) ↦ (as+r, ds+br) is a bijection, so (w, e) is uniformly distributed.

noncomputable def CatCrypt.Examples.OT.expAddEquiv {G : Type} [CGR : CyclicGroupRing G] (c : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G ≃ CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G

Translation equivalence on exponents: s ↦ s + c.

Equations

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

theorem CatCrypt.Examples.OT.otEnc_message_independent {G : Type} [CGR : CyclicGroupRing G] (a b d : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G) (m0 m1 : G) (hnd : CyclicGroupRing.expSub d (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.expMul a b) ≠ CyclicGroupRing.expZero) : otEnc a b d m0 = otEnc a b d m1

Key lemma: otEnc a b d m0 = otEnc a b d m1 when d - ab ≠ 0.

The proof uses a translation coupling. When d - ab ≠ 0, we can find a constant shift δ such that coupling s₀ ↔ s₀ + δ and r₀ ↔ r₀ - aδ preserves the first output component g^{as+r} and exactly compensates the message change in the second component g^{ds+br} · m.

theorem CatCrypt.Examples.OT.expSub_ne_zero_of_ne {G : Type} [CGR : CyclicGroupRing G] {c d : CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G} (h : c ≠ d) : CyclicGroupRing.expSub c d ≠ CyclicGroupRing.expZero

c ≠ d implies c - d ≠ 0 on exponents.

theorem CatCrypt.Examples.OT.advantageA_sample_bind_le_of_eq_off {α β : Type} [Fintype α] [Nonempty α] (f g : α → Core.SPComp β) (A : β → Core.SPComp Bool) (x₀ : α) (h : ∀ (x : α), x ≠ x₀ → f x = g x) : Crypto.AdvantageA ((Core.SPComp.sample α).bind f) ((Core.SPComp.sample α).bind g) A ≤ (↑(Fintype.card α))⁻¹

Sampling a uniform x and continuing with f x or with g x gives an advantage of at most 1 / |α| against every distinguisher, when f and g agree at every point except x₀.

theorem CatCrypt.Examples.OT.ot_sender_secure {G : Type} [CGR : CyclicGroupRing G] (m0 m1 : G) (sigma : Bool) (A : OTTranscript G → Core.SPComp Bool) : Crypto.AdvantageA (ot_real m0 m1 sigma) (ot_ideal m0 m1 sigma) A ≤ (↑(Fintype.card (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G)))⁻¹

Sender security of Naor–Pinkas OT, statistical form.

For every distinguisher A and every choice bit sigma, the real transcript (both messages encrypted) and the ideal transcript (the unchosen message replaced by the identity) are at advantage at most 1 / |Exp|. The two games coincide on every receiver sample with c ≠ a·b (otEnc_message_independent); the term 1 / |Exp| is the probability of the event c = a·b, on which the unchosen position is a DDH triple and its message is decryptable.

Receiver Security

The receiver's public values (g^a, g^b, z₀, z₁) encode the choice bit σ: position σ has a DDH triple (g^a, g^b, g^{ab}), the other has a random g^c.

Distinguishing σ=0 from σ=1 reduces to DDH via a standard hybrid argument.

noncomputable def CatCrypt.Examples.OT.receiverView {G : Type} [CGR : CyclicGroupRing G] (sigma : Bool) : Core.SPComp (G × G × G × G)

Receiver's view: what the sender sees (the public commitment).

Equations

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

noncomputable def CatCrypt.Examples.OT.receiverReduction {G : Type} [CGR : CyclicGroupRing G] (sigma : Bool) (A : G × G × G × G → Core.SPComp Bool) (challenge : CatCryptCore.Examples.CyclicGroupDDH.DDHTriple G) : Core.SPComp Bool

DDH reduction for receiver security.

Equations

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

theorem CatCrypt.Examples.OT.pure_eq_spcomp_pure {α : Type} (a : α) : pure a = Core.SPComp.pure a

Bridge lemma: monad pure equals SPComp.pure for simp matching.

theorem CatCrypt.Examples.OT.reduction_real_eq_receiver {G : Type} [CGR : CyclicGroupRing G] (sigma : Bool) (A : G × G × G × G → Core.SPComp Bool) : (CatCryptCore.Examples.CyclicGroupDDH.DDH_real G).bind (receiverReduction sigma A) = (receiverView sigma).bind A

The reduction with real DDH matches the receiver's view.

theorem CatCrypt.Examples.OT.receiver_ideal_indep {G : Type} [CGR : CyclicGroupRing G] (A : G × G × G × G → Core.SPComp Bool) : (CatCryptCore.Examples.CyclicGroupDDH.DDH_ideal G).bind (receiverReduction false A) = (CatCryptCore.Examples.CyclicGroupDDH.DDH_ideal G).bind (receiverReduction true A)

When DDH is ideal (z random), both σ values give the same distribution.

theorem CatCrypt.Examples.OT.receiver_security {G : Type} [CGR : CyclicGroupRing G] (A : G × G × G × G → Core.SPComp Bool) : Crypto.AdvantageA (receiverView false) (receiverView true) A ≤ CatCryptCore.Examples.CyclicGroupDDH.DDH_Advantage G (receiverReduction false A) + CatCryptCore.Examples.CyclicGroupDDH.DDH_Advantage G (receiverReduction true A)

Receiver security: the advantage of distinguishing σ=0 from σ=1 is bounded by the sum of two DDH advantages.