All Versions
11
Latest Version
Avg Release Cycle
268 days
Latest Release
1286 days ago

Changelog History
Page 1

  • v1.6.0 Changes

    September 09, 2020

    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]

  • v1.4.1 Changes

    January 18, 2019

    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

  • v1.4.0 Changes

    May 07, 2018
    • 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

  • v1.2.3 Changes

    February 28, 2018
    • 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

  • v1.2.2 Changes

    May 29, 2017
    • 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.

  • v1.2.1 Changes

    February 22, 2017
    • โฌ†๏ธ Upgrade to GHC 8.0.2 and stack lts-8.2.
    • โœ‚ Removed dependency from the derive package.
  • v1.2.0 Changes

    February 20, 2017
    • 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.
  • v0.8.6.1

    June 08, 2014
  • v0.8.6.0

    February 16, 2014
  • v0.8.5.1

    February 07, 2014