Previously, if a local (non-role) variable would have (implicit) agent type,
it would be assigned a concrete term before the roles. This would lead to
non-optimal choices, since we care more about the role instantiations than about other variables.
However, when making traces concrete, we use the run's 'locals' list. Because of
the way this is constructed (in reverse), non-role variables precede the role variables.
We therefore choose to traverse the list in reverse.
When an attack pattern is displayed, Scyther instantiates open variables with concrete names.
This is often more intuitive for humans.
In the case of instantiating role names, we often ended up assigning Alice to the B role and
Bob to the A role. This patch provides a more clever heuristic to find agent names
that start with the same letter as the role (variable) name. In case this fails, we
still try to map Alice to roles starting with 'I' and Bob to 'R', and otherwise we just pick something.
Also added "Simon" and "Pete" to cover some common role names.
Conflicts:
src/arachne.c
The option parser wrapper allocated memory in an incorrect way, which
could lead to problems especially with --xml-output, since it would
access the memory at a later point in the execution. This could then
propagate to GUI problems, since the GUI uses the --xml-output switch.
Rewrote the code to be more readable and less incorrect.
This patch addresses two 64-bit platform compilation issues:
- Force 32-bit mode for gcc using '-m32'
- Recent library modifications broke the 32-bit compilation on 64-bit machines: updated
'compile.txt' to include the need for the 'gcc-multilib' package.
The previous way of selecting fonts was an obsolete hack. Some recent versions of wxPython
ran into problems. Now updated to reflect the correct wxPython font selection conventions.
Bug report and fix suggestion by S. Dismore.
After the new function implementation, the 'Function' type is no longer one-way by default.
However, many protocol description files relied on this implicit assumption.
The solution is to use 'hashfunction' declarations instead to model one-wayness.
Original bug report by Binh Thanh Nguyen.
Recent versions of Graphviz no longer set the PATH variable on Windows.
Hence Scyther can fail to find dot.exe even though Graphviz was appropriately
installed.
This patch is a hack to try and locate dot.exe in the more common locations.
We currently have a hardcoded search through:
C:\Program Files\Graphviz*
C:\Program Files (x86)\Graphviz*
This is clearly fragile. Obviously, nobody should be solving Graphviz' problem
in such an ugly way. Change drives or languages and it stops working.
Until Graphviz provides at least an alternative environment variable (GVPATH?)
this hack will help the bulk of our users to get things up and running smoothly.
Shlex is only intended to work for Unix-like shells, and using it on
Windows causes problems. We now resort to simply always using the shell
on Unix-like platforms (as our command input is always a string, and not
an array). On Windows, the string input is always okay, even when not
using the shell.
This is a follow-up to a bug report by M. Kammerer on failing Windows
installs.
Previously, pressing 'cancel' in the verification window would leave a dangling scyther backend process.
Now the process gets correctly killed.
The following changes enable this:
- External processes are no longer invoked through the shell (otherwise they are subprocesses of the shell and cannot be reliably killed cross-platform).
- The 'safeCommand' procedure now has a hook for passing opened Popen objects.
- The GUI stores and kills the Popen objects on cancel or window close.
To do: an alternative interface for this in 'safeCommand' could expose a 'killMe' method through a callback; this might be cleaner in the long term.
For now, some parameters are hardcoded.
In the long term this functionality should be incorporated into the Scyther library directly, as
a method of Claim objects.
Changes:
1. Reverted restricted use of 'hashfunction': 'function' can now be used as an alternative (but they are identical).
2. Functions can be specified to be secret, as we had before.
Together with the newer 'inversekeyfunctions' declaration, this allows for the clean definition of alternative key infrastructures.
Example usage:
secret function sk2;
function pk2;
inversekeyfunctions (sk2,pk2);
Conflicts:
src/compiler.c
Previously, weak agreement and aliveness claims would enforce a requirement for all agents in the range
of the rho of the claim run.
For some three-party protocols this was stronger than needed. We now allow an
optional role name parameter for these claims; if such a parameter is used, the claim
is only evaluated for the agents performing that role.
En passant fixed a potential bug: aliveness and weak agreement require a run for each
agent, but previously we didn't check if these were helper protocols. Clearly they
should not be.
