From 8d6e549b44ee755b4e9fc8b6f6ff173f73a87363 Mon Sep 17 00:00:00 2001
From: MM45 <research@mmeijers.com>
Date: Wed, 17 Sep 2025 17:48:36 +0200
Subject: [PATCH 1/2] Add tweakable hash function library

---
 theories/crypto/TweakableHashFunctions.eca | 954 +++++++++++++++++++++
 1 file changed, 954 insertions(+)
 create mode 100644 theories/crypto/TweakableHashFunctions.eca

diff --git a/theories/crypto/TweakableHashFunctions.eca b/theories/crypto/TweakableHashFunctions.eca
new file mode 100644
index 000000000..5b8c17653
--- /dev/null
+++ b/theories/crypto/TweakableHashFunctions.eca
@@ -0,0 +1,954 @@
+(*^
+  TweakableHashFunctions.eca
+
+  Library for tweakable hash functions (THFs).
+
+  Formalizes the concept of THFs, collections of THFs, and several corresponding
+  properties. Conceptually, THFs are variants of keyed-hash functions (KHFs)
+  that explicitly consider contextual data (mostly for domain separation).
+  Most, if not all, material in this library is based on the relevant
+  literature. In partiular, this includes the following:
+
+  - [The SPHINCS+ Signature Framework](https://dl.acm.org/doi/10.1145/3319535.3363229)
+  - [Recovering the Tight Security Proof of SPHINCS+](https://link.springer.com/chapter/10.1007/978-3-031-22972-5_1)
+
+^*)
+
+(* Require/Import *)
+require import AllCore List Distr.
+
+
+(* Types *)
+(*& Type for public parameters ('keys') &*)
+type pp_t.
+
+(* Type for tweaks/context information *)
+type tw_t.
+
+(* Type for inputs ('messages') *)
+type in_t.
+
+(* Type for outputs ('message digests') *)
+type out_t.
+
+
+(* Operators *)
+(*& Tweakable hash function &*)
+op f : pp_t -> tw_t -> in_t -> out_t.
+
+
+(* Distributions *)
+(*& Distribution over the public parameter type &*)
+op dpp : pp_t distr.
+
+
+
+(* Properties *)
+(*&
+  Single-function, Multi-target, Distinct-Tweak PREimage resistance (SM_DT_PRE).
+&*)
+abstract theory SMDTPRE.
+  (*& Number of targets for SM_DT_PRE &*)
+  const t : { int | 0 <= t } as ge0_t.
+
+  (*& Distribution over the input type &*)
+  op din : in_t distr.
+
+  (*& Type for challenge oracle used in SM_DT_PRE &*)
+  module type Oracle_SMDTPRE = {
+    proc init(pp_init : pp_t) : unit
+    proc query(tw : tw_t) : out_t
+    proc get(i : int) : tw_t * out_t
+    proc get_tweaks() : tw_t list
+    proc nr_targets() : int
+    proc dist_tweaks() : bool
+  }.
+
+  (*& Type for challenge oracle given to the adversary in SM_DT_PRE &*)
+  module type COracle_SMDTPRE = {
+    include Oracle_SMDTPRE [query]
+  }.
+
+  (*& Class of adversaries against SM_DT_PRE &*)
+  module type Adv_SMDTPRE(O : COracle_SMDTPRE) = {
+    proc pick() : unit
+    proc find(pp : pp_t) : int * in_t {}
+  }.
+
+  (*&
+    Default implementation of a SM_DT_PRE challenge oracle,
+    including procedures for initialization and auxiliary tasks
+  &*)
+  module O_SMDTPRE_Default : Oracle_SMDTPRE = {
+    var pp : pp_t
+    var ts : (tw_t * out_t) list
+
+    proc init(pp_init : pp_t) : unit = {
+      pp <- pp_init;
+      ts <- [];
+    }
+
+    proc query(tw : tw_t) : out_t = {
+      var x : in_t;
+      var y : out_t;
+      var twy : tw_t * out_t;
+
+      x <$ din;
+      y <- f pp tw x;
+
+      twy <- (tw, y);
+      ts <- rcons ts twy;
+
+      return y;
+    }
+
+    proc get(i : int) : tw_t * out_t = {
+      return nth witness ts i;
+    }
+
+    proc get_tweaks() : tw_t list = {
+      return unzip1 ts;
+    }
+
+    proc nr_targets() : int = {
+      return size ts;
+    }
+
+    proc dist_tweaks() : bool = {
+      return uniq (unzip1 ts);
+    }
+  }.
+
+  (*& SM_DT_PRE game &*)
+  module SM_DT_PRE(A : Adv_SMDTPRE, O : Oracle_SMDTPRE) = {
+    proc main() : bool = {
+      var pp : pp_t;
+      var tw : tw_t;
+      var x : in_t;
+      var y : out_t;
+      var i : int;
+      var nrts : int;
+      var dist : bool;
+
+      pp <$ dpp;
+      O.init(pp);
+
+      A(O).pick();
+      (i, x) <@ A(O).find(pp);
+
+      (tw, y) <@ O.get(i);
+
+      nrts <@ O.nr_targets();
+      dist <@ O.dist_tweaks();
+
+      return 0 <= i < nrts /\ 0 <= nrts <= t /\ dist /\ f pp tw x = y;
+    }
+  }.
+end SMDTPRE.
+
+
+(*&
+  Single-function, Multi-target, Distinct-Tweak Open PREimage resistance (SM_DT_OpenPRE).
+&*)
+abstract theory SMDTOpenPRE.
+  (*& Number of targets for SM_DT_OpenPRE &*)
+  const t : { int | 0 <= t } as ge0_t.
+
+  (*& Distribution over the input type &*)
+  op din : in_t distr.
+
+  (*& Type for opening oracle used in SM_DT_OpenPRE &*)
+  module type Oracle_SMDTOpenPRE = {
+    proc init(pp_init : pp_t, tws_init : tw_t list) : out_t list
+    proc open(i : int) : in_t
+    proc get(i : int) : tw_t * out_t
+    proc get_tweaks() : tw_t list
+    proc nr_targets() : int
+    proc dist_tweaks() : bool
+    proc opened(i : int) : bool
+  }.
+
+  (*& Type for opening oracle given to the adversary in SM_DT_OpenPRE &*)
+  module type COracle_SMDTOpenPRE = {
+    include Oracle_SMDTOpenPRE [open]
+  }.
+
+  (*& Class of adversaries against SM_DT_OpenPRE &*)
+  module type Adv_SMDTOpenPRE(O : COracle_SMDTOpenPRE) = {
+    proc pick() : tw_t list {}
+    proc find(pp : pp_t, ys : out_t list) : int * in_t
+  }.
+
+  (*&
+    Default implementation of a SM_DT_OpenPRE opening oracle,
+    including procedures for initialization and auxiliary tasks
+  &*)
+  module O_SMDTOpenPRE_Default : Oracle_SMDTOpenPRE = {
+    var pp : pp_t
+    var ts : (tw_t * out_t) list
+    var xs : in_t list
+    var os : int list
+
+    proc init(pp_init : pp_t, tws_init : tw_t list) : out_t list = {
+      var x : in_t;
+      var y : out_t;
+      var ys : out_t list;
+      var tw : tw_t;
+      var twy : tw_t * out_t;
+
+      pp <- pp_init;
+      ts <- [];
+      xs <- [];
+      os <- [];
+
+      ys <- [];
+      while (size ts < min (size tws_init) t) {
+        tw <- nth witness tws_init (size ts);
+        x <$ din;
+        y <- f pp tw x;
+
+        twy <- (tw, y);
+
+        xs <- rcons xs x;
+        ys <- rcons ys y;
+        ts <- rcons ts twy;
+      }
+
+      return ys;
+    }
+
+    proc open(i : int) : in_t = {
+      os <- rcons os i;
+
+      return nth witness xs i;
+    }
+
+    proc get(i : int) : tw_t * out_t = {
+      return nth witness ts i;
+    }
+
+    proc get_tweaks() : tw_t list = {
+      return unzip1 ts;
+    }
+
+    proc nr_targets() : int = {
+      return size ts;
+    }
+
+    proc dist_tweaks() : bool = {
+      return uniq (unzip1 ts);
+    }
+
+    proc opened(i : int) : bool = {
+      return i \in os;
+    }
+  }.
+
+  (*& SM_DT_OpenPRE game &*)
+  module SM_DT_OpenPRE(A : Adv_SMDTOpenPRE, O : Oracle_SMDTOpenPRE) = {
+    proc main() : bool = {
+      var pp : pp_t;
+      var tw : tw_t;
+      var tws : tw_t list;
+      var x : in_t;
+      var y : out_t;
+      var ys : out_t list;
+      var i : int;
+      var nrts : int;
+      var opened, dist : bool;
+
+      pp <$ dpp;
+      tws <@ A(O).pick();
+      ys <@ O.init(pp, tws);
+
+      (i, x) <@ A(O).find(pp, ys);
+
+      (tw, y) <@ O.get(i);
+
+      nrts <@ O.nr_targets();
+      opened <@ O.opened(i);
+      dist <@ O.dist_tweaks();
+
+      return 0 <= i < nrts /\ 0 <= nrts <= t /\ !opened /\ dist /\ f pp tw x = y;
+    }
+  }.
+end SMDTOpenPRE.
+
+
+(*&
+  Single-function, Multi-target, Distinct-Tweak Target Collision Resistance (SM_DT_TCR).
+&*)
+abstract theory SMDTTCR.
+  (*& Number of targets for SM_DT_TCR &*)
+  const t : { int | 0 <= t } as ge0_t.
+
+  (*& Type for challenge oracle used in SM_DT_TCR &*)
+  module type Oracle_SMDTTCR = {
+    proc init(pp_init : pp_t) : unit
+    proc query(tw : tw_t, x : in_t) : out_t
+    proc get(i : int) : tw_t * in_t
+    proc get_tweaks() : tw_t list
+    proc nr_targets() : int
+    proc dist_tweaks() : bool
+  }.
+
+  (*& Type for challenge oracle given to the adversary in SM_DT_TCR &*)
+  module type COracle_SMDTTCR = {
+    include Oracle_SMDTTCR [query]
+  }.
+
+  (*& Class of adversaries against SM_DT_TCR &*)
+  module type Adv_SMDTTCR(O : Oracle_SMDTTCR) = {
+    proc pick() : unit { O.query }
+    proc find(pp : pp_t) : int * in_t {}
+  }.
+
+  (*&
+    Default implementation of a SM_DT_TCR challenge oracle,
+    including procedures for initialization and auxiliary tasks
+  &*)
+  module O_SMDTTCR_Default : Oracle_SMDTTCR = {
+    var pp : pp_t
+    var ts : (tw_t * in_t) list
+
+    proc init(pp_init : pp_t) : unit = {
+      pp <- pp_init;
+      ts <- [];
+    }
+
+    proc query(tw : tw_t, x : in_t) : out_t = {
+      var y : out_t;
+      var twx : tw_t * in_t;
+
+      y <- f pp tw x;
+
+      twx <- (tw, x);
+      ts <- rcons ts twx;
+
+      return y;
+    }
+
+    proc get(i : int) : tw_t * in_t = {
+      return nth witness ts i;
+    }
+
+    proc get_tweaks() : tw_t list = {
+      return unzip1 ts;
+    }
+
+    proc nr_targets() : int = {
+      return size ts;
+    }
+
+    proc dist_tweaks() : bool = {
+      return uniq (unzip1 ts);
+    }
+  }.
+
+  (*& SM_DT_TCR game &*)
+  module SM_DT_TCR(A : Adv_SMDTTCR, O : Oracle_SMDTTCR) = {
+    proc main() : bool = {
+      var pp : pp_t;
+      var tw : tw_t;
+      var x, x' : in_t;
+      var i : int;
+      var nrts : int;
+      var dist : bool;
+
+      pp <$ dpp;
+      O.init(pp);
+
+      A(O).pick();
+      (i, x') <@ A(O).find(pp);
+
+      (tw, x) <@ O.get(i);
+
+      nrts <@ O.nr_targets();
+      dist <@ O.dist_tweaks();
+
+      return 0 <= i < nrts /\ 0 <= nrts <= t /\ dist /\ x <> x' /\ f pp tw x = f pp tw x';
+    }
+  }.
+end SMDTTCR.
+
+
+(*&
+  Single-function, Multi-target, Distinct-Tweak Decisional Second Preimage Resistance (SM_DT_DSPR).
+&*)
+abstract theory SMDTDSPR.
+  (* Predicate that checks whether there exists a second preimage for a given x under g pp tw *)
+  abbrev spexists (g : pp_t -> tw_t -> in_t -> out_t) (pp : pp_t) (tw : tw_t) (x : in_t) =
+    exists (x' : in_t), x <> x' /\ g pp tw x = g pp tw x'.
+
+  (*& Number of targets for SM_DT_DSPR &*)
+  const t : { int | 0 <= t } as ge0_t.
+
+  (*& Type for challenge oracle used in SM_DT_DSPR &*)
+  module type Oracle_SMDTDSPR = {
+    proc init(pp_init : pp_t) : unit
+    proc query(tw : tw_t, x : in_t) : out_t
+    proc get(i : int) : tw_t * in_t
+    proc get_tweaks() : tw_t list
+    proc nr_targets() : int
+    proc dist_tweaks() : bool
+  }.
+
+  (*& Type for challenge oracle given to the adversary in SM_DT_DSPR &*)
+  module type COracle_SMDTDSPR = {
+    include Oracle_SMDTDSPR [query]
+  }.
+
+  (*& Class of adversaries against SM_DT_DSPR &*)
+  module type Adv_SMDTDSPR(O : Oracle_SMDTDSPR) = {
+    proc pick() : unit
+    proc guess(pp : pp_t) : int * bool {}
+  }.
+
+  (*&
+    Default implementation of a SM_DT_DSPR challenge oracle,
+    including procedures for initialization and auxiliary tasks
+  &*)
+  module O_SMDTDSPR_Default : Oracle_SMDTDSPR = {
+    var pp : pp_t
+    var ts : (tw_t * in_t) list
+
+    proc init(pp_init : pp_t) : unit = {
+      pp <- pp_init;
+      ts <- [];
+    }
+
+    proc query(tw : tw_t, x : in_t) : out_t = {
+      var y : out_t;
+      var twx : tw_t * in_t;
+
+      y <- f pp tw x;
+
+      twx <- (tw, x);
+      ts <- rcons ts twx;
+
+      return y;
+    }
+
+    proc get(i : int) : tw_t * in_t = {
+      return nth witness ts i;
+    }
+
+    proc get_tweaks() : tw_t list = {
+      return unzip1 ts;
+    }
+
+    proc nr_targets() : int = {
+      return size ts;
+    }
+
+    proc dist_tweaks() : bool = {
+      return uniq (unzip1 ts);
+    }
+  }.
+
+  (*&
+    Game used to denote the probability that could trivially be obtained in
+    the SM_DSPR game by invariably returning 1
+  &*)
+  module SM_DT_SPprob(A : Adv_SMDTDSPR, O : Oracle_SMDTDSPR) = {
+    proc main() : bool = {
+      var pp : pp_t;
+      var tw : tw_t;
+      var x : in_t;
+      var i : int;
+      var b : bool;
+      var nrts : int;
+      var dist : bool;
+
+      pp <$ dpp;
+      O.init(pp);
+
+      A(O).pick();
+      (i, b) <@ A(O).guess(pp);
+
+      (tw, x) <@ O.get(i);
+
+      nrts <@ O.nr_targets();
+      dist <@ O.dist_tweaks();
+
+      return 0 <= i < nrts /\ 0 <= nrts <= t /\ dist /\ spexists f pp tw x;
+    }
+  }.
+
+  (*& SM_DT_DSPR game &*)
+  module SM_DT_DSPR(A : Adv_SMDTDSPR, O : Oracle_SMDTDSPR) = {
+    module A = A(O)
+
+    proc main() : bool = {
+      var pp : pp_t;
+      var tw : tw_t;
+      var x : in_t;
+      var twx : tw_t * in_t;
+      var i : int;
+      var b : bool;
+      var nrts : int;
+      var dist : bool;
+
+      pp <$ dpp;
+      O.init(pp);
+
+      A.pick();
+      (i, b) <@ A.guess(pp);
+
+      (tw, x) <@ O.get(i);
+
+      nrts <@ O.nr_targets();
+      dist <@ O.dist_tweaks();
+
+      return 0 <= i < nrts /\ 0 <= nrts <= t /\ dist /\ spexists f pp tw x = b;
+    }
+  }.
+
+  (*
+    NOTE:
+    Contrary to more conventional properties, the advantage for the above
+    is defined as
+
+    Adv_SMDTDSPR(A)
+    =
+    max 0 (Pr[SM_DT_DSPR(A).main() @ &m : res] - Pr[SM_DT_SPprob.main() @ &m : res]).
+  *)
+end SMDTDSPR.
+
+
+(*&
+  Single-function, Multi-target, Distinct-Tweak UnDetectability (SM_DT_UD).
+&*)
+abstract theory SMDTUD.
+(*& Number of targets for SM_DT_UD &*)
+const t : { int | 0 <= t } as ge0_t.
+
+(* Distribution over the input type *)
+op din : in_t distr.
+
+(* Distribution over the output type *)
+op dout : out_t distr.
+
+(*& Type for challenge oracle used in SM_DT_UD &*)
+module type Oracle_SMDTUD = {
+  proc init(b_init : bool, pp_init : pp_t) : unit
+  proc query(tw : tw_t) : out_t
+  proc get_tweaks() : tw_t list
+  proc nr_targets() : int
+  proc dist_tweaks() : bool
+}.
+
+(*& Type for challenge oracle given to the adversary in SM_DT_UD &*)
+module type COracle_SMDTUD = {
+  include Oracle_SMDTUD [query]
+}.
+
+(*& Class of adversaries against SM_DT_UD &*)
+module type Adv_SMDTUD(O : Oracle_SMDTUD) = {
+  proc pick() : unit
+  proc distinguish(pp : pp_t) : bool {}
+}.
+
+(*&
+  Default implementation of a SM_DT_UD challenge oracle,
+  including procedures for initialization and auxiliary tasks
+&*)
+module O_SMDTUD_Default : Oracle_SMDTUD = {
+  var b : bool
+  var pp : pp_t
+  var ts : tw_t list
+
+  proc init(b_init : bool, pp_init : pp_t) : unit = {
+    b <- b_init;
+    pp <- pp_init;
+    ts <- [];
+  }
+
+  proc query(tw : tw_t) : out_t = {
+    var x : in_t;
+    var y : out_t;
+
+    if (b) {
+      y <$ dout;
+    } else {
+      x <$ din;
+      y <- f pp tw x;
+    }
+
+    ts <- rcons ts tw;
+
+    return y;
+  }
+
+  proc get_tweaks() : tw_t list = {
+    return ts;
+  }
+
+  proc nr_targets() : int = {
+    return size ts;
+  }
+
+  proc dist_tweaks() : bool = {
+    return uniq ts;
+  }
+}.
+
+(*& SM_DT_UD game &*)
+module SM_DT_UD(A : Adv_SMDTUD, O : Oracle_SMDTUD) = {
+  module A = A(O)
+
+  proc main(b : bool) : bool = {
+    var pp : pp_t;
+    var b' : bool;
+    var nrts : int;
+    var dist : bool;
+
+    pp <$ dpp;
+    O.init(b, pp);
+
+    A.pick();
+    b' <@ A.distinguish(pp);
+
+    nrts <@ O.nr_targets();
+    dist <@ O.dist_tweaks();
+
+    return 0 <= nrts <= t /\ dist /\ b';
+  }
+}.
+end SMDTUD.
+
+
+(*&
+  Tweakable hash function properties in the presence of an
+  encompassing collection.
+&*)
+abstract theory Collection.
+  (* Predicate that returns true iff the given lists do not share any elements *)
+  abbrev disj_lists (s1 s2 : 'a list) : bool = ! has (mem s2) s1.
+
+  (*&
+    Type for differentiating characteristic of input types. An example of a
+    differentiating characteristic is (message) length, in which case this type
+    should be instantiated as int.
+  &*)
+  type diff_t.
+
+  (*& Computes differentiating characteristic of an input value &*)
+  op get_diff : in_t -> diff_t.
+
+  (*& Tweakable hash function collection &*)
+  op fc : diff_t -> pp_t -> tw_t -> in_t -> out_t.
+
+  (*&
+    Tweakable hash function `f` is a member of the tweakable hash function
+    collection `fc`
+  &*)
+  axiom in_collection : exists (df : diff_t), fc df = f.
+
+  (*&
+    Type for collection oracle used in tweakable hash function properties
+    for members of a collection
+  &*)
+  module type Oracle_THFC = {
+    proc init(pp_init : pp_t) : unit
+    proc get_tweaks() : tw_t list
+    proc query(tw : tw_t, x : in_t) : out_t
+  }.
+
+  (*&
+    Type for collection oracle given to adversaries in
+    tweakable hash function properties  for members of a collection
+  &*)
+  module type COracle_THFC = {
+    include Oracle_THFC [query]
+  }.
+
+  (*& Default implementation of collection oracle &*)
+  module O_THFC_Default : Oracle_THFC = {
+    var pp : pp_t
+    var tws : tw_t list
+
+    proc init(pp_init : pp_t) : unit = {
+      pp <- pp_init;
+      tws <- [];
+    }
+
+    proc query(tw : tw_t, x : in_t) : out_t = {
+      var df : diff_t;
+      var y : out_t;
+
+      df <- get_diff x;
+      y <- fc df pp tw x;
+
+      tws <- rcons tws tw;
+
+      return y;
+    }
+
+    proc get_tweaks() : tw_t list = {
+      return tws;
+    }
+  }.
+
+  (*&
+    Single-function, Multi-target, Distinct-Tweak PREimage resistance for members
+    of a Collection (SM_DT_PRE_C).
+  &*)
+  abstract theory SMDTPREC.
+    clone include SMDTPRE.
+
+    (*& Class of adversaries against SM_DT_PRE_C &*)
+    module type Adv_SMDTPREC(O : COracle_SMDTPRE, OC : COracle_THFC) = {
+      proc pick() : unit
+      proc find(pp : pp_t) : int * in_t {}
+    }.
+
+    (*& SM_DT_PRE_C game &*)
+    module SM_DT_PRE_C(A : Adv_SMDTPREC, O : Oracle_SMDTPRE, OC : Oracle_THFC) = {
+      proc main() : bool = {
+        var pp : pp_t;
+        var tw : tw_t;
+        var x : in_t;
+        var y : out_t;
+        var i : int;
+        var nrts : int;
+        var dist : bool;
+        var twsO, twsOC : tw_t list;
+
+        pp <$ dpp;
+        OC.init(pp);
+        O.init(pp);
+
+        A(O, OC).pick();
+        (i, x) <@ A(O, OC).find(pp);
+
+        (tw, y) <@ O.get(i);
+
+        nrts <@ O.nr_targets();
+        dist <@ O.dist_tweaks();
+
+        twsO <@ O.get_tweaks();
+        twsOC <@ OC.get_tweaks();
+
+        return 0 <= i < nrts /\ 0 <= nrts <= t /\ dist /\ f pp tw x = y /\ disj_lists twsO twsOC;
+      }
+    }.
+  end SMDTPREC.
+
+  (*&
+    Single-function, Multi-target, Distinct-Tweak Open PREimage resistance
+    for members of a Collection (SM_DT_PRE_C).
+  &*)
+  abstract theory SMDTOpenPREC.
+    clone include SMDTOpenPRE.
+
+    (*& Class of adversaries against SM_DT_OpenPRE_C &*)
+    module type Adv_SMDTOpenPREC(O : COracle_SMDTOpenPRE, OC : COracle_THFC) = {
+      proc pick() : tw_t list { OC.query }
+      proc find(pp : pp_t, ys : out_t list) : int * in_t { O.open }
+    }.
+
+    (*& SM_DT_OpenPRE game &*)
+    module SM_DT_OpenPRE_C(A : Adv_SMDTOpenPREC, O : Oracle_SMDTOpenPRE, OC : Oracle_THFC) = {
+      proc main() : bool = {
+        var pp : pp_t;
+        var tw : tw_t;
+        var tws : tw_t list;
+        var x : in_t;
+        var y : out_t;
+        var ys : out_t list;
+        var i : int;
+        var nrts : int;
+        var opened, dist : bool;
+        var twsO, twsOC : tw_t list;
+
+        pp <$ dpp;
+        OC.init(pp);
+
+        tws <@ A(O, OC).pick();
+
+        ys <@ O.init(pp, tws);
+
+        (i, x) <@ A(O, OC).find(pp, ys);
+
+        (tw, y) <@ O.get(i);
+
+        nrts <@ O.nr_targets();
+        opened <@ O.opened(i);
+        dist <@ O.dist_tweaks();
+
+        twsO <@ O.get_tweaks();
+        twsOC <@ OC.get_tweaks();
+
+        return 0 <= i < nrts /\ 0 <= nrts <= t /\ !opened /\ dist /\ f pp tw x = y /\ disj_lists twsO twsOC;
+      }
+    }.
+  end SMDTOpenPREC.
+
+  (*&
+    Single-function, Multi-target, Distinct-Tweak Target Collision Resistance for members
+    of a Collection (SM_DT_TCR_C).
+  &*)
+  abstract theory SMDTTCRC.
+    clone include SMDTTCR.
+
+    (*& Class of adversaries against SM_DT_TCR_C &*)
+    module type Adv_SMDTTCRC(O : COracle_SMDTTCR, OC : COracle_THFC) = {
+      proc pick() : unit
+      proc find(pp : pp_t) : int * in_t {}
+    }.
+
+    (*& SM_DT_TCR_C game &*)
+    module SM_DT_TCR_C(A : Adv_SMDTTCRC, O : Oracle_SMDTTCR, OC : Oracle_THFC) = {
+      proc main() : bool = {
+        var pp : pp_t;
+        var tw : tw_t;
+        var x, x' : in_t;
+        var y : out_t;
+        var i : int;
+        var nrts : int;
+        var dist : bool;
+        var twsO, twsOC : tw_t list;
+
+        pp <$ dpp;
+        OC.init(pp);
+        O.init(pp);
+
+        A(O, OC).pick();
+        (i, x') <@ A(O, OC).find(pp);
+
+        (tw, x) <@ O.get(i);
+
+        nrts <@ O.nr_targets();
+        dist <@ O.dist_tweaks();
+
+        twsO <@ O.get_tweaks();
+        twsOC <@ OC.get_tweaks();
+
+        return 0 <= i < nrts /\ 0 <= nrts <= t /\ dist /\ x <> x' /\ f pp tw x = f pp tw x' /\ disj_lists twsO twsOC;
+      }
+    }.
+  end SMDTTCRC.
+
+
+  (*&
+    Single-function, Multi-target, Distinct-Tweak Decisional Second Preimage Resistance for
+    members of a Collection (SM_DT_DSPR_C).
+  &*)
+  abstract theory SMDTDSPRC.
+    clone include SMDTDSPR.
+
+    (*& Class of adversaries against SM_DT_DSPR_C &*)
+    module type Adv_SMDTDSPRC(O : COracle_SMDTDSPR, OC : COracle_THFC) = {
+      proc pick() : unit
+      proc guess(pp : pp_t) : int * bool {}
+    }.
+
+    (*&
+      Game used to denote the probability that could trivially be obtained in
+      the SM_DSPR_C game by invariably returning 1
+    &*)
+    module SM_DT_SPprob_C(A : Adv_SMDTDSPRC, O : Oracle_SMDTDSPR, OC : Oracle_THFC) = {
+      proc main() : bool = {
+        var pp : pp_t;
+        var tw : tw_t;
+        var x : in_t;
+        var i : int;
+        var b : bool;
+        var nrts : int;
+        var dist : bool;
+        var twsO, twsOC : tw_t list;
+
+        pp <$ dpp;
+        OC.init(pp);
+        O.init(pp);
+
+        A(O, OC).pick();
+        (i, b) <@ A(O, OC).guess(pp);
+
+        (tw, x) <@ O.get(i);
+
+        nrts <@ O.nr_targets();
+        dist <@ O.dist_tweaks();
+
+        twsO <@ O.get_tweaks();
+        twsOC <@ OC.get_tweaks();
+
+        return 0 <= i < nrts /\ 0 <= nrts <= t /\ dist /\ spexists f pp tw x /\ disj_lists twsO twsOC;
+      }
+    }.
+
+    (*& SM_CT_DSPR_C game &*)
+    module SM_DT_DSPR_C(A : Adv_SMDTDSPRC, O : Oracle_SMDTDSPR, OC : Oracle_THFC) = {
+      proc main() : bool = {
+        var pp : pp_t;
+        var tw : tw_t;
+        var x : in_t;
+        var i : int;
+        var b : bool;
+        var nrts : int;
+        var dist : bool;
+        var twsO, twsOC : tw_t list;
+
+        pp <$ dpp;
+        OC.init(pp);
+        O.init(pp);
+
+        A(O, OC).pick();
+        (i, b) <@ A(O, OC).guess(pp);
+
+        (tw, x) <@ O.get(i);
+
+        nrts <@ O.nr_targets();
+        dist <@ O.dist_tweaks();
+
+        twsO <@ O.get_tweaks();
+        twsOC <@ OC.get_tweaks();
+
+        return 0 <= i < nrts /\ 0 <= nrts <= t /\ dist /\ spexists f pp tw x = b /\ disj_lists twsO twsOC;
+      }
+    }.
+  end SMDTDSPRC.
+
+  (*&
+    Single-function, Multi-target, Distinct-Tweak Undetectability for
+    members of a Collection (SM_DT_UD_C).
+  &*)
+  abstract theory SMDTUDC.
+    clone include SMDTUD.
+
+    (*& Class of adversaries against SM_DT_UD_C &*)
+    module type Adv_SMDTUDC(O : COracle_SMDTUD, OC : COracle_THFC) = {
+      proc pick() : unit
+      proc distinguish(pp : pp_t) :  bool {}
+    }.
+
+    (*& SM_DT_UD_C game &*)
+    module SM_DT_UD_C(A : Adv_SMDTUDC, O : Oracle_SMDTUD, OC : Oracle_THFC) = {
+      proc main(b : bool) : bool = {
+        var pp : pp_t;
+        var tw : tw_t;
+        var x : in_t;
+        var b' : bool;
+        var nrts : int;
+        var dist : bool;
+        var twsO, twsOC : tw_t list;
+
+        pp <$ dpp;
+        OC.init(pp);
+        O.init(b, pp);
+
+        A(O, OC).pick();
+        b' <@ A(O, OC).distinguish(pp);
+
+        nrts <@ O.nr_targets();
+        dist <@ O.dist_tweaks();
+
+        twsO <@ O.get_tweaks();
+        twsOC <@ OC.get_tweaks();
+
+        return 0 <= nrts <= t /\ dist /\ b' /\ disj_lists twsO twsOC;
+       }
+    }.
+  end SMDTUDC.
+end Collection.

From e32c10662b391a92aa5f24910dc992c8af3edd0e Mon Sep 17 00:00:00 2001
From: MM45 <research@mmeijers.com>
Date: Thu, 18 Sep 2025 08:03:37 +0200
Subject: [PATCH 2/2] Consistency naming

---
 theories/crypto/TweakableHashFunctions.eca | 99 ++++++++++------------
 1 file changed, 47 insertions(+), 52 deletions(-)

diff --git a/theories/crypto/TweakableHashFunctions.eca b/theories/crypto/TweakableHashFunctions.eca
index 5b8c17653..34518746e 100644
--- a/theories/crypto/TweakableHashFunctions.eca
+++ b/theories/crypto/TweakableHashFunctions.eca
@@ -55,7 +55,7 @@ abstract theory SMDTPRE.
   op din : in_t distr.
 
   (*& Type for challenge oracle used in SM_DT_PRE &*)
-  module type Oracle_SMDTPRE = {
+  module type Oraclei_SMDTPRE = {
     proc init(pp_init : pp_t) : unit
     proc query(tw : tw_t) : out_t
     proc get(i : int) : tw_t * out_t
@@ -65,12 +65,12 @@ abstract theory SMDTPRE.
   }.
 
   (*& Type for challenge oracle given to the adversary in SM_DT_PRE &*)
-  module type COracle_SMDTPRE = {
-    include Oracle_SMDTPRE [query]
+  module type Oracle_SMDTPRE = {
+    include Oraclei_SMDTPRE [query]
   }.
 
   (*& Class of adversaries against SM_DT_PRE &*)
-  module type Adv_SMDTPRE(O : COracle_SMDTPRE) = {
+  module type Adv_SMDTPRE(O : Oracle_SMDTPRE) = {
     proc pick() : unit
     proc find(pp : pp_t) : int * in_t {}
   }.
@@ -79,7 +79,7 @@ abstract theory SMDTPRE.
     Default implementation of a SM_DT_PRE challenge oracle,
     including procedures for initialization and auxiliary tasks
   &*)
-  module O_SMDTPRE_Default : Oracle_SMDTPRE = {
+  module O_SMDTPRE_Default : Oraclei_SMDTPRE = {
     var pp : pp_t
     var ts : (tw_t * out_t) list
 
@@ -120,7 +120,7 @@ abstract theory SMDTPRE.
   }.
 
   (*& SM_DT_PRE game &*)
-  module SM_DT_PRE(A : Adv_SMDTPRE, O : Oracle_SMDTPRE) = {
+  module SM_DT_PRE(A : Adv_SMDTPRE, O : Oraclei_SMDTPRE) = {
     proc main() : bool = {
       var pp : pp_t;
       var tw : tw_t;
@@ -158,7 +158,7 @@ abstract theory SMDTOpenPRE.
   op din : in_t distr.
 
   (*& Type for opening oracle used in SM_DT_OpenPRE &*)
-  module type Oracle_SMDTOpenPRE = {
+  module type Oraclei_SMDTOpenPRE = {
     proc init(pp_init : pp_t, tws_init : tw_t list) : out_t list
     proc open(i : int) : in_t
     proc get(i : int) : tw_t * out_t
@@ -169,12 +169,12 @@ abstract theory SMDTOpenPRE.
   }.
 
   (*& Type for opening oracle given to the adversary in SM_DT_OpenPRE &*)
-  module type COracle_SMDTOpenPRE = {
-    include Oracle_SMDTOpenPRE [open]
+  module type Oracle_SMDTOpenPRE = {
+    include Oraclei_SMDTOpenPRE [open]
   }.
 
   (*& Class of adversaries against SM_DT_OpenPRE &*)
-  module type Adv_SMDTOpenPRE(O : COracle_SMDTOpenPRE) = {
+  module type Adv_SMDTOpenPRE(O : Oracle_SMDTOpenPRE) = {
     proc pick() : tw_t list {}
     proc find(pp : pp_t, ys : out_t list) : int * in_t
   }.
@@ -183,7 +183,7 @@ abstract theory SMDTOpenPRE.
     Default implementation of a SM_DT_OpenPRE opening oracle,
     including procedures for initialization and auxiliary tasks
   &*)
-  module O_SMDTOpenPRE_Default : Oracle_SMDTOpenPRE = {
+  module O_SMDTOpenPRE_Default : Oraclei_SMDTOpenPRE = {
     var pp : pp_t
     var ts : (tw_t * out_t) list
     var xs : in_t list
@@ -219,7 +219,6 @@ abstract theory SMDTOpenPRE.
 
     proc open(i : int) : in_t = {
       os <- rcons os i;
-
       return nth witness xs i;
     }
 
@@ -245,7 +244,7 @@ abstract theory SMDTOpenPRE.
   }.
 
   (*& SM_DT_OpenPRE game &*)
-  module SM_DT_OpenPRE(A : Adv_SMDTOpenPRE, O : Oracle_SMDTOpenPRE) = {
+  module SM_DT_OpenPRE(A : Adv_SMDTOpenPRE, O : Oraclei_SMDTOpenPRE) = {
     proc main() : bool = {
       var pp : pp_t;
       var tw : tw_t;
@@ -283,7 +282,7 @@ abstract theory SMDTTCR.
   const t : { int | 0 <= t } as ge0_t.
 
   (*& Type for challenge oracle used in SM_DT_TCR &*)
-  module type Oracle_SMDTTCR = {
+  module type Oraclei_SMDTTCR = {
     proc init(pp_init : pp_t) : unit
     proc query(tw : tw_t, x : in_t) : out_t
     proc get(i : int) : tw_t * in_t
@@ -293,8 +292,8 @@ abstract theory SMDTTCR.
   }.
 
   (*& Type for challenge oracle given to the adversary in SM_DT_TCR &*)
-  module type COracle_SMDTTCR = {
-    include Oracle_SMDTTCR [query]
+  module type Oracle_SMDTTCR = {
+    include Oraclei_SMDTTCR [query]
   }.
 
   (*& Class of adversaries against SM_DT_TCR &*)
@@ -307,7 +306,7 @@ abstract theory SMDTTCR.
     Default implementation of a SM_DT_TCR challenge oracle,
     including procedures for initialization and auxiliary tasks
   &*)
-  module O_SMDTTCR_Default : Oracle_SMDTTCR = {
+  module O_SMDTTCR_Default : Oraclei_SMDTTCR = {
     var pp : pp_t
     var ts : (tw_t * in_t) list
 
@@ -346,7 +345,7 @@ abstract theory SMDTTCR.
   }.
 
   (*& SM_DT_TCR game &*)
-  module SM_DT_TCR(A : Adv_SMDTTCR, O : Oracle_SMDTTCR) = {
+  module SM_DT_TCR(A : Adv_SMDTTCR, O : Oraclei_SMDTTCR) = {
     proc main() : bool = {
       var pp : pp_t;
       var tw : tw_t;
@@ -384,7 +383,7 @@ abstract theory SMDTDSPR.
   const t : { int | 0 <= t } as ge0_t.
 
   (*& Type for challenge oracle used in SM_DT_DSPR &*)
-  module type Oracle_SMDTDSPR = {
+  module type Oraclei_SMDTDSPR = {
     proc init(pp_init : pp_t) : unit
     proc query(tw : tw_t, x : in_t) : out_t
     proc get(i : int) : tw_t * in_t
@@ -394,8 +393,8 @@ abstract theory SMDTDSPR.
   }.
 
   (*& Type for challenge oracle given to the adversary in SM_DT_DSPR &*)
-  module type COracle_SMDTDSPR = {
-    include Oracle_SMDTDSPR [query]
+  module type Oracle_SMDTDSPR = {
+    include Oraclei_SMDTDSPR [query]
   }.
 
   (*& Class of adversaries against SM_DT_DSPR &*)
@@ -408,7 +407,7 @@ abstract theory SMDTDSPR.
     Default implementation of a SM_DT_DSPR challenge oracle,
     including procedures for initialization and auxiliary tasks
   &*)
-  module O_SMDTDSPR_Default : Oracle_SMDTDSPR = {
+  module O_SMDTDSPR_Default : Oraclei_SMDTDSPR = {
     var pp : pp_t
     var ts : (tw_t * in_t) list
 
@@ -450,7 +449,7 @@ abstract theory SMDTDSPR.
     Game used to denote the probability that could trivially be obtained in
     the SM_DSPR game by invariably returning 1
   &*)
-  module SM_DT_SPprob(A : Adv_SMDTDSPR, O : Oracle_SMDTDSPR) = {
+  module SM_DT_SPprob(A : Adv_SMDTDSPR, O : Oraclei_SMDTDSPR) = {
     proc main() : bool = {
       var pp : pp_t;
       var tw : tw_t;
@@ -476,9 +475,7 @@ abstract theory SMDTDSPR.
   }.
 
   (*& SM_DT_DSPR game &*)
-  module SM_DT_DSPR(A : Adv_SMDTDSPR, O : Oracle_SMDTDSPR) = {
-    module A = A(O)
-
+  module SM_DT_DSPR(A : Adv_SMDTDSPR, O : Oraclei_SMDTDSPR) = {
     proc main() : bool = {
       var pp : pp_t;
       var tw : tw_t;
@@ -492,8 +489,8 @@ abstract theory SMDTDSPR.
       pp <$ dpp;
       O.init(pp);
 
-      A.pick();
-      (i, b) <@ A.guess(pp);
+      A(O).pick();
+      (i, b) <@ A(O).guess(pp);
 
       (tw, x) <@ O.get(i);
 
@@ -530,7 +527,7 @@ op din : in_t distr.
 op dout : out_t distr.
 
 (*& Type for challenge oracle used in SM_DT_UD &*)
-module type Oracle_SMDTUD = {
+module type Oraclei_SMDTUD = {
   proc init(b_init : bool, pp_init : pp_t) : unit
   proc query(tw : tw_t) : out_t
   proc get_tweaks() : tw_t list
@@ -539,8 +536,8 @@ module type Oracle_SMDTUD = {
 }.
 
 (*& Type for challenge oracle given to the adversary in SM_DT_UD &*)
-module type COracle_SMDTUD = {
-  include Oracle_SMDTUD [query]
+module type Oracle_SMDTUD = {
+  include Oraclei_SMDTUD [query]
 }.
 
 (*& Class of adversaries against SM_DT_UD &*)
@@ -553,7 +550,7 @@ module type Adv_SMDTUD(O : Oracle_SMDTUD) = {
   Default implementation of a SM_DT_UD challenge oracle,
   including procedures for initialization and auxiliary tasks
 &*)
-module O_SMDTUD_Default : Oracle_SMDTUD = {
+module O_SMDTUD_Default : Oraclei_SMDTUD = {
   var b : bool
   var pp : pp_t
   var ts : tw_t list
@@ -594,9 +591,7 @@ module O_SMDTUD_Default : Oracle_SMDTUD = {
 }.
 
 (*& SM_DT_UD game &*)
-module SM_DT_UD(A : Adv_SMDTUD, O : Oracle_SMDTUD) = {
-  module A = A(O)
-
+module SM_DT_UD(A : Adv_SMDTUD, O : Oraclei_SMDTUD) = {
   proc main(b : bool) : bool = {
     var pp : pp_t;
     var b' : bool;
@@ -606,8 +601,8 @@ module SM_DT_UD(A : Adv_SMDTUD, O : Oracle_SMDTUD) = {
     pp <$ dpp;
     O.init(b, pp);
 
-    A.pick();
-    b' <@ A.distinguish(pp);
+    A(O).pick();
+    b' <@ A(O).distinguish(pp);
 
     nrts <@ O.nr_targets();
     dist <@ O.dist_tweaks();
@@ -649,7 +644,7 @@ abstract theory Collection.
     Type for collection oracle used in tweakable hash function properties
     for members of a collection
   &*)
-  module type Oracle_THFC = {
+  module type Oraclei_THFC = {
     proc init(pp_init : pp_t) : unit
     proc get_tweaks() : tw_t list
     proc query(tw : tw_t, x : in_t) : out_t
@@ -659,12 +654,12 @@ abstract theory Collection.
     Type for collection oracle given to adversaries in
     tweakable hash function properties  for members of a collection
   &*)
-  module type COracle_THFC = {
-    include Oracle_THFC [query]
+  module type Oracle_THFC = {
+    include Oraclei_THFC [query]
   }.
 
   (*& Default implementation of collection oracle &*)
-  module O_THFC_Default : Oracle_THFC = {
+  module O_THFC_Default : Oraclei_THFC = {
     var pp : pp_t
     var tws : tw_t list
 
@@ -698,13 +693,13 @@ abstract theory Collection.
     clone include SMDTPRE.
 
     (*& Class of adversaries against SM_DT_PRE_C &*)
-    module type Adv_SMDTPREC(O : COracle_SMDTPRE, OC : COracle_THFC) = {
+    module type Adv_SMDTPREC(O : Oracle_SMDTPRE, OC : Oracle_THFC) = {
       proc pick() : unit
       proc find(pp : pp_t) : int * in_t {}
     }.
 
     (*& SM_DT_PRE_C game &*)
-    module SM_DT_PRE_C(A : Adv_SMDTPREC, O : Oracle_SMDTPRE, OC : Oracle_THFC) = {
+    module SM_DT_PRE_C(A : Adv_SMDTPREC, O : Oraclei_SMDTPRE, OC : Oraclei_THFC) = {
       proc main() : bool = {
         var pp : pp_t;
         var tw : tw_t;
@@ -743,13 +738,13 @@ abstract theory Collection.
     clone include SMDTOpenPRE.
 
     (*& Class of adversaries against SM_DT_OpenPRE_C &*)
-    module type Adv_SMDTOpenPREC(O : COracle_SMDTOpenPRE, OC : COracle_THFC) = {
+    module type Adv_SMDTOpenPREC(O : Oracle_SMDTOpenPRE, OC : Oracle_THFC) = {
       proc pick() : tw_t list { OC.query }
       proc find(pp : pp_t, ys : out_t list) : int * in_t { O.open }
     }.
 
     (*& SM_DT_OpenPRE game &*)
-    module SM_DT_OpenPRE_C(A : Adv_SMDTOpenPREC, O : Oracle_SMDTOpenPRE, OC : Oracle_THFC) = {
+    module SM_DT_OpenPRE_C(A : Adv_SMDTOpenPREC, O : Oraclei_SMDTOpenPRE, OC : Oraclei_THFC) = {
       proc main() : bool = {
         var pp : pp_t;
         var tw : tw_t;
@@ -793,13 +788,13 @@ abstract theory Collection.
     clone include SMDTTCR.
 
     (*& Class of adversaries against SM_DT_TCR_C &*)
-    module type Adv_SMDTTCRC(O : COracle_SMDTTCR, OC : COracle_THFC) = {
+    module type Adv_SMDTTCRC(O : Oracle_SMDTTCR, OC : Oracle_THFC) = {
       proc pick() : unit
       proc find(pp : pp_t) : int * in_t {}
     }.
 
     (*& SM_DT_TCR_C game &*)
-    module SM_DT_TCR_C(A : Adv_SMDTTCRC, O : Oracle_SMDTTCR, OC : Oracle_THFC) = {
+    module SM_DT_TCR_C(A : Adv_SMDTTCRC, O : Oraclei_SMDTTCR, OC : Oraclei_THFC) = {
       proc main() : bool = {
         var pp : pp_t;
         var tw : tw_t;
@@ -839,7 +834,7 @@ abstract theory Collection.
     clone include SMDTDSPR.
 
     (*& Class of adversaries against SM_DT_DSPR_C &*)
-    module type Adv_SMDTDSPRC(O : COracle_SMDTDSPR, OC : COracle_THFC) = {
+    module type Adv_SMDTDSPRC(O : Oracle_SMDTDSPR, OC : Oracle_THFC) = {
       proc pick() : unit
       proc guess(pp : pp_t) : int * bool {}
     }.
@@ -848,7 +843,7 @@ abstract theory Collection.
       Game used to denote the probability that could trivially be obtained in
       the SM_DSPR_C game by invariably returning 1
     &*)
-    module SM_DT_SPprob_C(A : Adv_SMDTDSPRC, O : Oracle_SMDTDSPR, OC : Oracle_THFC) = {
+    module SM_DT_SPprob_C(A : Adv_SMDTDSPRC, O : Oraclei_SMDTDSPR, OC : Oraclei_THFC) = {
       proc main() : bool = {
         var pp : pp_t;
         var tw : tw_t;
@@ -879,7 +874,7 @@ abstract theory Collection.
     }.
 
     (*& SM_CT_DSPR_C game &*)
-    module SM_DT_DSPR_C(A : Adv_SMDTDSPRC, O : Oracle_SMDTDSPR, OC : Oracle_THFC) = {
+    module SM_DT_DSPR_C(A : Adv_SMDTDSPRC, O : Oraclei_SMDTDSPR, OC : Oraclei_THFC) = {
       proc main() : bool = {
         var pp : pp_t;
         var tw : tw_t;
@@ -918,13 +913,13 @@ abstract theory Collection.
     clone include SMDTUD.
 
     (*& Class of adversaries against SM_DT_UD_C &*)
-    module type Adv_SMDTUDC(O : COracle_SMDTUD, OC : COracle_THFC) = {
+    module type Adv_SMDTUDC(O : Oracle_SMDTUD, OC : Oracle_THFC) = {
       proc pick() : unit
       proc distinguish(pp : pp_t) :  bool {}
     }.
 
     (*& SM_DT_UD_C game &*)
-    module SM_DT_UD_C(A : Adv_SMDTUDC, O : Oracle_SMDTUD, OC : Oracle_THFC) = {
+    module SM_DT_UD_C(A : Adv_SMDTUDC, O : Oraclei_SMDTUD, OC : Oraclei_THFC) = {
       proc main(b : bool) : bool = {
         var pp : pp_t;
         var tw : tw_t;