SigmaZKP.ml

(** Zero-knowledge proofs using Sigma protocols *)

(* Copyright Xavier Leroy.
   License: LGPL 2.1 or later with OCaml LGPL Linking Exception *)

open Algebra

(* The interface of a protocol *)

module type SIGMA_PROTOCOL = sig

  type params
  type secret
  type commitment
  type challenge
  type response
  type prover_state

  val commit: params -> secret -> commitment * prover_state
  val challenge: unit -> challenge
  val reply: prover_state -> params -> secret -> challenge -> response
  val verify: params -> commitment -> challenge -> response -> bool
    (** The 4 main steps of the protocol *)

  val simulate: params -> challenge -> commitment * response
    (** The simulator used to show zero-knowledge-ness. *)

  val extract: params -> commitment -> challenge -> response -> challenge -> response -> secret
    (** The extractor used to show soundness. *)

  val hash: params -> commitment -> challenge
    (** A hash function for the Fiat-Shamir heuristic. *)
end

(* Test a protocol *)

module Test (S: SIGMA_PROTOCOL) = struct

let test p s wrong_s =
  (* Normal execution of the protocol *)
  let (k, st) = S.commit p s in
  let c = S.challenge () in
  let r = S.reply st p s c in
  assert (S.verify p k c r);
  let (k, st) = S.commit p wrong_s in
  let c = S.challenge () in
  let r = S.reply st p wrong_s c in
  assert (not (S.verify p k c r));

  (* Simulated execution *)
  let c = S.challenge () in
  let (k, r) = S.simulate p c in
  assert (S.verify p k c r);

  (* Extracting the secret from two executions with the same challenge *)
  let (k, st) = S.commit p s in
  let c1 = S.challenge () in
  let r1 = S.reply st p s c1 in
  let c2 = S.challenge () in
  let r2 = S.reply st p s c2 in
  if c1 <> c2 then begin
    let s' = S.extract p k c1 r1 c2 r2 in
    assert (s' = s)
  end

end

(* Running a protocol interactively *)

module Interactive (S: SIGMA_PROTOCOL) = struct

let prover ~verifier (p: S.params) (s: S.secret) =
  let (k, st) = S.commit p s in
  Multiparty.send verifier k;
  let c : S.challenge = Multiparty.receive verifier in
  let r = S.reply st p s c in
  Multiparty.send verifier r

let verifier ~prover (p: S.params) : bool =
  let k : S.commitment = Multiparty.receive prover in
  let c = S.challenge () in
  Multiparty.send prover c;
  let r = Multiparty.receive prover in
  S.verify p k c r

end

(* Running a protocol non-interactively, using the Fiat-Shamir heuristic *)

module Noninteractive (S: SIGMA_PROTOCOL) = struct

type params = S.params
type secret = S.secret
type proof = S.commitment * S.response

let proof (p: params) (s: secret) =
  let (k, st) = S.commit p s in
  let c = S.hash p k in
  let r = S.reply st p s c in
  (k, r)

let verify (p: params) (k, r: proof) =
  let c = S.hash p k in
  S.verify p k c r

end

(* Schnorr's protocol: proving knowledge of a discrete logarithm. *)

module Schnorr (G: GROUP) = struct

type params = G.t
type secret = Z.t
type commitment = G.t
type challenge = Z.t
type response = Z.t
type prover_state = Z.t

module M = Z_p(struct let p = G.order end)

let rng =
  Cryptokit.Random.(pseudo_rng (string secure_rng 32))

let commit a x =
  let y = M.random ~rng in
  (G.(generator ** y), y)

let challenge () =
  M.random ~rng

let reply y a x c =
  M.(y + x * c)

let verify a k c r =
  G.(generator ** r) = G.(k * a ** c)

let simulate a c =
  let r = M.random ~rng in
  (G.(generator ** r / a ** c), r)

let extract a k c1 r1 c2 r2 =
  M.(div (sub r1 r2) (sub c1 c2))

let hash p k =
  G.to_bytes p ^ G.to_bytes k
  |> Cryptokit.(hash_string (Hash.sha256()))
  |> M.of_bytes

end

(* Chaum-Pedersen: proving the well-formedness of an ElGamal encryption of 0 *)

module ChaumPedersen (G: GROUP) = struct

module M = Z_p(struct let p = G.order end)

let rng =
  Cryptokit.Random.(pseudo_rng (string secure_rng 32))

type params = G.t * G.t * G.t
type secret = Z.t
type commitment = G.t * G.t
type challenge = Z.t
type response = Z.t
type prover_state = Z.t

let commit (a, b, h) x =
  let u = M.random ~rng in
  let k = G.(generator ** u, h ** u) in
  (k, u)

let challenge () =
  M.random ~rng

let reply u params x c =
  M.(u + x * c)

let verify (a, b, h) k c r =
     G.(generator ** r = fst k * a ** c)
  && G.(h         ** r = snd k * b ** c)

let simulate (a, b, h) c =
  let r = M.random ~rng in
  let k = G.(generator ** r / a ** c, h ** r / b ** c) in
  (k, r)

let extract params k c1 r1 c2 r2 =
  M.(div (sub r1 r2) (sub c1 c2))

let hash (a, b, h) (k1, k2) =
  [a; b; h; k1; k2]
  |> List.map G.to_bytes
  |> String.concat ""
  |> Cryptokit.(hash_string (Hash.sha256()))
  |> M.of_bytes

end

(* Build a Sigma protocol for the property [P \/ Q]
   given Sigma protocols for [P] and [Q]. *)

module Disjunction (P: SIGMA_PROTOCOL with type challenge = Z.t)
                   (Q: SIGMA_PROTOCOL with type challenge = Z.t)
= struct

type params = P.params * Q.params
type secret = (P.secret, Q.secret) Either.t
type commitment = P.commitment * Q.commitment
type challenge = Z.t
type response = P.challenge * P.response * Q.challenge * Q.response
type prover_state =
  (P.prover_state * Q.challenge * Q.response,
   Q.prover_state * P.challenge * P.response) Either.t

let commit (params1, params2) secret =
  match secret with
  | Either.Left x ->
      let (k1, s1) = P.commit params1 x in
      let c2 = Q.challenge () in
      let (k2, r2) = Q.simulate params2 c2 in
      ((k1, k2), Either.Left (s1, c2, r2))
  | Either.Right x ->
      let (k2, s2) = Q.commit params2 x in
      let c1 = P.challenge () in
      let (k1, r1) = P.simulate params1 c1 in
      ((k1, k2), Either.Right (s2, c1, r1))

let challenge = P.challenge

let reply state (params1, params2) secret c =
  match state, secret with
  | Either.Left(s1, c2, r2), Either.Left x ->
      let c1 = Z.logxor c c2 in
      let r1 = P.reply s1 params1 x c1 in
      (c1, r1, c2, r2)
  | Either.Right(s2, c1, r1), Either.Right x ->
      let c2 = Z.logxor c c1 in
      let r2 = Q.reply s2 params2 x c2 in
      (c1, r1, c2, r2)
  | _, _ -> assert false

let verify (params1, params2) (k1, k2) c (c1, r1, c2, r2) =
     Z.logxor c1 c2 = c
  && P.verify params1 k1 c1 r1
  && Q.verify params2 k2 c2 r2

let simulate (params1, params2) c =
  let c1 = P.challenge() in
  let c2 = Z.logxor c c1 in
  let (k1, r1) = P.simulate params1 c1
  and (k2, r2) = Q.simulate params2 c2 in
  ((k1, k2), (c1, r1, c2, r2))

let extract (params1, params2) (k1, k2) c (c1, r1, c2, r2) c' (c1', r1', c2', r2') =
  if c2' = c2 then
    Either.Left (P.extract params1 k1 c1 r1 c1' r1')
  else if c1' = c1 then
    Either.Right (Q.extract params2 k2 c2 r2 c2' r2')
  else
    assert false

let hash (params1, params2) (k1, k2) =
  Z.logxor (P.hash params1 k1) (Q.hash params2 k2)

end

(* Application: proving that an ElGamal ciphertext encrypts either 0 or 1. *)

module ElGamal01 (G: GROUP) = struct

module CP = ChaumPedersen(G)
module D = Disjunction(CP)(CP)

type params = G.t * G.t * G.t
type secret = bool * CP.secret
type commitment = D.commitment
type challenge = Z.t
type response = D.response
type prover_state = D.prover_state

let conv_params (a, b, h as p) =
  (* A pair of Chaum-Pedersen parameters,
     one corresponding to an ElGamal encryption of 0    (g^r, h^r)
     the other to an ElGamal encryption of 1          (g^r, h^r g) *)
  (p, (a, G.(b / generator), h))

let conv_secret (b, sk) =
  if b then Either.Right sk else Either.Left sk

let commit params x = D.commit (conv_params params) (conv_secret x)
let challenge = D.challenge
let reply u params x c = D.reply u (conv_params params) (conv_secret x) c
let verify params k c r = D.verify (conv_params params) k c r
let simulate params c = D.simulate (conv_params params) c
let extract params k c1 r1 c2 r2 =
  match D.extract (conv_params params) k c1 r1 c2 r2 with
  | Either.Left x -> (false, x)
  | Either.Right x -> (true, x)
let hash params k = D.hash (conv_params params) k

end