Changelog of @hackage/scyther-proof 0.6.0.0

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