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]

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]

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]

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 "TAMARINNOMAUDE_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, 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

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