Fujisaki-Okamoto U Transform

This file defines the U-transform family on top of the T-transform oracle world.

structure FujisakiOkamoto.Variant {ι : Type} (hashOracleSpec : OracleSpec ι) (M PK C R K : Type) : Type (v + 1)

A reusable FO hash world packages the public hash-oracle interface together with the variant-specific ways of deriving encryption coins and shared keys.

• QueryCache : Type
• initCache : self.QueryCache
• queryImpl : QueryImpl hashOracleSpec (StateT self.QueryCache ProbComp)
• deriveCoins {m : Type → Type v} [Monad m] [MonadLiftT ProbComp m] [HasQuery hashOracleSpec m] : PK → M → m R
• deriveKey {m : Type → Type v} [Monad m] [MonadLiftT ProbComp m] [HasQuery hashOracleSpec m] : PK → M → C → m K

structure FujisakiOkamoto.RejectionPolicy (K C : Type) : Type 1

Rejection behavior is factored out from the FO hash world so explicit and implicit rejection share the same core construction.

• FallbackState : Type
• keygen : ProbComp self.FallbackState
• onReject : self.FallbackState → C → Option K

def FujisakiOkamoto.explicitRejection {K C : Type} : RejectionPolicy K C

Explicit rejection returns none and carries no extra secret state.

def FujisakiOkamoto.implicitRejection {K C KPRF : Type} (prf : PRFScheme KPRF C K) : RejectionPolicy K C

Implicit rejection stores a PRF key and derives a fallback shared key from the ciphertext.

noncomputable def FujisakiOkamoto.spmfSemantics {ι : Type} {hashOracleSpec : OracleSpec ι} {M PK C R K : Type} (variant : Variant hashOracleSpec M PK C R K) : SPMFSemantics (OracleComp (unifSpec + hashOracleSpec))

Bundled subprobabilistic semantics for an FO hash world, obtained by hiding the variant-specific cache after running the public-randomness-plus-hash simulation.

noncomputable def FujisakiOkamoto.runtime {ι : Type} {hashOracleSpec : OracleSpec ι} {M PK C R K : Type} (variant : Variant hashOracleSpec M PK C R K) : ProbCompRuntime (OracleComp (unifSpec + hashOracleSpec))

Full public-randomness runtime for an FO hash world.

