Composed Fujisaki-Okamoto Transform

This file exposes the composed two-RO Fujisaki-Okamoto transform together with a single-RO specialization for the H(m) branch.

def FujisakiOkamoto {M PK SK R C KD K : Type} (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (policy : FujisakiOkamoto.RejectionPolicy K C) [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] : KEMScheme (OracleComp (UTransform.oracleSpec M R KD K)) K PK ((PK × SK) × policy.FallbackState) C

The canonical two-RO Fujisaki-Okamoto family is the U-transform instantiated with a variant-specific key-derivation input and rejection policy.

@[reducible, inline]

abbrev FujisakiOkamoto.singleROHashOracleSpec (PKHash M R K : Type) : OracleSpec (PKHash × M)

The hash-oracle interface for the single-RO FO variant: one public oracle maps (pkh pk, m) to both encryption coins and the shared key.

@[reducible, inline]

abbrev FujisakiOkamoto.singleROOracleSpec (PKHash M R K : Type) : OracleSpec (ℕ ⊕ PKHash × M)

The full oracle world for the single-RO FO variant, consisting of unrestricted public randomness plus the combined (pkh pk, m) ↦ (r, k) random oracle.

@[reducible, inline]

abbrev FujisakiOkamoto.SingleROQueryCache (PKHash M R K : Type) : Type

Cache state for the single lazy random oracle used by the single-RO FO variant.

def FujisakiOkamoto.singleROOracleImpl {PKHash M R K : Type} [DecidableEq PKHash] [DecidableEq M] [SampleableType R] [SampleableType K] : QueryImpl (singleROHashOracleSpec PKHash M R K) (StateT (SingleROQueryCache PKHash M R K) ProbComp)

Lazy single random oracle returning both coins and the derived key.

def FujisakiOkamoto.singleROVariant {M PK R C K PKHash : Type} (pkh : PK → PKHash) [DecidableEq PKHash] [DecidableEq M] [SampleableType R] [SampleableType K] : Variant (singleROHashOracleSpec PKHash M R K) M PK C R K

Single-RO FO hash world: both the encryption coins and the shared key are derived from the same public random-oracle query on (pkh pk, msg).

def FujisakiOkamoto.singleRO {M PK SK R C K PKHash : Type} (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (pkh : PK → PKHash) (policy : RejectionPolicy K C) [DecidableEq PKHash] [DecidableEq M] [DecidableEq C] [SampleableType M] [SampleableType R] [SampleableType K] : KEMScheme (OracleComp (singleROOracleSpec PKHash M R K)) K PK ((PK × SK) × policy.FallbackState) C

Single-RO specialization for the H(m) branch. The oracle input is (pkh pk, m) and the oracle output supplies both the encryption coins and the shared key.

noncomputable def FujisakiOkamoto.twoRORuntime {M R KD K : Type} [DecidableEq M] [DecidableEq KD] [SampleableType R] [SampleableType K] : ProbCompRuntime (OracleComp (UTransform.oracleSpec M R KD K))

Runtime bundle for the canonical two-RO Fujisaki-Okamoto oracle world.

noncomputable def FujisakiOkamoto.singleRORuntime {M R K PKHash : Type} [DecidableEq PKHash] [DecidableEq M] [SampleableType R] [SampleableType K] : ProbCompRuntime (OracleComp (singleROOracleSpec PKHash M R K))

Runtime bundle for the single-RO Fujisaki-Okamoto oracle world.

theorem FujisakiOkamoto.IND_CCA_bound {M PK SK R C KD K KPRF : Type} [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (prf : PRFScheme KPRF C K) (adversary : (FujisakiOkamoto pke kdInput (implicitRejection prf)).IND_CCA_Adversary) (correctnessBound epsMsg : ℝ) (qHK : ℕ) : ∃ (cpaAdv₁ : (pke.toAsymmEncAlg ProbCompRuntime.probComp).IND_CPA_adversary) (cpaAdv₂ : (pke.toAsymmEncAlg ProbCompRuntime.probComp).IND_CPA_adversary) (prfAdv : PRFScheme.PRFAdversary C K), KEMScheme.IND_CCA_Advantage twoRORuntime adversary ≤ 2 * (AsymmEncAlg.IND_CPA_advantage cpaAdv₁).toReal + 2 * (AsymmEncAlg.IND_CPA_advantage cpaAdv₂).toReal + prf.prfAdvantage prfAdv + ↑(2 * qHK + 3) * correctnessBound + 2 * ↑(2 * qHK + 2) * epsMsg

Main composed Fujisaki-Okamoto IND-CCA theorem statement.

WARNING: this is a placeholder statement, not the final theorem. The current shape is unsound as written: correctnessBound and epsMsg are unconstrained ℝ parameters, so the right-hand side can be made arbitrarily negative while the left-hand side is a probability and hence nonnegative. In the final composed FO statement these slack terms must be constrained (correctnessBound is the underlying PKE's δ-correctness error, and epsMsg is the message-distribution collision/min-entropy term, both provably nonnegative quantities derived from pke).

The proof is intentionally deferred. The reduction artifacts (cpaAdv₁, cpaAdv₂, prfAdv) are existentially quantified rather than passed in as unrelated inputs, but the bound itself still needs to be tightened before this can be a meaningful security claim.