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.