Documentation

ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.ProverTransform

Prover transformation #

This file contains the prover transformation (via query simulation) for the analysis of duplex sponge Fiat-Shamir, following Section 5.4 in the paper.

source
def DuplexSpongeFS.duplexSpongeToBasicFSQueryImpl {StmtIn : Type} {n : ℕ} {pSpec : ProtocolSpec n} {U : Type} [SpongeUnit U] [SpongeSize] :
QueryImpl (OracleSpec.duplexSpongeChallengeOracle StmtIn U) (OracleComp (ProtocolSpec.fsChallengeOracle StmtIn pSpec))

The query simulation between duplex sponge oracles and basic Fiat-Shamir oracles. This is then composed with the duplex-sponge malicious prover to obtain a basic F-S malicious prover

Instances For
    source
    def DuplexSpongeFS.d2SQueryImpl {StmtIn : Type} {n : ℕ} {pSpec : ProtocolSpec n} {U : Type} [SpongeUnit U] [SpongeSize] :
    QueryImpl (OracleSpec.duplexSpongeChallengeOracle StmtIn U) (OracleComp (ProtocolSpec.fsChallengeOracle StmtIn pSpec))

    Alias of DuplexSpongeFS.duplexSpongeToBasicFSQueryImpl.

    The query simulation between duplex sponge oracles and basic Fiat-Shamir oracles. This is then composed with the duplex-sponge malicious prover to obtain a basic F-S malicious prover

    Instances For
      source
      def DuplexSpongeFS.duplexSpongeToBasicFSAlgo {ι : Type} {oSpec : OracleSpec ι} {StmtIn : Type} {n : ℕ} {pSpec : ProtocolSpec n} {U : Type} [SpongeUnit U] [SpongeSize] (P : OracleComp (oSpec + OracleSpec.duplexSpongeChallengeOracle StmtIn U) (StmtIn × pSpec.Messages)) :
      OracleComp (oSpec + ProtocolSpec.fsChallengeOracle StmtIn pSpec) (StmtIn × pSpec.Messages)

      The transformation of a duplex-sponge Fiat-Shamir malicious prover to a basic Fiat-Shamir one.

      Note: this transformation needs to be an oracle computation itself

      Instances For
        source
        def DuplexSpongeFS.d2SAlgo {ι : Type} {oSpec : OracleSpec ι} {StmtIn : Type} {n : ℕ} {pSpec : ProtocolSpec n} {U : Type} [SpongeUnit U] [SpongeSize] (P : OracleComp (oSpec + OracleSpec.duplexSpongeChallengeOracle StmtIn U) (StmtIn × pSpec.Messages)) :
        OracleComp (oSpec + ProtocolSpec.fsChallengeOracle StmtIn pSpec) (StmtIn × pSpec.Messages)

        Alias of DuplexSpongeFS.duplexSpongeToBasicFSAlgo.

        The transformation of a duplex-sponge Fiat-Shamir malicious prover to a basic Fiat-Shamir one.

        Note: this transformation needs to be an oracle computation itself

        Instances For