Fujisaki-Okamoto T Transform

This file defines the derandomizing T transform:

• coins are derived from a random oracle on the plaintext
• decryption re-derives the coins and checks re-encryption

@[reducible, inline]

abbrev TTransform.oracleSpec (M R : Type) : OracleSpec (ℕ ⊕ M)

The full oracle world for the T-transform: unrestricted public randomness plus a random oracle mapping plaintexts to encryption coins.

@[reducible, inline]

abbrev TTransform.QueryCache (M R : Type) : Type

Cache state for the T-transform's lazy coins oracle.

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

Query implementation for the T-transform hash oracle.

def TTransform.decrypt {M PK SK R C : Type} {m : Type → Type v} [Monad m] (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) [DecidableEq C] [HasQuery (OracleSpec.ofFn fun (x : M) => R) m] (pk : PK) (sk : SK) (c : C) : m (Option M)

Decryption for the T transform: decrypt deterministically, then re-query the coins oracle and check that re-encryption reproduces the ciphertext.

def TTransform {M PK SK R C : Type} {m : Type → Type v} [Monad m] (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) [DecidableEq C] [MonadLiftT ProbComp m] [HasQuery (OracleSpec.ofFn fun (x : M) => R) m] : AsymmEncAlg m M PK (PK × SK) C

The HHK17 T transform, realized as a monadic AsymmEncAlg in the random-oracle world unifSpec + (M →ₒ R).

theorem map_construction {M PK SK R C : Type} [DecidableEq C] {m : Type → Type u} [Monad m] {n : Type → Type v} [Monad n] [MonadLiftT ProbComp m] [MonadLiftT ProbComp n] [HasQuery (OracleSpec.ofFn fun (x : M) => R) m] [HasQuery (OracleSpec.ofFn fun (x : M) => R) n] (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (F : HasQuery.QueryHom (OracleSpec.ofFn fun (x : M) => R) m n) (hLift : HasQuery.PreservesProbCompLift F.toMonadHom) : (TTransform pke).map F.toMonadHom = TTransform pke

The T-transform is natural in any oracle-semantics morphism that preserves both the plaintext-to-coins query capability and the distinguished lift of ProbComp.

theorem encrypt_usesExactQueryCost {M PK SK R C : Type} [DecidableEq C] {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] (runtime : QueryImpl (OracleSpec.ofFn fun (x : M) => R) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (pk : PK) (msg : M) (costFn : M → ω) : HasQuery.UsesCostExactly (fun [HasQuery (OracleSpec.ofFn fun (x : M) => R) (AddWriterT ω m)] => (TTransform pke).encrypt pk msg) runtime costFn (costFn msg)

T-transform encryption incurs exactly the weighted cost assigned to the single coins-oracle query on msg.

theorem encrypt_expectedQueryCost_eq {M PK SK R C : Type} [DecidableEq C] {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] [Preorder ω] [HasEvalPMF m] (runtime : QueryImpl (OracleSpec.ofFn fun (x : M) => R) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (pk : PK) (msg : M) (costFn : M → ω) (val : ω → ENNReal) (hval : Monotone val) : HasQuery.expectedQueryCost (fun [HasQuery (OracleSpec.ofFn fun (x : M) => R) (AddWriterT ω m)] => (TTransform pke).encrypt pk msg) runtime costFn val = val (costFn msg)

T-transform encryption has expected weighted query cost equal to the weight of querying msg.

theorem encrypt_usesExactlyOneQuery {M PK SK R C : Type} [DecidableEq C] {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (runtime : QueryImpl (OracleSpec.ofFn fun (x : M) => R) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (pk : PK) (msg : M) : HasQuery.UsesExactlyQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M) => R) (AddWriterT ℕ m)] => (TTransform pke).encrypt pk msg) runtime 1

T-transform encryption makes exactly one hash-oracle query under unit-cost instrumentation.

theorem decrypt_usesZeroQueryCost_of_decrypt_eq_none {M PK SK R C : Type} [DecidableEq C] {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] (runtime : QueryImpl (OracleSpec.ofFn fun (x : M) => R) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (pk : PK) (sk : SK) (c : C) (costFn : M → ω) (hdec : pke.decrypt sk c = none) : HasQuery.UsesCostExactly (fun [HasQuery (OracleSpec.ofFn fun (x : M) => R) (AddWriterT ω m)] => (TTransform pke).decrypt (pk, sk) c) runtime costFn 0

If deterministic decryption fails immediately, the T-transform incurs zero weighted query cost.

theorem decrypt_expectedQueryCost_eq_zero_of_decrypt_eq_none {M PK SK R C : Type} [DecidableEq C] {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] [Preorder ω] [HasEvalPMF m] (runtime : QueryImpl (OracleSpec.ofFn fun (x : M) => R) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (pk : PK) (sk : SK) (c : C) (costFn : M → ω) (val : ω → ENNReal) (hval : Monotone val) (hdec : pke.decrypt sk c = none) : HasQuery.expectedQueryCost (fun [HasQuery (OracleSpec.ofFn fun (x : M) => R) (AddWriterT ω m)] => (TTransform pke).decrypt (pk, sk) c) runtime costFn val = val 0

If deterministic decryption fails immediately, the T-transform has expected weighted query cost 0.

theorem decrypt_usesExactQueryCost_of_decrypt_eq_some {M PK SK R C : Type} [DecidableEq C] {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] (runtime : QueryImpl (OracleSpec.ofFn fun (x : M) => R) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (pk : PK) (sk : SK) (c : C) (costFn : M → ω) {msg : M} (hdec : pke.decrypt sk c = some msg) : HasQuery.UsesCostExactly (fun [HasQuery (OracleSpec.ofFn fun (x : M) => R) (AddWriterT ω m)] => (TTransform pke).decrypt (pk, sk) c) runtime costFn (costFn msg)

If deterministic decryption returns a message, the T-transform incurs exactly the weighted cost of querying that message to re-derive the coins.

theorem decrypt_expectedQueryCost_eq_of_decrypt_eq_some {M PK SK R C : Type} [DecidableEq C] {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] [Preorder ω] [HasEvalPMF m] (runtime : QueryImpl (OracleSpec.ofFn fun (x : M) => R) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (pk : PK) (sk : SK) (c : C) (costFn : M → ω) (val : ω → ENNReal) (hval : Monotone val) {msg : M} (hdec : pke.decrypt sk c = some msg) : HasQuery.expectedQueryCost (fun [HasQuery (OracleSpec.ofFn fun (x : M) => R) (AddWriterT ω m)] => (TTransform pke).decrypt (pk, sk) c) runtime costFn val = val (costFn msg)

If deterministic decryption returns a message, the T-transform has expected weighted query cost equal to the weight of querying that message.

theorem decrypt_usesNoQueries_of_decrypt_eq_none {M PK SK R C : Type} [DecidableEq C] {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (runtime : QueryImpl (OracleSpec.ofFn fun (x : M) => R) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (pk : PK) (sk : SK) (c : C) (hdec : pke.decrypt sk c = none) : HasQuery.UsesExactlyQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M) => R) (AddWriterT ℕ m)] => (TTransform pke).decrypt (pk, sk) c) runtime 0

If deterministic decryption fails immediately, the T-transform makes no hash-oracle queries.

theorem decrypt_usesExactlyOneQuery_of_decrypt_eq_some {M PK SK R C : Type} [DecidableEq C] {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (runtime : QueryImpl (OracleSpec.ofFn fun (x : M) => R) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (pk : PK) (sk : SK) (c : C) {msg : M} (hdec : pke.decrypt sk c = some msg) : HasQuery.UsesExactlyQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M) => R) (AddWriterT ℕ m)] => (TTransform pke).decrypt (pk, sk) c) runtime 1

If deterministic decryption returns a message, the T-transform makes exactly one hash-oracle query to re-derive the coins.

theorem decrypt_usesAtMostOneQuery {M PK SK R C : Type} [DecidableEq C] {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] [HasEvalSet m] (runtime : QueryImpl (OracleSpec.ofFn fun (x : M) => R) m) (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (pk : PK) (sk : SK) (c : C) : HasQuery.UsesAtMostQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M) => R) (AddWriterT ℕ m)] => (TTransform pke).decrypt (pk, sk) c) runtime 1

