1.8.0

• Support for natural numbers and subterm reasoning

• Internal 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 global 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

• 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

• 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, see manual for details

  • 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

• 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.

tamarin-prover version 1.2.1

• Upgrade to GHC 8.0.2 and stack lts-8.2.
• Removed dependency from the derive package.

tamarin-prover version 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.