Oracle Diffie-Hellman (ODH) Assumption

This file defines the ODH assumption parametrically over any SampleableType W, following the pattern of DDH.lean.

ODH Game

The ODH assumption (Abdalla-Bellare-Rogaway, CT-RSA 2001) captures the difficulty of distinguishing H(g^{ab}) from random, given (g^a, g^b) and oracle access to H. The simplified formulation used here (following the EasyCrypt pattern) makes the hash oracle implicit: given (g^a, g^b), distinguish hash(ecdh(a, g^b)) from random. When hash is the identity, this reduces to DDH.

At the abstract level with SampleableType W, the ODH game becomes:

• Real: sample a, b, give (pub_a, pub_b, hash(ecdh(a, pub_b), label)) to adversary
• Ideal: sample a, b, r, give (pub_a, pub_b, r) to adversary

Main definitions

• ODHDef — extends DDHDef with a hash function hash : W → W → W
• ODH_Adversary — adversary receiving (pub_a, pub_b, challenge), outputs (label, Bool)
• ODH_Game_Real / ODH_Game_Ideal — the real/ideal ODH games
• ODH_Advantage — advantage of an adversary in breaking ODH
• ODHSecure — security predicate: all adversaries have bounded advantage

Reduction: DDH + PRF ⟹ ODH

The standard reduction (ABR01 Thm 2): if hash is a PRF keyed by the DH secret, then ODH security reduces to DDH + PRF security:

ODH_Advantage ≤ DDH_Advantage + PRF_Advantage

• odh_of_ddh_prf — the reduction theorem (two-hop hybrid via the triangle inequality)

Cross-Validation

Property	This file	EasyCrypt
ODH game	ODH_Game_Real/Ideal	ODH0/ODH1 in ODH.ec
Hash oracle	Implicit (via PRF)	Explicit H.hash oracle
Advantage	Advantage(Real, Ideal)	|Pr[ODH0] - Pr[ODH1]|

References

• Abdalla, Bellare, Rogaway. DHIES: An Encryption Scheme Based on the Diffie-Hellman Problem. CT-RSA 2001, §3.
• Boneh & Shoup, A Graduate Course in Applied Cryptography, §12.4.
• EasyCrypt: assumptions/ODH.ec

ODH Definition

structure CatCrypt.Crypto.Assumptions.ODHDef (W : Type) [SampleableType W] extends CatCrypt.Crypto.Assumptions.DDHDef W : Type

Abstract Oracle Diffie-Hellman definition, extending DDH with a hash function.

• hash secret label models H(g^{ab}, label) — a keyed hash where the DH shared secret acts as the key and label is an auxiliary input.
• When hash is the identity (ignoring label), ODH reduces to DDH.
• When hash is a PRF keyed by the DH secret, ODH follows from DDH + PRF.

• ecdh : W → W → W
• keygen : Core.SPComp (W × W)
• keygen_isPure : self.keygen.IsPure
• hash : W → W → W

  Hash function: hash(dh_secret, label) → output. Models the hash oracle H in the ODH game. The DH shared secret serves as the key; label is the auxiliary input.

ODH Games

@[reducible, inline]

abbrev CatCrypt.Crypto.Assumptions.ODH_Adversary (W : Type) : Type

Type of ODH adversary: receives (pub_a, pub_b, challenge) and must distinguish whether challenge is hash(ecdh(a, pub_b), label) or random.

The adversary outputs (label, bit) where label is the adversary's chosen label for the hash query and bit is the distinguishing guess.

In the simplified formulation, the adversary chooses a label first, then receives the challenge computed at that label. We model this by having the adversary output a pair.

Equations

• CatCrypt.Crypto.Assumptions.ODH_Adversary W = (W → W → W → CatCrypt.Core.SPComp (W × Bool))

noncomputable def CatCrypt.Crypto.Assumptions.ODH_Game_Real {W : Type} [SampleableType W] (D : ODHDef W) (A : ODH_Adversary W) : Core.SPComp Bool

ODH real game: adversary receives (pub_a, pub_b, hash(ecdh(a, pub_b), label)).

The adversary first sees (pub_a, pub_b), outputs (label, _), and the challenge is computed as hash(shared_secret, label). In this simplified formulation, the adversary receives the challenge directly.

Simplified model: The adversary receives (pub_a, pub_b, challenge) and outputs (label, bit). The game computes the challenge using the adversary's label. To avoid circularity, we use a two-phase adversary: phase 1 chooses the label, phase 2 distinguishes. Here we collapse this into a single interaction where the challenge uses a fixed label sampled uniformly.

Equations

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

