diff --git a/Design/scyther-button-beta6-angle.svg b/Design/scyther-button-beta6-angle.svg
index a55fb28..bcbb6d5 100644
--- a/Design/scyther-button-beta6-angle.svg
+++ b/Design/scyther-button-beta6-angle.svg
@@ -19,6 +19,18 @@
sodipodi:docname="scyther-button-beta6-angle.svg">
+
+
+
+
+ style="stop-color:#fc8024;stop-opacity:1;" />
+
-
-
-
-
+ gradientTransform="matrix(0.871233,-5.251187e-7,5.812853e-7,1.195697,2.060264,-4.477073)" />
+
+
+
+
+
+ gridempspacing="8"
+ inkscape:grid-points="true" />
@@ -192,6 +219,18 @@
+
+
+
+ width="27.870968"
+ height="30.980282"
+ x="2.0645161"
+ y="0.019719051" />
+ style="opacity:1;display:inline"
+ sodipodi:insensitive="true">
-
-
-
-
-
+ inkscape:groupmode="layer"
+ id="layer5"
+ inkscape:label="lock ring"
+ style="opacity:1;display:inline"
+ sodipodi:insensitive="true" />
+
+
+
+
+
+
+
+ style="display:inline"
+ sodipodi:insensitive="true">
+
+
+
+ style="opacity:1;fill:none;fill-opacity:1;fill-rule:evenodd;stroke:black;stroke-width:0.49999994;stroke-linecap:round;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1;display:inline" />
Scyther
+ x="19.062848"
+ y="6.5987983"
+ style="font-size:7.59374714px;font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;text-align:center;line-height:100%;writing-mode:lr-tb;text-anchor:middle;fill:white;fill-opacity:1;stroke:none;stroke-width:0.40000001;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;font-family:Consolas">SCYTHER
diff --git a/gui/Changelog.txt b/gui/Changelog.txt
index a431b8e..0e6aad0 100644
--- a/gui/Changelog.txt
+++ b/gui/Changelog.txt
@@ -4,13 +4,21 @@
Scyther 1.0-beta6
- * Added Mac support (added universal binary)
- * Fixed bug in scripting backend (e.g. with mpa.py)
- * Added claim parameter for Reachable claim; Reachable,R means
- that role R should be trusted (as well as the actor), but not
- any other claim. This can be useful for showing stronger
- authentication properties of protocols with more than two
- parties.
+ New features:
+
+ * [Gui] Added Mac support (added universal binary)
+ * [Language] Added claim parameter for Reachable claim;
+ Reachable,R means that role R should be trusted (as well as the
+ actor), but not any other claim. This can be useful for showing
+ stronger authentication properties of protocols with more than
+ two parties.
+ * [Backend] Added '--max-of-role=N' switch (to narrow scenarios)
+ * [Backend] Added '--scan-claims' switch (allows for retrieving a list of
+ claims)
+
+ Bugfixes:
+
+ * [Scripting] Fixed bug in python interface backend (e.g. with mpa.py)
Scyther 1.0-beta5
diff --git a/gui/Scyther/Bin/scyther-mac b/gui/Scyther/Bin/scyther-mac
index 12e4f04..d989476 100755
Binary files a/gui/Scyther/Bin/scyther-mac and b/gui/Scyther/Bin/scyther-mac differ
diff --git a/gui/Scyther/Bin/scyther-w32.exe b/gui/Scyther/Bin/scyther-w32.exe
index c33dd00..4c452c8 100755
Binary files a/gui/Scyther/Bin/scyther-w32.exe and b/gui/Scyther/Bin/scyther-w32.exe differ
diff --git a/src/notes.txt b/src/notes.txt
index 0889d39..6e52578 100644
--- a/src/notes.txt
+++ b/src/notes.txt
@@ -1,5 +1,10 @@
- (!!) Are the Arachne rules for keys that are variables sane? E.g. what
- is their inverse key? Check!
+ is their inverse key? Check! Intuition: one cannot know what the
+ inverse is of a non-instantiated key variable, given the current
+ semantics, if asymmetric keys are allowed.
+ Consequence: the current implementation is just fine, because
+ asymmetric key variables cannot be defined in the language. Thus, the
+ rules are fine. Investigate for the other case.
- If no attack/state output is needed, maybe the attack heuristic should
be simpler (which means just weighting the trace length etc.) in order
to avoid uneccesary continuation of the search. Maybe even stop
@@ -8,21 +13,5 @@
constants. This should works also with a modifier of sorts (e.g.
'predictable') and such constants should be leaked to the intruder at
the start of the run, possibly by prefixing a send.
-- The trace incremental search should start at something like 'distance of
- first claim + SOMECONST * runs'. SOMECONST relates to the partial-order
- induced trace prolonings.
-- Because the properties checked are related to the partial order reductions,
- it makes sense to check 'all secrecy claims' or 'all synchronisation claims'
- at once. This holds in a similar way for arachne.
-- Given originator assumptions and such, we might want to implement the
- compiler, that for non-typed matching, it will ignore all type definitions
- in the code (as in, putting them in stype, but still considering Function).
- Then, for 'any agent' we can use stype silently. The modelchecker should
- then always consider the types with -m0 and -m1.
-- In a paper concerning the CASRUL compiler, they mention associativity for
- the equality relations. Note that CASRUL restricts the intruder actions,
- and sometimes uses approximations.
-- Several memory leak detectors are still in place, they can all be located by
- searching for "lead" or "diff" and destroying the code.
- knowledgeAddTerm might be improved by scanning through key list only with
things that are newly added.
diff --git a/src/todo.txt b/src/todo.txt
index 1c82a08..855b3f6 100644
--- a/src/todo.txt
+++ b/src/todo.txt
@@ -8,10 +8,6 @@
cumbersome and might impact on performance. Alternatively, iterators
can be implemented as macros, which is probably the fastest, but maybe
less readable.
-- I've started on sanitizing the --max-attacks switch. It now prunes as a
- bound, but it also needs to limit per-claim, I guess.
-- There is something weird when automatically generating claim labels
- and trying to filter on them (try eg duplicates)
- --check is slightly f***ed up because there is no good semantics for
the --disable intruder check. As a result, it is now too strict can
cause correct protocols to fail. Fix.