CHANGES

* 1.8.0
  - Support for natural numbers and subterm reasoning

  - Tactics language added, improves over oracle use

  - SAPIC:
    improvements and extensions, including an export functionality targeting ProVerif and DeepSec;
    boundedness checks;
    SAPIC now also supports natural numbers (deprecating use of multisets)

  - Advanced DH (subgroups) with additional neutral group element added to Diffie-Hellman builtin

  - Added macros

  - Improved warnings:
    Added checks to notify user of likely modeling errors as warnings, regarding equational theory use
    Added warning to notify if a fact occurs in LHS, but never in any RHS (thus not executable)
    Generally made warnings more readable

  - Improved graph visualization:
    auto sources annotations are hidden in graphs by default except when proving sources lemmas
    less relation arrows are colored depending on their causes
    a transitive reduction is applied by default to make graphs more readable
    
  - More verbose Tamarin self-identification on --version

  - Allow optional trailing commas in lists

  - Refactoring of Theory.hs, and other smaller files

  - Use GitHub actions for automated regression tests

  - Numerous bug fixes

  - Added many examples from different published papers

  - Allow Maude up to 3.3.1 (default 3.2.1)

  - Using stack LTS resolver 20.26 and GHC 9.2.8 now [stack update, stack upgrade may be needed]

* 1.6.1
  - Further SAPIC integration

  - Improved auto sources - compute sources lemmas automatically
  
  - Allow specifying the oracle to use in an oracle ranking within the Tamarin file, either globally or per lemma

  - Add a shortcut to prove all lemmas ('s' and 'S')
  
  - Export and import rule variants
  
  - Docker files for Tamarin

  - Allow Maude 3.1 and fixed parser accordingly
  
  - Add check for PNG support in GraphViz

  - Numerous bug fixes
  
  - Added script for automated tests, even on Travis
  
  - Refactoring and fixing the parser
  
  - Fixed SAPIC for OCaml 4.12
  
  - Fixed compatibility with GHC 9, removed monad-unlift
  
  - Multiple new case studies

  - Using stack LTS resolver 18.5 and GHC 8.10.4 now [stack update, stack upgrade may be needed]

* 1.6.0
  - SAPIC integration

  - New feature: auto sources - compute sources lemmas automatically

  - New feature: predicate support

  - Observational equivalence concludes with attack more quickly, without requiring instantiation to public values for free variables.

  - Add a true (sequential) depth-first search (DFS) option: --stop-on-trace=seqdfs

  - nixOS development simplification

  - Allow Maude 3.0.0 (in addition to 2.7.1)

  - Change: --prove=name only verifies lemma named 'name', to prove all lemmas with the prefix 'name' use --prove=name* instead; adjusted existing examples

  - Numerous bug fixes

  - Multiple new case studies

  - Using stack LTS resolver 16.12 and GHC 8.8.4 now [stack update, stack upgrade needed]

