Bijection Between Real View and Simulated View

Question

I have some basic idea about cryptography and trying to understand zero knowledge proof, so pardon my ignorance and stupidity. I am trying to formalize sigma protocol in Coq theorem prover, and so far everything is correct except the special honest verifier zero knowledge proof. The definition of special honest verifier zero knowledge proof [1]:

There exists a p.p.t. algorithm S (simulator) which given any v ∈ L_{R} and any challenge c ∈ C produces conversations (a, c, r) with the same probability distribution as conversations between honest P and V on common input v and challenge c, where P uses any witness w satisfying (v, w) ∈ R.

So, the definition roughly translates to:

Pr[Real_view (v, w, c)] = Pr[Simulator_view (v, c)]

But, say for the moment, if I do no want to do probabilistic reasoning inside Coq, and I write that there is a bijection between the real view and simulator view with making all the randomness explicitly:

f : Real_view (v (* statement *), w (* witness *), 
               c (* challenge from verifier *), 
               r (* random coin toss of prover *)) <-> 
    Simulator_view (v (* statement *), 
                    c (* challenge of verifier *)
                    z (* response chose randomly *) 

So my question is: is producing f sufficient for showing special honest verifier zero knowledge proof? The axiom would roughly look like this.

SHVZK : forall (v ∈ Statement) (w ∈ witness) (H : (v, w) ∈ R)
               (c ∈ Challenge) (r ∈ Randomness) (z ∈ Response), 
  exists f : Real_view (v, w, c, r) <-> Simulator_view (v, c, z), 
             verify (Real_view (v, w, c, r)) = true /\
             verify (Simulator_view (v, c, z)) = true. 

[1] https://www.win.tue.nl/~berry/2WC13/LectureNotes.pdf

Answer 1

Sigma protocols were formalized in ZKCrypt, a Coq library based on Easycrypt.

Answer 2

I came up with something which, I believe, avoids the probabilistic reasoning for Sigma protocol, but I will be very happy for your constructive criticism. Before I proceed, please have a look at my modelling of sigma protocol in Coq, specifically the axiom Special_Honest_Verifier_ZKP.

Module Type SigmaProtocol.
  Parameter (Statement : Type) (* Statement x *)
            (Witness : Type) (* witness w *)
            (Rel : Statement -> Witness -> bool) (* decidable relation *)
            (RandCoin : Type) (* random coin *) 
            (Commitment : Type) (* commitments *)
            (Challenge : Type) (* challenges *) 
            (Response : Type) (* response *). 

  Parameter  (initial : RandCoin -> Commitment)
             (challenge : Challenge)
             (response : Statement -> Witness ->
                         RandCoin -> Challenge ->
                         Response)
             (verify : Statement * Commitment * Challenge * Response -> bool).

  Parameter (simulator : Statement -> Challenge -> Response ->
                         Statement * Commitment * Challenge * Response)
            (extractor : Challenge -> Response -> Challenge -> Response -> Witness).


  Axiom Completness : forall (s : Statement) (w : Witness) (r : RandCoin)
                        (e : Challenge),
      Rel s w = true -> verify (s, initial r, e, response s w r e) = true.

  Axiom Special_Soundness : forall s c e1 e2 r1 r2,
      e1 <> e2 ->
      verify (s, c, e1, r1) = true ->
      verify (s, c, e2, r2) = true ->
      Rel s (extractor e1 r1 e2 r2) = true.


  (* Probablistic Reasoning could have made it nicer *)
  Axiom Special_Honest_Verifier_ZKP  : forall (s : Statement) (w : Witness) (e : Challenge),
    forall (r : RandCoin), verify (s, initial r, e, response s w r e) = true <->
                      forall (z : Response), verify (simulator s e z) = true.


End SigmaProtocol.     

Let's take a brief detour, assume that we were doing a probabilistic reasoning, then our real view and simulated would have looked like:

Real_view (s : Statement) (w : Witness) (e : Challenge) := do
  r <- G (* generate a random value from some group G *)
  let a := g^{r} (* commitment *)
  let z := r + e * w  (* compute the response *)
  return (s, a, e, z)



Simulator_view (s : Statement) (e : Challenge) := do
 z <- G (* random element from some group G *)
 return (s, g^z s^(-e), e, z)$




 Special_Honest_Verifier_ZKP  (s : Statement) (w : Witness) 
  (e : Challenge) (H : Rel s w = true) := 
  Pr [Real_view  s w e] = 
  Pr [Simulator_view s e]

Based on two probabilistic view, we could have shown that two are equal. Intuitively, in $Real\_view$, statement $s$, witness $w$, and the challenge $e$ is fixed, so the only thing that vary is the random coin drawn uniformly from some group $G$. The probability of drawing an element uniformly from a given set $S$ is 1/|S|, so the value of $\Pr [\text{Real_view s w e}] = 1/|G|$. By the same token of reasoning, $\Pr [\text{Simulator_view s e}] = 1/|G|$ which concludes that both probabilities are equal. However, the only problem is that we are not doing probabilistic reasoning, but not all all hope is lost. One key observation to escape this probabilistic reasoning is that we can make the randomness $r$ and response $z$ as explicit parameter. Consequently, our probabilistic program would turn into a deterministic Coq program.

Real_view (s : Statement) (w : Witness) (e : Challenge) 
  (r : RandCoin):=
  let a := g^{r} in (* commitment *)
  let z := r + e * w in  (* compute the response *)
  (s, a, e, z)

Simulator_view (s : Statement) (e : Challenge) 
 (z : Response) :=
 (s, g^z s^(-e), e, z)

Now that our views are deterministic, we need to find a way to model the probability distribution of the two views. We solve this problem by showing a bi-implication between the real view and simulated view. We show that real view and simulator's view align with each other. In terms of Coq, it is expressed as:

 (* Probablistic Reasoning could have made it nicer *)
 Special_Honest_Verifier_ZKP  (s : Statement) (w : Witness) 
  (e : Challenge) (Rel : Statement -> Witness -> bool) 
  (H : Rel s w = true) :
  forall (r : RandCoin), verify (Real_view s w e r) = true <->
  forall (z : Response), verify (Simulator_view s e z) = true;

The axiom $Special\_Honest\_Verifier\_ZKP$ says that for any given fixed statement $s$, witness $w$, challenge $e$, relation $Rel$, and assumption that $Rel$ $s$ $w$ holds, then for every random coin $r$ and a accepting real transcript, simulator can construct an accepting transcript from all random response drawn from response space.