* 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.