noncomputable def CatCrypt.Crypto.Assumptions.ODH_Game_Ideal {W : Type} [SampleableType W] (D : ODHDef W) (A : ODH_Adversary W) : Core.SPComp Bool

ODH ideal game: adversary receives (pub_a, pub_b, r) where r is random.

Equations

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

noncomputable def CatCrypt.Crypto.Assumptions.ODH_Advantage {W : Type} [SampleableType W] (D : ODHDef W) (A : ODH_Adversary W) : ENNReal

ODH advantage: ability to distinguish hash(ecdh(a, pub_b), label) from random, given (pub_a, pub_b).

Equations

• CatCrypt.Crypto.Assumptions.ODH_Advantage D A = CatCrypt.Crypto.Advantage (CatCrypt.Crypto.Assumptions.ODH_Game_Real D A) (CatCrypt.Crypto.Assumptions.ODH_Game_Ideal D A)

Security Predicate

def CatCrypt.Crypto.Assumptions.ODHSecure {W : Type} [SampleableType W] (D : ODHDef W) (ε : ENNReal) : Prop

ODH security: all adversaries have bounded distinguishing advantage.

ODHSecure D ε means that for all adversaries A, the advantage of A in the ODH game is at most ε.

Equations

• CatCrypt.Crypto.Assumptions.ODHSecure D ε = ∀ (A : CatCrypt.Crypto.Assumptions.ODH_Adversary W), CatCrypt.Crypto.Assumptions.ODH_Advantage D A ≤ ε

IsPure Proofs

theorem CatCrypt.Crypto.Assumptions.ODH_Game_Real_isPure {W : Type} [SampleableType W] (D : ODHDef W) (A : ODH_Adversary W) (hA : ∀ (x y z : W), (A x y z).IsPure) : (ODH_Game_Real D A).IsPure

theorem CatCrypt.Crypto.Assumptions.ODH_Game_Ideal_isPure {W : Type} [SampleableType W] (D : ODHDef W) (A : ODH_Adversary W) (hA : ∀ (x y z : W), (A x y z).IsPure) : (ODH_Game_Ideal D A).IsPure

Relationship to DDH

When hash is the identity function (ignoring the label), ODH degenerates to DDH. This provides a sanity check on the formulation.

def CatCrypt.Crypto.Assumptions.ODHDef.ofDDH_id {W : Type} [SampleableType W] (D : DDHDef W) : ODHDef W

Any DDH group induces an ODH group with identity hash (ignoring label).

Equations

• CatCrypt.Crypto.Assumptions.ODHDef.ofDDH_id D = { toDDHDef := D, hash := fun (secret _label : W) => secret }

Reduction: DDH + PRF ⟹ ODH

The standard reduction (ABR01, Theorem 2): if the hash function H is a PRF keyed by the DH shared secret, then the ODH advantage is bounded by the sum of the DDH advantage and the PRF advantage.

Proof sketch:

1. Replace ecdh(a, pub_b) with random c (DDH step, cost ε_ddh)
2. Now hash(c, label) with random key c is a PRF evaluation
3. Replace hash(c, label) with random r (PRF step, cost ε_prf)
4. The resulting game is ODH_Game_Ideal

By the triangle inequality: ODH_Advantage ≤ DDH_Advantage + PRF_Advantage

noncomputable def CatCrypt.Crypto.Assumptions.ODH_Hybrid {W : Type} [SampleableType W] (D : ODHDef W) (A : ODH_Adversary W) : Core.SPComp Bool

The hybrid game: replace the DH shared secret with random, but still apply hash. This is the intermediate game in the DDH + PRF ⟹ ODH reduction.

Equations

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

theorem CatCrypt.Crypto.Assumptions.odh_of_ddh_prf {W : Type} [SampleableType W] (D : ODHDef W) (A : ODH_Adversary W) (ε_ddh ε_prf : ENNReal) (h_ddh : ∀ (B : DDH_Adversary W), DDH_Advantage D.toDDHDef B ≤ ε_ddh) (h_prf : Advantage (ODH_Hybrid D A) (ODH_Game_Ideal D A) ≤ ε_prf) : ODH_Advantage D A ≤ ε_ddh + ε_prf

DDH + PRF ⟹ ODH: if hash is a PRF keyed by the DH secret, then the ODH advantage is bounded by the DDH advantage plus the PRF advantage.

• ε_ddh bounds the DDH advantage (cost of replacing ecdh(a, pub_b) with random)
• ε_prf bounds the PRF advantage of hash (cost of replacing hash(c, ·) with random)

The bound is: ODH_Advantage D A ≤ ε_ddh + ε_prf