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

Equations
    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

      Equations
        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

          Equations
            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

              Equations
                Instances For