* 0.8.0.0
- new homepage: http://www.infsec.ethz.ch/research/software/tamarin
- mailing list: https://groups.google.com/group/tamarin-prover
- issue tracker: https://github.com/tamarin-prover/tamarin-prover/issues
- GUI:
- new: added shortcuts for bounded autoprover and searching for all
solutions, which can be used to characterize the set of solutions of
a constraint system.
- improved: pretty-printing of formulas and constraint systems using
Unicode characters.
- .spthy files:
- new: support for restricting the set of considered traces using
axioms. This allows for example to conveniently model equality
checks using actions and a corresponding axiom. See the 'Tutorial'
for more information.
- new: proof checking support. This allows you to save interactive
proofs from the GUI for later verification. Just copy the proof or a
prefix of the proof into your input file. 'sorry' steps are
then automatically expanded when using 'tamarin-prover --prove'.
- new: formulas can now use mathematical symbols represented using
their Unicode characters.
- removed: support for (* ... *) style comments.
- prover:
- We now use the following additional normal form condition.
> There is no edge (i,1)>->(j,1) between two exponentiation rules
> i and j.
This removes the need for exponentiation tags and thereby simplifies
the constraint-reduction rules, both in theory and in code. Note
that the arity of the 'KU' fact changed from arity two to arity one.
Theories using typing invariants must thus be adapted, which is the
reason for the minor version bump.
- improved: error messages of wellformedness checks
- reduced: memory usage of the autoprover by a factor 2 to 10.
- improved parallelization: 10% speed increase on an i7 Quad-Core
- editor support: Tomas Zgraggen contributed a syntax highligthing file
for .spthy files for Notepad++ (http://notepad-plus-plus.org/). This is
great text editor for Windows. The syntax-highlighting file is installed
in the same directory as the 'examples' directory under
'etc/notepad_plus_plus_stphy.xml'.
- fixed: bug in unique facts computation and application.
- fixed: induction now generates cases for the empty and the non-empty trace
- fixed: We no longer use local 'tamarin-prover-img' directories to cache
rendered constraint systems. All images are now cached in
a 'tamarin-prover-cache/img' subdirectory of the OS specific
temporary directory.
* 0.6.1.0
- fixed: parallel exploration of proof tree was using too much memory
- fixed: reference to Tutorial.spthy broken in help message
* 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