* 0.6.0.0
- open-sourced the code: https://github.com/tamarin-prover/tamarin-prover
- core prover:
- Normal form construction rules now log their conclusion as a
KU-action. This allows to refer to the conclusions of construction
rules in security properties. We exploit this to formalize typing
invariants, which describe the structure of the instantiation of
message variables precisely enough for getting rid of
Chain-constraints starting from these message variables.
- Reimplemented the constraint solver using a modified set of
constraint rules that also supports attack extraction, when using
inductive strengthening of security properties. As a nice side effect
this allowed us to get rid of implicit construction dependencies.
Moreover, the new prover's code is extensively documented, thereby
facilitating further extensions.
- Removed preliminary support for typing invariants based on
Ded-actions and the deducible-before-atom (--|).
- See the MANUAL for an explanation of the theory that we changed with
respect to our CSF'12 paper.
- GUI:
- action atoms are also displayed graphically
- the autoprover now respect all flags from the command line; e.g.,
using `tamarin-prover interactive --bound=7` will give you a
bounded-depth prover in the interactive GUI.
* 0.4.1.0
- core prover:
- detect maude errors earlier
- GUI
- support for SVG output
- the network interface for the webserver is configurable now
- bugfixes:
- fix unit-test executed by 'test' mode
* 0.4.0.0 The version we used for our CSF'12 paper
- core prover:
- improved speed of constraint solver
- improved goal selection heuristic
- compute better loop-breakers for precomputing case splits
- experimental support for partial forward evaluation
- experimental support for loop invariants about construction rules
- input syntax:
- allow searching for trace existence using 'exists-trace'
- allow local let-block in rule definitions
- GUI:
- normalize variable indices before display
- more compact and beautiful default style for graph layout
- bugfixes: quite a slew, most notably
- compilation on Windows and GHC 7.4.1
- intruder rule generation works now correctly again
* 0.1.1.0 Bug-fix release
- fixed: automatically create output directory, if it does not exist
- fixed: wrong flags given in help message for starting interactive mode
* 0.1.0.0 First public release