Identification from Sigma protocols

A Sigma protocol together with a key generator for its relation is an identification scheme ([BS23], Section 19.6): the key generator samples a witness-statement pair (x, y), the statement y is the public verification key, and the prover proves knowledge of x. This module states the exact, finite security reductions of Boneh and Shoup's Chapter 19 for such schemes. There is no efficiency claim here: the reductions are explicit programs, and the theorems relate the success probabilities of explicit experiments at a fixed security level.

An Impersonator commits from what it sees, keeps a private state, and answers the verifier's challenge from that state, possibly with fresh randomness. In a direct attack it sees only the verification key (directAttack, Attack Game 18.1); in an eavesdropping attack it also sees Q honest conversations (eavesdropAttack, Attack Game 18.2). oneWayGame is the one-way key generation experiment (Attack Game 19.2).

• Extraction (Theorem 19.14). If extract is a witness extractor for the statements the key generator produces (SpecialSoundOn, implied by SpecialSoundness), rewinding an impersonator with direct-attack success probability ε recovers a witness for the key with probability at least ε ^ 2 - ε / N, where N is the number of challenges; consequently ε ≤ 1 / N + √ε'. The generated pairs need not be in the relation.
• Simulation (Theorems 19.3 and 19.15). If the protocol is special HVZK, an eavesdropper succeeds with exactly the probability of the direct impersonator that simulates the conversations itself, provided the key generator only outputs pairs in the relation.

Both reductions only run the given impersonator and the simulator or extractor. Their efficiency, and the corresponding asymptotic statements under a hardness assumption, are separate obligations.

The experiments are Games, that is PMF Bool, written in do notation; the PMF monad lives in a single universe, so the protocol's types and the impersonator's state are in Type here, although SigmaProtocol itself is universe-polymorphic.

Main definitions

• SigmaProtocol.Impersonator: a two-stage prover strategy.
• SigmaProtocol.directAttack, SigmaProtocol.eavesdropAttack: impersonation experiments.
• SigmaProtocol.oneWayGame: recover a witness for a generated statement.
• SigmaProtocol.SpecialSoundOn: special soundness for the statements of a key generator.
• SigmaProtocol.Impersonator.rewind: the rewinding witness extractor.
• SigmaProtocol.simulateConversation, SigmaProtocol.Impersonator.withSimulatedViews: replace eavesdropped conversations by simulated ones.

Main results

• SigmaProtocol.sq_sub_le_oneWayGame_rewind: ε ^ 2 - ε / N ≤ ε' (Theorem 19.14).
• SigmaProtocol.succProbability_directAttack_le: ε ≤ 1 / N + √ε' (Theorem 19.14).
• SigmaProtocol.eavesdropAttack_eq_directAttack: eavesdropping is no stronger than a direct attack (Theorems 19.3 and 19.15).
• SigmaProtocol.succProbability_eavesdropAttack_le: the two combined.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Sections 18.2, 19.1 and 19.6.

structure Cslib.Crypto.Protocols.SigmaProtocol.Impersonator (View T C Z : Type) : Type 1

An impersonator: from its view it commits to t and keeps a private state, and from that state it answers the verifier's challenge, possibly with fresh randomness.

• State : Type

  The impersonator's private state between its two messages.

• commit : View → PMF (T × self.State)

  Commit from the view, keeping a private state.

• respond : self.State → C → PMF Z

  Answer a challenge from the private state.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.directAttack {X Y T C Z : Type} [Fintype C] [Nonempty C] (P : SigmaProtocol X Y T C Z) (keyGen : PMF (X × Y)) (A : Impersonator Y T C Z) : Game

A direct impersonation attack ([BS23], Attack Game 18.1): a key pair is generated, the impersonator sees the verification key y, commits, receives a uniform challenge, and responds; it wins when the conversation is accepting for y.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.eavesdropAttack {X Y T C Z : Type} [Fintype C] [Nonempty C] (P : SigmaProtocol X Y T C Z) (keyGen : PMF (X × Y)) (Q : ℕ) (A : Impersonator (Y × (Fin Q → T × C × Z)) T C Z) : Game

An eavesdropping impersonation attack ([BS23], Attack Game 18.2): as directAttack, but the impersonator first sees Q independent honest conversations between the prover and the verifier for the generated key.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.oneWayGame {X Y : Type} (keyGen : PMF (X × Y)) (R : X → Y → Prop) [(x : X) → (y : Y) → Decidable (R x y)] (B : Y → PMF X) : Game

One-way key generation ([BS23], Attack Game 19.2): the adversary sees a generated statement and wins when it outputs a witness for it, not necessarily the generated one.

Extraction by rewinding

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.Impersonator.rewind {X Y T C Z : Type} [Fintype C] [Nonempty C] (A : Impersonator Y T C Z) (extract : Y → T → C → Z → C → Z → X) (y : Y) : PMF X

The rewinding extractor (proof of [BS23], Theorem 19.14): run the impersonator to its commitment, answer two independent uniform challenges from the same state, and apply the extractor to the two conversations.

def Cslib.Crypto.Protocols.SigmaProtocol.SpecialSoundOn {X Y T C Z : Type} (P : SigmaProtocol X Y T C Z) (keyGen : PMF (X × Y)) (R : X → Y → Prop) (extract : Y → T → C → Z → C → Z → X) : Prop

