https://github.com/EasyCrypt/easycrypt
Raw File
Tip revision: a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC
Fix bug w.r.t. _tools presence detection.
Tip revision: a79f9ae
MAC.ec
(* --------------------------------------------------------------------
 * Copyright IMDEA Software Institute / INRIA - 2013, 2014
 * -------------------------------------------------------------------- *)

require import FSet.

type key.
type message.
type tag.

module type Scheme = {
  proc * init(): unit {}
  proc keygen(): key
  proc mac(k:key,m:message): tag
  proc verify(k:key,m:message,t:tag): bool
}.

module type Oracles = {
  proc mac(m:message): tag
  proc verify(m:message,t:tag): bool
}.

module Wrap(S:Scheme) = {
  var qs:message set
  var k:key

  proc init(): unit = {
    qs = empty;
    S.init();
    k = S.keygen();
  }

  proc mac(m:message): tag = {
    var r:tag;

    qs = add m qs;
    r = S.mac(k,m);
    return r;
  }

  proc verify(m:message,t:tag): bool = {
    var r:bool;

    r = S.verify(k,m,t);
    return r;
  }

  proc fresh(m:message): bool = {
    return (!mem m qs);
  }
}.

module type Adv_CMA(O:Oracles) = {
  proc forge(): (message * tag)
}.

module CMA(S:Scheme,A:Adv_CMA) = {
  module O = Wrap(S)
  module A = A(O)

  proc main(): bool = {
    var m:message;
    var t:tag;
    var forged,fresh:bool;

    O.init();
    (m,t) = A.forge();
    forged = O.verify(m,t);
    fresh = O.fresh(m);
    return forged /\ fresh;
  }
}.
back to top