(* --------------------------------------------------------------------
 * Copyright (c) - 2016--2017 - Roberto Metere <r.metere2@ncl.ac.uk>
 *
 * Distributed under the terms of the CeCILL-B-V1 license
 * -------------------------------------------------------------------- *)

(* A formalisation of generic commitment schemes *)
require import DBool.

theory CommitmentProtocol.
  type value.
  type message.
  type commitment.
  type openingkey.

  module type CommitmentScheme = {
    proc gen() : value
    proc commit(x: value, m: message) : commitment * openingkey
    proc verify(x: value, m: message, c: commitment, d: openingkey) : bool
  }.

  module Correctness (S:CommitmentScheme) = {
    proc main(m: message) : bool = {
      var x, c, d, b;

      x      <@ S.gen();
      (c, d) <@ S.commit(x, m);
      b      <@ S.verify(x, m, c, d);

      return b;
    }
  }.

  (*
    Hiding: The commitment c shall not reveal (almost) anything about the message m.
  *)
  module type Unhider = {
    proc choose(x: value) : message * message
    proc guess(c: commitment) : bool
  }.

  module HidingExperiment (S:CommitmentScheme, U:Unhider) = {
    proc main() : bool = {
      var b, b', m0, m1, x, c, d;

      x        <@ S.gen();
      (m0, m1) <@ U.choose(x);
      b        <$ {0,1};
      (c, d)   <@ S.commit(x, b ? m1 : m0);
      b'       <@ U.guess(c);

      return (b = b');
    }
  }.

  (*
    Hard to generate a commitment of two different messages.
    With only x, a binder (whatever run by the committer or the receiver)
    shall not be able to produce two different messages such that
    both verify with the same commitment.
  *)
  module type Binder = {
    proc bind(x: value) : commitment * message * openingkey * message * openingkey
  }.

  module BindingExperiment (S:CommitmentScheme, B:Binder) = {
    proc main() : bool = {
      var x, c, m, m', d, d', v, v';

      x                 <@ S.gen();
      (c, m, d, m', d') <@ B.bind(x);
      v                 <@ S.verify(x, m , c, d );
      v'                <@ S.verify(x, m', c, d');

      return v /\ v' /\ (m <> m');
    }
  }.
end CommitmentProtocol.