Special soundness for the statements a key generator can produce: from two accepting conversations with a common commitment and distinct challenges for such a statement, extract computes a witness. It follows from SpecialSoundness, and suffices for extraction.

theorem Cslib.Crypto.Protocols.SigmaProtocol.SpecialSoundness.specialSoundOn {X Y T C Z : Type} {P : SigmaProtocol X Y T C Z} {R : X → Y → Prop} {extract : Y → T → C → Z → C → Z → X} (hP : P.SpecialSoundness R extract) (keyGen : PMF (X × Y)) : P.SpecialSoundOn keyGen R extract

Special soundness gives special soundness for every key generator.

theorem Cslib.Crypto.Protocols.SigmaProtocol.sq_sub_le_oneWayGame_rewind {X Y T C Z : Type} [Fintype C] [Nonempty C] {P : SigmaProtocol X Y T C Z} {R : X → Y → Prop} [(x : X) → (y : Y) → Decidable (R x y)] {extract : Y → T → C → Z → C → Z → X} {keyGen : PMF (X × Y)} (hP : P.SpecialSoundOn keyGen R extract) (A : Impersonator Y T C Z) : ↑(P.directAttack keyGen A).succProbability ^ 2 - ↑(P.directAttack keyGen A).succProbability / ↑(Fintype.card C) ≤ ↑(oneWayGame keyGen R (A.rewind extract)).succProbability

Extraction from an impersonator ([BS23], Theorem 19.14, Equation 19.17): with special soundness on the generated statements, the rewinding extractor recovers a witness with probability at least ε ^ 2 - ε / N, where ε is the direct-attack success probability and N the number of challenges.

theorem Cslib.Crypto.Protocols.SigmaProtocol.succProbability_directAttack_le {X Y T C Z : Type} [Fintype C] [Nonempty C] {P : SigmaProtocol X Y T C Z} {R : X → Y → Prop} [(x : X) → (y : Y) → Decidable (R x y)] {extract : Y → T → C → Z → C → Z → X} {keyGen : PMF (X × Y)} (hP : P.SpecialSoundOn keyGen R extract) (A : Impersonator Y T C Z) : ↑(P.directAttack keyGen A).succProbability ≤ 1 / ↑(Fintype.card C) + √↑(oneWayGame keyGen R (A.rewind extract)).succProbability

Security against direct attacks ([BS23], Theorem 19.14, Equation 19.18): with special soundness on the generated statements, the direct-attack success probability is at most 1 / N + √ε', where ε' is the success probability of the rewinding extractor in the one-way game.

Eavesdropping by simulation

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.simulateConversation {Y T C Z : Type} [Fintype C] [Nonempty C] (simulate : Y → C → PMF (T × Z)) (y : Y) : PMF (T × C × Z)

A simulated conversation: a uniform challenge and the simulator's commitment and response for it. Under special HVZK this is the law of an honest conversation (SpecialHVZK.conversation_eq).

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.Impersonator.withSimulatedViews {Y T C Z : Type} [Fintype C] [Nonempty C] (simulate : Y → C → PMF (T × Z)) {Q : ℕ} (A : Impersonator (Y × (Fin Q → T × C × Z)) T C Z) : Impersonator Y T C Z

An eavesdropper turned into a direct impersonator ([BS23], Theorem 19.3 and Figure 19.2): it simulates the Q conversations it would have overheard.

theorem Cslib.Crypto.Protocols.SigmaProtocol.eavesdropAttack_eq_directAttack {X Y T C Z : Type} [Fintype C] [Nonempty C] {P : SigmaProtocol X Y T C Z} {R : X → Y → Prop} {simulate : Y → C → PMF (T × Z)} (hP : P.SpecialHVZK R simulate) {keyGen : PMF (X × Y)} (hkey : ∀ key ∈ keyGen.support, R key.1 key.2) {Q : ℕ} (A : Impersonator (Y × (Fin Q → T × C × Z)) T C Z) : P.eavesdropAttack keyGen Q A = P.directAttack keyGen (Impersonator.withSimulatedViews simulate A)

Eavesdropping does not help ([BS23], Theorems 19.3 and 19.15): for a special HVZK protocol and a key generator whose pairs are in the relation, an eavesdropper succeeds with exactly the probability of the direct impersonator that simulates its views.

theorem Cslib.Crypto.Protocols.SigmaProtocol.succProbability_eavesdropAttack_le {X Y T C Z : Type} [Fintype C] [Nonempty C] {P : SigmaProtocol X Y T C Z} {R : X → Y → Prop} [(x : X) → (y : Y) → Decidable (R x y)] {extract : Y → T → C → Z → C → Z → X} {simulate : Y → C → PMF (T × Z)} (hsound : P.SpecialSoundness R extract) (hzk : P.SpecialHVZK R simulate) {keyGen : PMF (X × Y)} (hkey : ∀ key ∈ keyGen.support, R key.1 key.2) {Q : ℕ} (A : Impersonator (Y × (Fin Q → T × C × Z)) T C Z) : ↑(P.eavesdropAttack keyGen Q A).succProbability ≤ 1 / ↑(Fintype.card C) + √↑(oneWayGame keyGen R ((Impersonator.withSimulatedViews simulate A).rewind extract)).succProbability

Security of a special-sound, special-HVZK identification scheme against eavesdropping ([BS23], Theorems 19.14 and 19.15 combined): ε ≤ 1 / N + √ε', for the rewinding extractor of the simulating direct impersonator.