Security of interactive reductions

Exact security notions for a reduction from a relation relIn to a relation relOut, in a world W implementing the oracles. All errors are in ℝ≥0∞; a perfect notion is error 0.

• Reduction.Complete W R relIn relOut ε: on every (x, w) in relIn, the honest run fails with probability at most ε, where success means that the verifier outputs the prover's statement and the prover's witness is valid for it.
• Verifier.Sound W V langIn langOut ε: on every x ∉ langIn, every prover strategy makes the verifier output a statement of langOut with probability at most ε.
• Verifier.KnowledgeSound V relIn relOut E ε: in the plain model, the straight-line extractor E recovers a valid input witness from the transcript and the prover's output witness, except with probability ε.
• Verifier.RbrSound V langIn langOut ε: round-by-round soundness in the plain model, with an error for every challenge round, through a state function on transcript prefixes.
• Reduction.HVZK R relIn Sim ε: in the plain model, the simulator's transcripts are ε-close in statistical distance to honest ones.

Interactive proofs and interactive oracle proofs are the reductions to the trivial relation Interactive.Accept, with output language Set.univ. Verifier.Sound quantifies over all prover strategies, with no query or time bound, so it is the information-theoretic notion in every world; arguments and query-bounded soundness in oracle worlds are separate notions. Verifier.KnowledgeSound is straight-line extraction from the transcript, as for interactive oracle proofs; proofs of knowledge in the sense of Bellare and Goldreich, whose extractors rewind the prover, are a different notion. Knowledge soundness and zero knowledge are stated in the plain model: in an oracle world the extractor would need the prover's queries and the simulator the oracle's view, which these definitions do not provide. Extractors and simulators are named arguments, so a property cannot hold vacuously through an unconstrained existential. Their efficiency is a separate layer.

Main definitions

• Interactive.language, Interactive.Accept, Interactive.CloseTo.
• Interactive.Reduction.Complete, Interactive.Verifier.Sound, Interactive.Verifier.KnowledgeSound.
• Interactive.Prefix, Interactive.RbrFrom, Interactive.Verifier.RbrSound.
• Interactive.Reduction.HVZK.

References

• R. Canetti, Y. Chen, J. Holmgren, A. Lombardi, G. N. Rothblum, R. D. Rothblum, D. Wichs, Fiat–Shamir: from practice to theory

def Cslib.Interactive.language {Stmt Wit : Type} (rel : Stmt → Wit → Prop) : Set Stmt

The language of a relation: the statements with a witness.

def Cslib.Interactive.Accept : Unit → Unit → Prop

The trivial relation that proof systems reduce to: acceptance.

def Cslib.Interactive.CloseTo {α : Type} (μ ν : PMF α) (ε : ENNReal) : Prop

μ is within statistical distance ε of ν: no event is more likely under μ than under ν by more than ε. Quantifying over all events makes this symmetric, and it is the total variation distance on any type, finite or not.

theorem Cslib.Interactive.CloseTo.map {α β : Type} {μ ν : PMF α} {ε : ENNReal} (h : CloseTo μ ν ε) (f : α → β) : CloseTo (PMF.map f μ) (PMF.map f ν) ε

Statistical closeness is preserved by postprocessing.

theorem Cslib.Interactive.CloseTo.trans {α : Type} {μ ν ρ : PMF α} {ε δ : ENNReal} (h₁ : CloseTo μ ν ε) (h₂ : CloseTo ν ρ δ) : CloseTo μ ρ (ε + δ)

Statistical closeness errors add along a chain.

Completeness, soundness and knowledge soundness

def Cslib.Interactive.Reduction.Complete {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} {s : Spec} {StmtIn WitIn StmtOut WitOut : Type} (W : World oP oV) (R : Reduction oP oV s StmtIn WitIn StmtOut WitOut) (relIn : StmtIn → WitIn → Prop) (relOut : StmtOut → WitOut → Prop) (ε : ENNReal) : Prop

Completeness with error ε.

def Cslib.Interactive.Verifier.Sound {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} {s : Spec} {StmtIn StmtOut : Type} (W : World oP oV) (V : Verifier oV s StmtIn StmtOut) (langIn : Set StmtIn) (langOut : Set StmtOut) (ε : ENNReal) : Prop

Soundness with error ε, against every prover strategy. Provers are not bounded in time or in oracle queries, so this is information-theoretic soundness in every world.

def Cslib.Interactive.Verifier.KnowledgeSound {s : Spec} {StmtIn WitIn StmtOut WitOut : Type} (V : Verifier OracleSpec.empty s StmtIn StmtOut) (relIn : StmtIn → WitIn → Prop) (relOut : StmtOut → WitOut → Prop) (E : StmtIn → s.Transcript → WitOut → WitIn) (ε : ENNReal) : Prop

Straight-line knowledge soundness with error ε, in the plain model: whenever a prover strategy, ending with an output witness, makes the verifier output a statement for which that witness is valid, the extractor E recovers a valid input witness from the statement, the transcript and the output witness, except with probability ε.

Round-by-round soundness

@[reducible]

def Cslib.Interactive.Prefix : Spec → Type

The prefixes of transcripts: none is the empty prefix of a nonempty protocol, and a protocol without rounds has only its complete (empty) transcript.

def Cslib.Interactive.Prefix.empty (s : Spec) : Prefix s

The empty prefix.

def Cslib.Interactive.PerChallenge.sum (s : Spec) : Spec.PerChallenge (fun (x : Type) => ENNReal) s → ENNReal

The total of per-round errors.

def Cslib.Interactive.RbrFrom (s : Spec) : Spec.PerChallenge ProbComp s → Spec.PerChallenge (fun (x : Type) => ENNReal) s → (Prefix s → Prop) → (s.Transcript → Prop) → Prop

The round-by-round condition on the rounds s, for the state function S on their prefixes (false on doomed prefixes), per-round errors ε and the event wins on complete transcripts. A prover message never leaves a doomed prefix; a challenge leaves one with probability at most its error; and the verifier's output on a doomed complete transcript never wins.

noncomputable def Cslib.Interactive.Verifier.outputOn {s : Spec} {StmtIn StmtOut : Type} (V : Verifier OracleSpec.empty s StmtIn StmtOut) (x : StmtIn) (τ : s.Transcript) : Option StmtOut

The output of a verifier without oracles on a complete transcript.

def Cslib.Interactive.Verifier.RbrSound {s : Spec} {StmtIn StmtOut : Type} (V : Verifier OracleSpec.empty s StmtIn StmtOut) (langIn : Set StmtIn) (langOut : Set StmtOut) (ε : Spec.PerChallenge (fun (x : Type) => ENNReal) s) : Prop

Round-by-round soundness in the plain model with per-round errors ε: some state function is false on the empty prefix of every x ∉ langIn and satisfies the round-by-round condition.

Zero knowledge

def Cslib.Interactive.Reduction.HVZK {s : Spec} {StmtIn WitIn StmtOut WitOut : Type} (R : Reduction OracleSpec.empty OracleSpec.empty s StmtIn WitIn StmtOut WitOut) (relIn : StmtIn → WitIn → Prop) (Sim : StmtIn → ProbComp s.Transcript) (ε : ENNReal) : Prop

Honest-verifier zero knowledge with statistical error ε (perfect for ε = 0), in the plain model: on every (x, w) in relIn, the simulator's transcript law is ε-close to the honest one.