* 0.8.5 Dropped support for GHC 7.0.x and GHC 7.2.x in favor of GHC 7.6.x - fix: faster and simpler variant computation - fix: parse errors when loading files with non-ASCII characters from GUI - fix: compiles with GHC 7.6.x * 0.8.4 features: 1. irreducible function symbols are now allowed in formulas 2. Support for an AC operator "+" which can also be used in formulas. See the examples - "ake/bilinear/{Joux,TAK1}.spthy" for modeling multisets, - "features/multiset/counter.spthy" for modeling natural numbers as counters, and - "ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching.spthy" for modeling lists with an "isPrefixOf" operation. See below for documentation. 3. Support for reasoning about protocols that use bilinear pairing (see "ake/bilinear/" for examples). 4. Support for private function symbols (see "cav13/DH_example.spthy" and "features/private_function_symbols/" for examples. documentation: - Schmidt's PhD thesis on "Formal Analysis of Key Exchange and Physical Protocols" is now available online at http://www.infsec.ethz.ch/research/software/tamarin and provides a detailed explanation of the theory and application of Tamarin including the reasoning about Diffie-Hellman exponentiation and bilinear pairing. new protocol models (most of them referenced in Schmidt's thesis): - Identity-based key exchange protocols (RYY, Scott, Chen-Kudla) - tripartite group key exchange protocols (Joux, TAK1) - multiprotocol scenarios for 3-pass AKE protocols (DHKEA+NAXOS-C, UM-C+UM-1) - new Yubikey models that model counters with multisets (contributed by Robert Künnemann). * 0.8.2.1 bugfix release Should fix the ominous "no such lemma or proof path" GUI bug. * 0.8.2.0 documentation: - The submitted draft of the Meier's PhD thesis on "Advancing Automated Security Protocol Analysis" is now available online at http://www.infsec.ethz.ch/research/software/tamarin It explains the theory underlying Tamarin in much more detail than our CSF'12 paper. It also explains the theory underlying trace induction and type assertions. user interface: - allow lemma selection with '--prove': The lemmas being analyzed are the ones whose name is an extension of one of the prefixes given with a '--prove' flag. - disallow parsing of reserved rule names: Fresh, irecv, isend, coerce, fresh, pub new protocol models (referenced in Meier's PhD thesis): - models of TESLA Scheme 1 and 2 - modeled the - injective agreement for TLS and NSLPK - include the contributed YubiKey models from: "R. Kuennemann and G. Steel. Yubisecure? formal security analysis results for the Yubikey and YubiHSM. In Proc. of the 8th Workshop on Security and Trust Management (STM 2012), Pisa, Italy, September 2012." - minimal hash chain example: this demonstrates a short-coming in our current proof calculus. It does not suffice to reason about iterated function application. architectural changes: - upgraded the GUI to use version 1.1 of the Yesod web-framework - split off Theory module hierarchy as a separate library called 'tamarin-prover-theory' * 0.8.1.0 - enabled parallelization by default when compiling `tamarin-prover` with GHC 7.4 and higher. It uses as many threads as there are CPU cores on the system. Use `tamarin-prover +RTS -N1 -RTS` to use only one thread. - fixed: lemmas proven for some trace ('exists-trace') and marked with the [reuse] attribute were wrongly used in the proof of other lemmas. - fixed: axioms that are not safety formulas were not transformed properly when applying induction. - fixed: fresh name generation was not always handled properly when applying a precomputed case distinction to a goal that uses DH-exponentiation. Security protocol models that use DH-exponentiation should be checked again. Some of our case studies were indeed missing a few cases, but no property changed its validity. - fixed: no more case names containing spaces, when solving deconstruction chains. - fixed: avoid solving KU-goals for nullary function symbols * 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