T-transform decryption makes at most one hash-oracle query under unit-cost instrumentation.

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

Runtime bundle for the T-transform random-oracle world.

def TTransform.OW_PCVA_Adversary.MakesAtMostQueries {M PK SK R C : Type} [DecidableEq M] [DecidableEq C] [SampleableType R] {pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C} (adversary : OW_PCVA_Adversary (TTransform pke)) (qH qP qV : ℕ) : Prop

Structural query bound for T-transform OW-PCVA adversaries: uniform-sampling queries are unrestricted, while qH, qP, and qV bound the hash, plaintext-checking, and validity oracles respectively.

Defined as the conjunction of three predicate-targeted query bounds IsQueryBoundP, one per counted oracle. Because the three index predicates are pairwise disjoint, the conjunction is equivalent to the prior single-vector IsQueryBound formulation.

theorem TTransform.OW_PCVA_bound {M PK SK R C : Type} [DecidableEq M] [DecidableEq C] [SampleableType M] [SampleableType R] (pke : AsymmEncAlg.ExplicitCoins ProbComp M PK SK R C) (adversary : OW_PCVA_Adversary (TTransform pke)) (correctnessBound gamma epsMsg : ℝ) (qH qP qV : ℕ) : OW_PCVA_Adversary.MakesAtMostQueries adversary qH qP qV → ∃ (cpaAdv₁ : (pke.toAsymmEncAlg ProbCompRuntime.probComp).IND_CPA_adversary) (cpaAdv₂ : (pke.toAsymmEncAlg ProbCompRuntime.probComp).IND_CPA_adversary), (OW_PCVA_Advantage runtime adversary).toReal ≤ 2 * (AsymmEncAlg.IND_CPA_advantage cpaAdv₁).toReal + 2 * (AsymmEncAlg.IND_CPA_advantage cpaAdv₂).toReal + correctnessBound + ↑qV * gamma + 2 * ↑(qH + qP + 1) * epsMsg

The T-transform OW-PCVA security statement.

WARNING: this is a placeholder statement, not the final theorem. The current shape is unsound as written: correctnessBound, gamma, and epsMsg are unconstrained ℝ parameters, so the right-hand side can be driven arbitrarily negative while the left-hand side is a probability and hence nonnegative. In the final HHK-style statement these slack terms must be constrained (typically correctnessBound is the underlying PKE's δ-correctness error, gamma is the γ-spreadness bound on ciphertexts, and epsMsg is the message-distribution collision/min-entropy term, all of which are provably nonnegative quantities derived from pke).

The proof is intentionally deferred. The oracle surface and query-budget parameters (qH, qP, qV) now match the HHK OW-PCVA game, but the bound itself still needs to be tightened before this can be a meaningful security claim.