def FujisakiOkamoto.scheme {ι : Type} {hashOracleSpec : OracleSpec ι} {M PK SK R C K : Type} {m : Type → Type v} [Monad m] [MonadLiftT ProbComp m] (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (variant : Variant hashOracleSpec M PK C R K) (policy : RejectionPolicy K C) [SampleableType M] [DecidableEq C] [HasQuery hashOracleSpec m] : KEMScheme m K PK ((PK × SK) × policy.FallbackState) C

Generic FO construction parameterized by a hash world and a rejection policy.

@[reducible, inline]

abbrev UTransform.hashOracleSpec (M R KD K : Type) : OracleSpec (M ⊕ KD)

The public hash-oracle interface for the two-RO U-transform: one oracle derives encryption coins from plaintexts and the other derives shared keys from the chosen derivation input.

@[reducible, inline]

abbrev UTransform.oracleSpec (M R KD K : Type) : OracleSpec (ℕ ⊕ M ⊕ KD)

The full oracle world for the U-transform, consisting of unrestricted public randomness plus the two public hash oracles.

@[reducible, inline]

abbrev UTransform.QueryCache (M R KD K : Type) : Type

Cache state for the U-transform's two lazy random oracles.

def UTransform.coinOracleImpl {M R KD K : Type} [DecidableEq M] [SampleableType R] : QueryImpl (OracleSpec.ofFn fun (x : M) => R) (StateT (QueryCache M R KD K) ProbComp)

Lazy random oracle for encryption coins, threaded through the combined U-transform state.

def UTransform.keyOracleImpl {M R KD K : Type} [DecidableEq KD] [SampleableType K] : QueryImpl (OracleSpec.ofFn fun (x : KD) => K) (StateT (QueryCache M R KD K) ProbComp)

Lazy random oracle for key derivation, threaded through the combined U-transform state.

def UTransform.queryImpl {M R KD K : Type} [DecidableEq M] [DecidableEq KD] [SampleableType R] [SampleableType K] : QueryImpl (hashOracleSpec M R KD K) (StateT (QueryCache M R KD K) ProbComp)

Query implementation for the full two-RO FO hash world.

def UTransform.variant {M PK C R KD K : Type} (kdInput : M → C → KD) [DecidableEq M] [DecidableEq KD] [SampleableType R] [SampleableType K] : FujisakiOkamoto.Variant (hashOracleSpec M R KD K) M PK C R K

Two-RO FO hash world: one oracle derives coins from the message, the other derives the shared key from a variant-chosen encoding of (m, c).

def UTransform {M PK SK R C KD K : Type} {m : Type → Type v} [Monad m] [MonadLiftT ProbComp m] (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] [HasQuery (UTransform.hashOracleSpec M R KD K) m] : KEMScheme m K PK ((PK × SK) × policy.FallbackState) C

The generic two-RO U-transform family. The argument kdInput chooses whether the shared key is derived from m, (m, c), or some other encoding of the recovered plaintext and ciphertext.

theorem UTransform.encaps_usesExactFamilyWeightedCost {M PK SK R C KD K : Type} [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] (runtime : QueryRuntime (hashOracleSpec M R KD K) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (policy : FujisakiOkamoto.RejectionPolicy K C) (pk : PK) (costFn : (hashOracleSpec M R KD K).Domain → ω) (wCoins wKey : ω) (hCoins : ∀ (msg : M), costFn (Sum.inl msg) = wCoins) (hKeys : ∀ (kd : KD), costFn (Sum.inr kd) = wKey) : HasQuery.UsesCostExactly (fun [HasQuery (hashOracleSpec M R KD K) (AddWriterT ω m)] => (UTransform pke kdInput policy).encaps pk) runtime costFn (wCoins + wKey)

If each of the two U-transform oracle families is assigned a constant weight, encapsulation incurs exactly the sum of those family weights.

theorem UTransform.encaps_usesWeightedQueryCostAtMost {M PK SK R C KD K : Type} [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [IsOrderedAddMonoid ω] [HasEvalSet m] (runtime : QueryRuntime (hashOracleSpec M R KD K) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (policy : FujisakiOkamoto.RejectionPolicy K C) (pk : PK) (costFn : (hashOracleSpec M R KD K).Domain → ω) (wCoins wKey : ω) (hCoins : ∀ (msg : M), costFn (Sum.inl msg) ≤ wCoins) (hKeys : ∀ (kd : KD), costFn (Sum.inr kd) ≤ wKey) : HasQuery.UsesCostAtMost (fun [HasQuery (hashOracleSpec M R KD K) (AddWriterT ω m)] => (UTransform pke kdInput policy).encaps pk) runtime costFn (wCoins + wKey)

Under per-family upper bounds on the two U-transform oracle families, encapsulation incurs weighted query cost at most the sum of those bounds.

theorem UTransform.encaps_usesExactlyTwoQueries {M PK SK R C KD K : Type} [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (runtime : QueryRuntime (hashOracleSpec M R KD K) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (policy : FujisakiOkamoto.RejectionPolicy K C) (pk : PK) : HasQuery.UsesExactlyQueries (fun [HasQuery (hashOracleSpec M R KD K) (AddWriterT ℕ m)] => (UTransform pke kdInput policy).encaps pk) runtime 2

Unit-cost specialization: U-transform encapsulation always makes exactly two oracle queries, one to derive coins and one to derive the shared key.

theorem UTransform.encaps_expectedQueryCost_eq_of_constantOracleWeights {M PK SK R C KD K : Type} [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] [Preorder ω] [HasEvalPMF m] (runtime : QueryRuntime (hashOracleSpec M R KD K) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (policy : FujisakiOkamoto.RejectionPolicy K C) (pk : PK) (costFn : (hashOracleSpec M R KD K).Domain → ω) (wCoins wKey : ω) (val : ω → ENNReal) (hval : Monotone val) (hCoins : ∀ (msg : M), costFn (Sum.inl msg) = wCoins) (hKeys : ∀ (kd : KD), costFn (Sum.inr kd) = wKey) : HasQuery.expectedQueryCost (fun [HasQuery (hashOracleSpec M R KD K) (AddWriterT ω m)] => (UTransform pke kdInput policy).encaps pk) runtime costFn val = val (wCoins + wKey)

Expected weighted query cost of U-transform encapsulation under constant per-family weights.

theorem UTransform.encaps_expectedQueryCost_le {M PK SK R C KD K : Type} [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [IsOrderedAddMonoid ω] [HasEvalPMF m] (runtime : QueryRuntime (hashOracleSpec M R KD K) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (policy : FujisakiOkamoto.RejectionPolicy K C) (pk : PK) (costFn : (hashOracleSpec M R KD K).Domain → ω) (wCoins wKey : ω) (val : ω → ENNReal) (hval : Monotone val) (hCoins : ∀ (msg : M), costFn (Sum.inl msg) ≤ wCoins) (hKeys : ∀ (kd : KD), costFn (Sum.inr kd) ≤ wKey) : HasQuery.expectedQueryCost (fun [HasQuery (hashOracleSpec M R KD K) (AddWriterT ω m)] => (UTransform pke kdInput policy).encaps pk) runtime costFn val ≤ val (wCoins + wKey)

Expected weighted query cost of U-transform encapsulation is bounded by the sum of the per-family bounds.

theorem UTransform.encaps_expectedQueries_eq_two {M PK SK R C KD K : Type} [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] [HasEvalPMF m] (runtime : QueryRuntime (hashOracleSpec M R KD K) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (policy : FujisakiOkamoto.RejectionPolicy K C) (pk : PK) : HasQuery.expectedQueries (fun [HasQuery (hashOracleSpec M R KD K) (AddWriterT ℕ m)] => (UTransform pke kdInput policy).encaps pk) runtime = 2

Expected query count of U-transform encapsulation is exactly 2.

theorem UTransform.decaps_usesZeroQueryCost_of_decrypt_eq_none {M PK SK R C KD K : Type} [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] (runtime : QueryRuntime (hashOracleSpec M R KD K) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (policy : FujisakiOkamoto.RejectionPolicy K C) (pk : PK) (sk : SK) (fb : policy.FallbackState) (c : C) (costFn : (hashOracleSpec M R KD K).Domain → ω) (hdec : pke.decrypt sk c = none) : HasQuery.UsesCostExactly (fun [HasQuery (hashOracleSpec M R KD K) (AddWriterT ω m)] => (UTransform pke kdInput policy).decaps ((pk, sk), fb) c) runtime costFn 0

If deterministic decryption fails immediately, U-transform decapsulation incurs zero weighted query cost.

theorem UTransform.decaps_usesWeightedQueryCostAtMost {M PK SK R C KD K : Type} [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [IsOrderedAddMonoid ω] [CanonicallyOrderedAdd ω] [HasEvalSet m] (runtime : QueryRuntime (hashOracleSpec M R KD K) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (policy : FujisakiOkamoto.RejectionPolicy K C) (pk : PK) (sk : SK) (fb : policy.FallbackState) (c : C) (costFn : (hashOracleSpec M R KD K).Domain → ω) (wCoins wKey : ω) (hCoins : ∀ (msg : M), costFn (Sum.inl msg) ≤ wCoins) (hKeys : ∀ (kd : KD), costFn (Sum.inr kd) ≤ wKey) : HasQuery.UsesCostAtMost (fun [HasQuery (hashOracleSpec M R KD K) (AddWriterT ω m)] => (UTransform pke kdInput policy).decaps ((pk, sk), fb) c) runtime costFn (wCoins + wKey)

Under per-family upper bounds on the two U-transform oracle families, decapsulation incurs weighted query cost at most the sum of those bounds.

theorem UTransform.decaps_expectedQueryCost_eq_zero_of_decrypt_eq_none {M PK SK R C KD K : Type} [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] [Preorder ω] [HasEvalPMF m] (runtime : QueryRuntime (hashOracleSpec M R KD K) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (policy : FujisakiOkamoto.RejectionPolicy K C) (pk : PK) (sk : SK) (fb : policy.FallbackState) (c : C) (costFn : (hashOracleSpec M R KD K).Domain → ω) (val : ω → ENNReal) (hval : Monotone val) (hdec : pke.decrypt sk c = none) : HasQuery.expectedQueryCost (fun [HasQuery (hashOracleSpec M R KD K) (AddWriterT ω m)] => (UTransform pke kdInput policy).decaps ((pk, sk), fb) c) runtime costFn val = val 0

If deterministic decryption fails immediately, decapsulation has expected weighted query cost 0.

theorem UTransform.decaps_expectedQueryCost_le {M PK SK R C KD K : Type} [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddCommMonoid ω] [PartialOrder ω] [IsOrderedAddMonoid ω] [CanonicallyOrderedAdd ω] [HasEvalPMF m] (runtime : QueryRuntime (hashOracleSpec M R KD K) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (policy : FujisakiOkamoto.RejectionPolicy K C) (pk : PK) (sk : SK) (fb : policy.FallbackState) (c : C) (costFn : (hashOracleSpec M R KD K).Domain → ω) (wCoins wKey : ω) (val : ω → ENNReal) (hval : Monotone val) (hCoins : ∀ (msg : M), costFn (Sum.inl msg) ≤ wCoins) (hKeys : ∀ (kd : KD), costFn (Sum.inr kd) ≤ wKey) : HasQuery.expectedQueryCost (fun [HasQuery (hashOracleSpec M R KD K) (AddWriterT ω m)] => (UTransform pke kdInput policy).decaps ((pk, sk), fb) c) runtime costFn val ≤ val (wCoins + wKey)

Expected weighted query cost of U-transform decapsulation is bounded by the sum of the per-family bounds.

theorem UTransform.decaps_usesAtMostTwoQueries {M PK SK R C KD K : Type} [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] [HasEvalSet m] (runtime : QueryRuntime (hashOracleSpec M R KD K) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (policy : FujisakiOkamoto.RejectionPolicy K C) (pk : PK) (sk : SK) (fb : policy.FallbackState) (c : C) : HasQuery.UsesAtMostQueries (fun [HasQuery (hashOracleSpec M R KD K) (AddWriterT ℕ m)] => (UTransform pke kdInput policy).decaps ((pk, sk), fb) c) runtime 2

Unit-cost specialization: U-transform decapsulation makes at most two oracle queries.

theorem UTransform.decaps_expectedQueries_le_two {M PK SK R C KD K : Type} [DecidableEq M] [DecidableEq C] [DecidableEq KD] [SampleableType M] [SampleableType R] [SampleableType K] {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] [HasEvalPMF m] (runtime : QueryRuntime (hashOracleSpec M R KD K) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (kdInput : M → C → KD) (policy : FujisakiOkamoto.RejectionPolicy K C) (pk : PK) (sk : SK) (fb : policy.FallbackState) (c : C) : HasQuery.expectedQueries (fun [HasQuery (hashOracleSpec M R KD K) (AddWriterT ℕ m)] => (UTransform pke kdInput policy).decaps ((pk, sk), fb) c) runtime ≤ 2

Expected query count of U-transform decapsulation is at most 2.

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

Runtime bundle for the two-RO U-transform oracle world.

theorem UTransform.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) (prf : PRFScheme KPRF C K) (kdInput : M → C → KD) (adversary : (UTransform pke kdInput (FujisakiOkamoto.implicitRejection prf)).IND_CCA_Adversary) (correctnessBound₁ correctnessBound₂ : ℝ) : ∃ (prfAdv : PRFScheme.PRFAdversary C K) (owAdv : OW_PCVA_Adversary (TTransform pke)), KEMScheme.IND_CCA_Advantage runtime adversary ≤ prf.prfAdvantage prfAdv + correctnessBound₁ + correctnessBound₂ + (OW_PCVA_Advantage TTransform.runtime owAdv).toReal

The generic U-transform CCA bound. The proof is intentionally deferred, but the reduction artifacts are now existentially quantified rather than passed in as unrelated inputs.