Changelog for scyther-proof-0.8.0.0If this renders badly as markdown, see the plain text version
- upgraded dependency on Isabelle to Isabelle-2013-2
- ported to Isabelle-2013 by Andreas Lochbihler
- removed buggy isabelle timout support
- tested compilation on GHC 7.4.2
- 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.