Changelog of @hackage/scyther-proof 0.10.0.1

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