CHANGES

* 0.10.0.1
    - make it compile with GHC 7.10.1

* 0.10.0.0
    - upgraded dependency on Isabelle to Isabelle2014
    - add support for explicit matching and non-matching steps in protocols
    - new protocol example for optimistic fair exchange

* 0.8.0.0
    - upgraded dependency on Isabelle to Isabelle-2013-2

* 0.6.0.0
    - ported to Isabelle-2013 by Andreas Lochbihler
    - removed buggy isabelle timout support
    - tested compilation on GHC 7.4.2

* 0.5.0.0
    - implemented proof generation for injective agreement
    - fixed bug in unification of inverse-key constructors

* 0.4.1.0 Bugfixes and dropped export of library
    - widen 'pretty' dependency
    - update package description

* 0.4.0.0 Bugfixes and dropped export of library

    - Compiles now with GHC 7.0.x, 7.2.x, 7.4.x
    - Fixed some corner cases in unification code for key-inversion.
    - Library is no longer exported, as there are no more users of it.
      We split our internal development and the tamarin-prover provides its
      own utility libraries.

* 0.3.2 Lexer improvements

    - Also lex SLASH and BACKSLASH symbols.


* 0.3.1 Bugfix, small enhancement release

    - Bugfix: Added missing cases for bidirectional shared keys in Message
      deconstruction functions.

    - Provide more precise warnings for internal certification checks. Improves
      debugging experience.

    - Updated documentation: UnionFind and .cabal project description

    - Allow parsing of user-specified type assertions. For protocols with
      nested encryptions, the inferred type assertions are sometimes not
      precise enough. We handle these cases using user-specified type
      assertions.

    - Removed support for weak-atomicity, as it is subsumed by type assertions.

    - Changed lexer to also recognize `!'

* 0.3.0 First public version

    Aligned with paper submission for CCS'11: Provably repairing the ISO-9798
    authentication protocols.