Documentation

VCVio.CryptoFoundations.FujisakiOkamoto.Composed

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.

source
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.

Instances For
    source
    @[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.

    Instances For
      source
      @[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.

      Instances For
        source
        @[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.

        Instances For
          source
          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.

          Instances For
            source
            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).

            Instances For
              source
              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.

              Instances For
                source
                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.

                Instances For
                  source
                  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.

                  Instances For
                    source
                    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 theorem statement. The proof is intentionally deferred, but the reduction artifacts are now existentially quantified rather than passed in as unrelated inputs.