Bijection Between Real View and Simulated View 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 *)) &lt;-&gt; 
    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) &lt;-&gt; 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
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 -&gt; Witness -&gt; bool) (* decidable relation *)
            (RandCoin : Type) (* random coin *) 
            (Commitment : Type) (* commitments *)
            (Challenge : Type) (* challenges *) 
            (Response : Type) (* response *). 

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

  Parameter (simulator : Statement -&gt; Challenge -&gt; Response -&gt;
                         Statement * Commitment * Challenge * Response)
            (extractor : Challenge -&gt; Response -&gt; Challenge -&gt; Response -&gt; Witness).


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

  Axiom Special_Soundness : forall s c e1 e2 r1 r2,
      e1 &lt;&gt; e2 -&gt;
      verify (s, c, e1, r1) = true -&gt;
      verify (s, c, e2, r2) = true -&gt;
      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 &lt;-&gt;
                      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 &lt;- 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 &lt;- 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 -&gt; Witness -&gt; bool) 
  (H : Rel s w = true) :
  forall (r : RandCoin), verify (Real_view s w e r) = true &lt;-&gt;
  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.