tamarin-prover v1.6.0 Release Notes
Release Date: 2020-09-09 // over 4 years 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