tamarin-prover v1.6.0 Release Notes

Release Date: 2020-09-09 // about 1 year ago

    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]

Previous changes from v1.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