https://github.com/EasyCrypt/easycrypt
Tip revision: 895e467d1beefdebcaa7bcf3306604947f525637 authored by Benjamin Gregoire on 25 January 2023, 14:28:17 UTC
cleanup
cleanup
Tip revision: 895e467
SigmaProtocol.ec
(* A formalisation of generic Sigma protocols *)
require import DBool.
require import Int.
require import Distr.
theory SigmaProtocol.
type statement.
type witness. (* witness to the statement *)
type message.
type secret. (* this may relate to the message *)
type challenge.
type response.
type transcript = message * challenge * response.
(* op dm: message distr. *)
op de: challenge distr.
(* op dz: response distr. *)
(*
(x, w) ← gen() should be such that
- (x, w) in R
- |w| <= poly(|x|) ← HOW?
*)
op slen: int.
op wlen: int.
op R (x: statement) (w: witness): bool.
axiom slen_pos: 0 < slen.
axiom wlen_pos: 0 < wlen.
module type SigmaScheme = {
proc gen() : statement * witness
proc commit(x: statement, w: witness) : message * secret
proc test(x: statement, m: message) : challenge
proc respond(sw: statement * witness, ms: message * secret, e: challenge) : response
proc verify(x: statement, m: message, e: challenge, z: response) : bool
}.
module type SigmaAlgorithms = {
proc soundness(x: statement, m: message, e: challenge, z: response, e': challenge, z': response) : witness option
proc simulate(x: statement, e: challenge) : message * challenge * response
}.
module Completeness (S: SigmaScheme) = {
proc main(x: statement, w: witness) : bool = {
var e, m, s, z, b;
(m, s) <@ S.commit(x, w);
e <@ S.test(x, m);
z <@ S.respond((x, w), (m, s), e);
b <@ S.verify(x, m, e, z);
return b;
}
}.
module Run (S: SigmaScheme) = {
proc main() : statement * message * challenge * response = {
var x, w, m, s, e, z;
(x, w) <@ S.gen();
(m, s) <@ S.commit(x, w);
e <@ S.test(x, m);
z <@ S.respond((x, w), (m, s), e);
return (x, m, e, z);
}
}.
(*
Special soundness is supposed to be a PPTA.
S(m, e, z, e', z') → (x, w) in R
*)
module SpecialSoundnessExperiment (S: SigmaScheme, A: SigmaAlgorithms) = {
proc main(x: statement, m: message, e: challenge, z: response, e': challenge, z': response) : witness option = {
var s, sto, w, r, v, v';
sto <@ A.soundness(x, m, e, z, e', z');
if (e <> e' /\ sto <> None) {
w <- oget sto;
r <- R x w;
v <@ S.verify(x, m, e , z );
v' <@ S.verify(x, m, e', z' );
if (r /\ v /\ v') {
s <- Some(w);
} else {
s <- None;
}
} else {
s <- None;
}
return s;
}
}.
(*
The simulator M is a PPTA that generates
Sigma Protocol transcripts from (x, e).
M(x, e) → (a, e, z)
M'(x) → (a, e, z) more strict but simulatable -- usless to implement?
*)
module SpecialHVZKExperiment (S: SigmaScheme, A: SigmaAlgorithms) = {
proc main(x: statement, e: challenge) : (message * challenge * response) option = {
var m, z, v, to;
(m, e, z) <@ A.simulate(x, e);
v <@ S.verify(x, m, e, z);
if (v) {
to <- Some(m, e, z);
} else {
to <- None;
}
return to;
}
}.
(*
* Trace is the triple (message, challenge, response).
* Conventionally, this distinguisher shall say true if the triplet comes
* from a real execution, otherwise false for an ideal execution.
*)
module type SigmaTraceDistinguisher = {
proc distinguish(x: statement, t: transcript) : bool
}.
module SimulateHonestVerifier (S: SigmaScheme, A: SigmaAlgorithms, D: SigmaTraceDistinguisher) = {
proc gameIdeal() : bool = {
var b, e, i, m, s, t, to, x, w;
(x, w) <@ S.gen();
(m, s) <@ S.commit(x, w);
e <$ de;
to <@ SpecialHVZKExperiment(S, A).main(x, e);
i <- 0; (* rubbish to circumvent some limits of the while/unroll tactic. *)
while (to = None) {
to <@ SpecialHVZKExperiment(S, A).main(x, e);
i <- i + 1;
}
t <- oget to;
b <@ D.distinguish(x, t);
return b;
}
proc gameReal() : bool = {
var b, t, m, e, z, x;
(x, m, e, z) <@ Run(S).main();
t <- (m, e, z);
b <@ D.distinguish(x, t);
return b;
}
proc main() : bool = {
var b, b';
b <$ {0,1};
if (b) {
b' <@ gameIdeal();
} else {
b' <@ gameReal();
}
return (b' = b);
}
}.
end SigmaProtocol.