Documentation

Complexity.Crypto.Protocols.SigmaProtocol.Abort

Sigma protocols with aborts #

In lattice-based Sigma protocols the prover may refuse to answer a challenge: in Lyubashevsky's Fiat–Shamir with aborts ([Lyu09], [Lyu12]) it withholds every response that would leak information about its witness. Such a protocol is an ordinary SigmaProtocol whose responses are Option Z. The prover answers none to abort, and the verifier is expected to reject none.

This module studies an erased-abort projection, not the full interactive verifier view. An identification verifier has already seen the commitment before an abort; retrying does not erase that observation. A signer can instead keep aborted attempts unpublished and retry with fresh randomness. Full interactive-view simulation requires a separate theorem. acceptedTranscript x y c is the honest commitment and response at the challenge c, erased to none when the prover aborts. A simulator must reproduce the abort probability as well as the law of the transcripts that are not aborted. Plain SpecialHVZK usually fails for these protocols, because the commitment of an aborted run depends on the witness.

These are the exact, per-challenge analogues of Complete and SpecialHVZK. Special soundness needs no change: it only concerns accepting conversations, and SpecialSoundness applies as it stands.

Main definitions #

Main results #

References #

source
noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.acceptedTranscript {X Y T C Z : Type u} (P : SigmaProtocol X Y T C (Option Z)) (x : X) (y : Y) (c : C) :
PMF (Option (T × Z))

The honest commitment and response at the challenge c, or none if the prover aborts.

Instances For
    source
    noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.acceptedConversation {X Y T C Z : Type u} (P : SigmaProtocol X Y T C (Option Z)) [Fintype C] [Nonempty C] (x : X) (y : Y) :
    PMF (Option (T × C × Z))

    An honest conversation with a uniform challenge, or none if the prover aborts.

    Instances For
      source
      def Cslib.Crypto.Protocols.SigmaProtocol.NonAbortComplete {X Y T C Z : Type u} (P : SigmaProtocol X Y T C (Option Z)) (R : X → Y → Prop) :
      Prop

      Completeness up to aborts: for every witness-statement pair in R and every challenge, every honest transcript in which the prover does not abort is accepting.

      Instances For
        source
        structure Cslib.Crypto.Protocols.SigmaProtocol.NonAbortSpecialHVZK {X Y T C Z : Type u} (P : SigmaProtocol X Y T C (Option Z)) (R : X → Y → Prop) (simulate : Y → C → PMF (Option (T × Z))) :
        Prop

        Special honest-verifier zero knowledge up to aborts, with the explicit simulator simulate. Given a statement and a challenge, the simulator returns a commitment and a response, or none for an abort.

        • accepts (y : Y) (c : C) (t : T) (z : Z) : some (t, z) ∈ (simulate y c).support → P.Accepts y t c (some z)

          Simulated transcripts that are not aborted are accepting, for every statement and challenge.

        • acceptedTranscript_eq (x : X) (y : Y) : R x y → ∀ (c : C), simulate y c = P.acceptedTranscript x y c

          For a witness-statement pair, simulation at any fixed challenge has the law of the accepted view, aborts included.

        Instances For
          source
          theorem Cslib.Crypto.Protocols.SigmaProtocol.NonAbortComplete.mono {X Y T C Z : Type u} {P : SigmaProtocol X Y T C (Option Z)} {R R' : X → Y → Prop} (h : P.NonAbortComplete R) (hR : ∀ (x : X) (y : Y), R' x y → R x y) :
          P.NonAbortComplete R'

          Completeness up to aborts for a relation implies it for every smaller relation.

          source
          theorem Cslib.Crypto.Protocols.SigmaProtocol.NonAbortSpecialHVZK.mono {X Y T C Z : Type u} {P : SigmaProtocol X Y T C (Option Z)} {R R' : X → Y → Prop} {simulate : Y → C → PMF (Option (T × Z))} (h : P.NonAbortSpecialHVZK R simulate) (hR : ∀ (x : X) (y : Y), R' x y → R x y) :
          P.NonAbortSpecialHVZK R' simulate

          A simulator up to aborts for a relation is one for every smaller relation.

          source
          theorem Cslib.Crypto.Protocols.SigmaProtocol.acceptedConversation_eq_bind {X Y T C Z : Type u} (P : SigmaProtocol X Y T C (Option Z)) [Fintype C] [Nonempty C] (x : X) (y : Y) :
          P.acceptedConversation x y = do let c ← Probability.PMF.uniformOfFintype C let tz ← P.acceptedTranscript x y c pure (Option.map (fun (tz : T × Z) => (tz.1, c, tz.2)) tz)

          An honest execution with aborted runs erased samples the challenge first.

          source
          theorem Cslib.Crypto.Protocols.SigmaProtocol.NonAbortComplete.accepts_of_mem_support_acceptedConversation {X Y T C Z : Type u} {P : SigmaProtocol X Y T C (Option Z)} {R : X → Y → Prop} [Fintype C] [Nonempty C] (h : P.NonAbortComplete R) {x : X} {y : Y} (hxy : R x y) {t : T} {c : C} {z : Z} (htcz : some (t, c, z) ∈ (P.acceptedConversation x y).support) :
          P.Accepts y t c (some z)

          Every published honest conversation is accepting.

          source
          theorem Cslib.Crypto.Protocols.SigmaProtocol.NonAbortSpecialHVZK.acceptedConversation_eq {X Y T C Z : Type u} {P : SigmaProtocol X Y T C (Option Z)} {R : X → Y → Prop} [Fintype C] [Nonempty C] {simulate : Y → C → PMF (Option (T × Z))} (h : P.NonAbortSpecialHVZK R simulate) {x : X} {y : Y} (hxy : R x y) :
          P.acceptedConversation x y = do let c ← Probability.PMF.uniformOfFintype C let tz ← simulate y c pure (Option.map (fun (tz : T × Z) => (tz.1, c, tz.2)) tz)

          Zero knowledge up to aborts. With a uniform challenge, the simulator reproduces the accepted view of an honest conversation: the abort probability, and the law of the published conversations.