* 1.4.1
  - Variants are now computed in Maude, for a pre-computation speedup for theories with many variants. Old internal variant computation still accessible by setting the environment variable "TAMARIN_NO_MAUDE_VARIANTS".

  - XOR support added to SAPIC

  - Locking and unlocking in SAPIC improved

  - Input spthy files can declare the heuristic to be used in two ways: globally for all lemmas; and locally each lemma can overwrite that. Note that both take precedence over a heuristic parameter passed on the command-line.

  - Hex color parsing for rules updated

  - 5G-AKA protocol models added, described in the CCS 2018 paper (https://arxiv.org/abs/1806.10360): "A Formal Analysis of 5G Authentication"

  - DNP3 protocol models added, described in ESORICS 2017 paper: "Secure Authentication in the Grid: A Formal Analysis of DNP3: SAv5 ", and extended version in JCS 2018.

  - Numerous bug fixes

  - Syntax highlighting options improved and moved for multiple editors

  - Using stack LTS resolver 13.2 and GHC 8.6.3 now

* 1.4.0
  - Added support for XOR operations in Tamarin as a new built-in, as described in the CSF 2018 paper (https://hal.archives-ouvertes.fr/hal-01780544): "Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR"

  - Voting protocol models for "Alethea" added, described in "A Provably Secure Random Sample Voting Protocol", also at CSF 2018

  - Better mirror displays in equivalence mode

  - Numerous bug fixes

  - Using stack LTS resolver 11.7 now

* 1.2.3
  - GUI shows warnings on load that previously were only shown on command line

  - Additional warnings emitted on undefined (i.e., never defined in a rule) actions when only used in restrictions (lemmas already did this)

  - New oracle ranking heuristic=O added that uses the default smart heuristic as base. Oracles can now be given in files with any name, with the option --oraclefile=FILE

  - Rule coloring option added

  - Prevent reuse of builtin function names by user-defined theory

  - New built-in theory for signing which reveals the signed message

  - Various performance improvements and bug fixes

  - Now building with stack LTS resolver 10.7 with ghc-8.2.2


* 1.2.2
  - "partial deconstructions" text added to cases with partial deconstructions, which makes them searchable.

  - Improved visualization of mirrors/attacks in ObsEq diff-mode.

  - Running "tamarin-prover --version" now shows more detail.

  - Various performance improvements and bug fixes.

  - Upgrade to stack lts-8.5.

* 1.2.1
  - Upgrade to GHC 8.0.2 and stack lts-8.2.

  - Removed dependency from the derive package.

* 1.2.0
  - Extension for non-subterm convergent equational theories with FVP,
    as documented in the POST 2017 publication: 
    https://hal.inria.fr/hal-01430490
  
  - Included SAPIC, which is automatically built if OCAML is available. If
    Tamarin is called on a .sapic file, it first automatically translates
    to .spthy and then runs the Tamarin prover.

  - Upgraded to GHC 8 and stack resolver lts-7.18.

  - Multiple bug fixes.

  - Changed terminology: axioms are now called restrictions, and [typing]
    lemmas are now [sources] lemmas, also associated GUI changes. 
    Solves issue #177.

* 1.0.0
  - Change build system to use stack, see https://stackage.org,
    builds with lts-2.22 (GHC 7.8)

  - Adds observational equivalence feature. Available via --diff flag.

  - Some minor fixes:
     + issue #144
     + saving and loading theories with proofs

* 0.9.0
  - Improve build-stability by switching to Stackage-based precise
    version-constraints: tamarin-prover should now build under GHC
    7.8.4, GHC 7.6.2, and GHC 7.4.2. See

      https://travis-ci.org/tamarin-prover/tamarin-prover

    for it's build status.

  - Make executable relocatable => this means we can now offer pre-built
    binaries. This is the preferred way for distributin tamarin-prover. We no
    longer support publishing to Hackage and downloading from Hackage.

  - We no longer include examples, manuals, and licence files. They should be
    downloaded from the github repository:
    https://github.com/tamarin-prover/tamarin-prover

* 0.8.6.0
  - Incorporate a patch contributed by Ognjen Maric that improves reasoning
    about injective facts in inductive proofs.

* 0.8.5.1
  - Added KEA+ models with adversarial key registration.
  - Make case splitting more extensive. This possibly increases precomputation
    time, but in some cases it enables proving more properties.
  - fix: restrict aeson depedency to 0.6.*

* 0.8.5 Dropped support for GHC 7.0.x and GHC 7.2.x in favor of GHC 7.6.x

  - fix: faster and simpler variant computation
  - fix: parse errors when loading files with non-ASCII characters from GUI
  - fix: compiles with GHC 7.6.x

* 0.8.4
    features:
      1. irreducible function symbols are now allowed in formulas
      2. Support for an AC operator "+" which can also be used
         in formulas.
         See the examples
           - "ake/bilinear/{Joux,TAK1}.spthy" for modeling multisets,
           - "features/multiset/counter.spthy" for modeling natural
             numbers as counters, and
           - "ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching.spthy" for
             modeling lists with an "isPrefixOf" operation.
         See below for documentation.
      3. Support for reasoning about protocols that use bilinear pairing
         (see "ake/bilinear/" for examples).
      4. Support for private function symbols (see "cav13/DH_example.spthy"
         and "features/private_function_symbols/" for examples.

    documentation:
      - Schmidt's PhD thesis on "Formal Analysis of Key Exchange and Physical
        Protocols" is now available online at

          http://www.infsec.ethz.ch/research/software/tamarin

        and provides a detailed explanation of the theory and application of
        Tamarin including the reasoning about Diffie-Hellman exponentiation
        and bilinear pairing.

    new protocol models (most of them referenced in Schmidt's thesis):
      - Identity-based key exchange protocols (RYY, Scott, Chen-Kudla)
      - tripartite group key exchange protocols (Joux, TAK1)
      - multiprotocol scenarios for 3-pass AKE protocols (DHKEA+NAXOS-C, UM-C+UM-1)
      - new Yubikey models that model counters with multisets (contributed by
        Robert Künnemann).

* 0.8.2.1 bugfix release
    Should fix the ominous "no such lemma or proof path" GUI bug.

* 0.8.2.0
    documentation:
      - The submitted draft of the Meier's PhD thesis on "Advancing Automated
        Security Protocol Analysis" is now available online at

          http://www.infsec.ethz.ch/research/software/tamarin

        It explains the theory underlying Tamarin in much more detail than our
        CSF'12 paper. It also explains the theory underlying trace induction
        and type assertions.

    user interface:
      - allow lemma selection with '--prove': The lemmas being analyzed are the
        ones whose name is an extension of one of the prefixes given with a
        '--prove' flag.
      - disallow parsing of reserved rule names:
        Fresh, irecv, isend, coerce, fresh, pub

    new protocol models (referenced in Meier's PhD thesis):
      - models of TESLA Scheme 1 and 2
      - modeled the
      - injective agreement for TLS and NSLPK

      - include the contributed YubiKey models from:
        "R. Kuennemann and G. Steel. Yubisecure? formal security analysis
        results for the Yubikey and YubiHSM. In Proc. of the 8th Workshop on
        Security and Trust Management (STM 2012), Pisa, Italy, September 2012."

      - minimal hash chain example: this demonstrates a short-coming in our
        current proof calculus. It does not suffice to reason about iterated
        function application.

    architectural changes:
      - upgraded the GUI to use version 1.1 of the Yesod web-framework
      - split off Theory module hierarchy as a separate library called
        'tamarin-prover-theory'


* 0.8.1.0
    - enabled parallelization by default when compiling `tamarin-prover` with
      GHC 7.4 and higher. It uses as many threads as there are CPU cores on
      the system. Use `tamarin-prover +RTS -N1 -RTS` to use only one thread.

    - fixed: lemmas proven for some trace ('exists-trace') and marked with
        the [reuse] attribute were wrongly used in the proof of other lemmas.
    - fixed: axioms that are not safety formulas were not transformed
        properly when applying induction.
    - fixed: fresh name generation was not always handled properly when
        applying a precomputed case distinction to a goal that uses
        DH-exponentiation. Security protocol models that use DH-exponentiation
        should be checked again. Some of our case studies were indeed missing
        a few cases, but no property changed its validity.
    - fixed: no more case names containing spaces,
        when solving deconstruction chains.
    - fixed: avoid solving KU-goals for nullary function symbols

* 0.8.0.0
    - new homepage:  http://www.infsec.ethz.ch/research/software/tamarin
    - mailing list:  https://groups.google.com/group/tamarin-prover
    - issue tracker: https://github.com/tamarin-prover/tamarin-prover/issues

    - GUI:
        - new: added shortcuts for bounded autoprover and searching for all
          solutions, which can be used to characterize the set of solutions of
          a constraint system.

        - improved: pretty-printing of formulas and constraint systems using
          Unicode characters.

    - .spthy files:
        - new: support for restricting the set of considered traces using
          axioms. This allows for example to conveniently model equality
          checks using actions and a corresponding axiom. See the 'Tutorial'
          for more information.

        - new: proof checking support. This allows you to save interactive
          proofs from the GUI for later verification. Just copy the proof or a
          prefix of the proof into your input file. 'sorry' steps are
          then automatically expanded when using 'tamarin-prover --prove'.

        - new: formulas can now use mathematical symbols represented using
          their Unicode characters.

        - removed: support for (* ... *) style comments.

    - prover:
        - We now use the following additional normal form condition.

            > There is no edge (i,1)>->(j,1) between two exponentiation rules
            > i and j.

          This removes the need for exponentiation tags and thereby simplifies
          the constraint-reduction rules, both in theory and in code. Note
          that the arity of the 'KU' fact changed from arity two to arity one.
          Theories using typing invariants must thus be adapted, which is the
          reason for the minor version bump.

        - improved: error messages of wellformedness checks
        - reduced: memory usage of the autoprover by a factor 2 to 10.
        - improved parallelization: 10% speed increase on an i7 Quad-Core

    - editor support: Tomas Zgraggen contributed a syntax highligthing file
      for .spthy files for Notepad++ (http://notepad-plus-plus.org/).  This is
      great text editor for Windows. The syntax-highlighting file is installed
      in the same directory as the 'examples' directory under
      'etc/notepad_plus_plus_stphy.xml'.

    - fixed: bug in unique facts computation and application.
    - fixed: induction now generates cases for the empty and the non-empty trace
    - fixed: We no longer use local 'tamarin-prover-img' directories to cache
             rendered constraint systems. All images are now cached in
             a 'tamarin-prover-cache/img' subdirectory of the OS specific
             temporary directory.

* 0.6.1.0
   - fixed: parallel exploration of proof tree was using too much memory
   - fixed: reference to Tutorial.spthy broken in help message

* 0.6.0.0
   - open-sourced the code: https://github.com/tamarin-prover/tamarin-prover

   - core prover:
       - Normal form construction rules now log their conclusion as a
         KU-action. This allows to refer to the conclusions of construction
         rules in security properties. We exploit this to formalize typing
         invariants, which describe the structure of the instantiation of
         message variables precisely enough for getting rid of
         Chain-constraints starting from these message variables.

       - Reimplemented the constraint solver using a modified set of
         constraint rules that also supports attack extraction, when using
         inductive strengthening of security properties. As a nice side effect
         this allowed us to get rid of implicit construction dependencies.
         Moreover, the new prover's code is extensively documented, thereby
         facilitating further extensions.

       - Removed preliminary support for typing invariants based on
         Ded-actions and the deducible-before-atom (--|).

       - See the MANUAL for an explanation of the theory that we changed with
         respect to our CSF'12 paper.

   - GUI:
       - action atoms are also displayed graphically
       - the autoprover now respect all flags from the command line; e.g.,
         using `tamarin-prover interactive --bound=7` will give you a
         bounded-depth prover in the interactive GUI.

* 0.4.1.0
   - core prover:
       - detect maude errors earlier

   - GUI
       - support for SVG output
       - the network interface for the webserver is configurable now

   - bugfixes:
       - fix unit-test executed by 'test' mode

* 0.4.0.0 The version we used for our CSF'12 paper

   - core prover:
       - improved speed of constraint solver
       - improved goal selection heuristic
       - compute better loop-breakers for precomputing case splits
       - experimental support for partial forward evaluation
       - experimental support for loop invariants about construction rules

   - input syntax:
       - allow searching for trace existence using 'exists-trace'
       - allow local let-block in rule definitions

   - GUI:
       - normalize variable indices before display
       - more compact and beautiful default style for graph layout

   - bugfixes: quite a slew, most notably
       - compilation on Windows and GHC 7.4.1
       - intruder rule generation works now correctly again

* 0.1.1.0 Bug-fix release

  - fixed: automatically create output directory, if it does not exist
  - fixed: wrong flags given in help message for starting interactive mode

* 0.1.0.0 First public release