All Versions
11
Latest Version
Avg Release Cycle
268 days
Latest Release
1471 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