Commit Graph

1677 Commits

Author SHA1 Message Date
Cas Cremers
1a9d088aa8 Updated installation and compilation notes. 2013-12-11 16:48:20 +00:00
Cas Cremers
a7230702cb Cleanup of obsolete module import. 2013-12-09 14:25:11 +00:00
Cas Cremers
c9b1d08f4f Hack for Windows users to compensate for Graphviz "feature".
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.
2013-12-09 14:24:57 +00:00
Cas Cremers
7e3f0ed73b BUGFIX: Reverted use of shlex.
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.
2013-12-09 09:07:47 +00:00
Cas Cremers
1a9b494f85 Updating the protocol generator for the ffgg family.
- Removed obsolete declarations, updating syntax conventions.
- Added a more useful origin comment.
2013-11-18 16:59:11 +00:00
Cas Cremers
1b04bf9274 Updated changelog. 2013-10-13 10:34:49 +01:00
Cas Cremers
8f9dc0cb83 Updated manual. 2013-10-12 20:12:01 +01:00
Cas Cremers
d06247fcfe Updating time stamps for next release. 2013-10-05 23:56:12 +01:00
Cas Cremers
4e78a1d3fa Removing obsolete file. 2013-10-05 23:49:13 +01:00
Cas Cremers
2ee202b1ae Updated Denning-Sacco-Lowe note. 2013-08-23 15:15:19 +02:00
Cas Cremers
fe364fbe9d GUI: Canceling verification now also kills back-end thread.
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.
2013-06-30 23:14:28 +02:00
Cas Cremers
6473aba398 Misc: improving output of generate-attack-graphs.py script. 2013-06-20 10:32:16 +02:00
Cas Cremers
c11a4268b0 Misc: note in attack graphs script on how to produce time/memory consumption output as well (on Linux) 2013-06-20 09:54:56 +02:00
Cas Cremers
2004a0f4aa Misc: Added Python script to dump attack outputs for large sets of files.
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.
2013-06-19 23:03:46 +02:00
Cas Cremers
6134b46557 Backend DOT graph generation: Removing redundant ';' which seems to confuse more recent versions of Graphviz (>2.26) 2013-06-19 23:03:36 +02:00
Cas Cremers
45d5cb0a3a Cleanup: Cleanup of some spacing, conform coding conventions.
This is simply the result from running reindent.sh again.
2013-06-19 23:03:26 +02:00
Cas Cremers
c6280d745e Backend DOT graph generation: Removing debugging reporting of 'cost' in attack graphs.
This was confusing to casual users.
2013-06-19 23:02:58 +02:00
Cas Cremers
4263c81e52 Removing obsolete design files. 2013-06-10 16:21:09 +02:00
Cas Cremers
486633fecd Updating INSTALL file. 2013-05-24 12:32:04 +02:00
Cas Cremers
fe25a53232 Regression-fix: Reintroduced option for alternative PKI.
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
2013-05-24 11:27:14 +02:00
Cas Cremers
5c2eded8f9 Weakagree and Alive claims now also allow for a role parameter + BUGFIX.
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.
2013-05-24 11:27:14 +02:00
Cas Cremers
9e13d07b6e BUGFIX: Invoking Scyther scripts from non-standard directories or using symlinks should work consistently now.
Before, we were using both __file__ as well as sys.argv[0] to determine the base directory
for Scyther, and we were not taking symlinks into account.

By using the inspect module, we can consistently pick the current frame and derive
the file from that, then use realpath to strip symlinks.
2013-05-01 14:16:12 +02:00
Cas Cremers
7658644295 Rati Gelashvili reported a rare but annoying bug in the hash function handling.
The fix requires a significant reworking of the function handling. This
is a first attempt.

Conflicts:
	src/knowledge.c
	src/knowledge.h

Regression test suggests that the Hashfunction fix works.
2013-04-26 14:47:27 +02:00
Cas Cremers
4a1898db92 src/regression-tests: Consistent regression testing.
There is now a script

  src/regression-tests/regression-test.py

that should in the future be the default for running regression tests
instead of the ad-hoc approach we are currently using. The goal is to
ultimately have more reliable and consistent regression testing.

The script takes as input "tests.txt" and tries to perform tests from
that. This is effectively a collection of inputs to the scyther-linux
binary. The results are writting to the 'results' directory, as
test-X.out and test-X.err, where those correspond to stdout and stderr,
respectively. Additionally, a measurement of wall-clock time in seconds
is written to test-X.time.

For now, we are using the timer to ensure all tests terminate. It would
be nicer to use a less environment-dependent way of enforcing
termination.
2013-04-26 14:29:22 +02:00
Cas Cremers
b92c097b38 BUGFIX: Windows version had a compilation problem.
The use of 'strndup' in scanner.l caused problems for non-gnu modes of gcc, which
was being invoked for the mingw32 compilation. Replaced now by the more portable
strncpy + malloc version.
2012-12-17 20:51:42 +01:00
Cas Cremers
49097852d9 Fixing path. 2012-12-17 11:33:48 +01:00
Cas Cremers
6dc3b21859 Added current manual snapshot. 2012-12-17 11:32:58 +01:00
Cas Cremers
408a88807f Updated changelogs and readme's. 2012-12-17 11:26:04 +01:00
Cas Cremers
091ce01f60 Minor synchronisation updates. 2012-12-17 10:14:31 +01:00
Cas Cremers
1df5bf1fc3 Fixing typos. 2012-12-15 00:00:26 +01:00
Cas Cremers
35045adf69 NEW: Scyther input files can now specify any command-line option.
By specifying:

  option "--X=Y";

in the Scyther input file, command-line options can be directly integrated.

For example, one can specify:

  option "--one-role-per-agent";
2012-12-14 23:55:07 +01:00
Cas Cremers
d88402998e NEW: Added '--one-role-per-agent' switch.
This switch disallows agents from performing multiple roles.

Conflicts:
	src/prune_theorems.c
2012-12-14 17:06:55 +01:00
Cas Cremers
8372078d07 Corrected minor comment typos.
Conflicts:
	src/prune_theorems.c
2012-12-14 17:05:20 +01:00
Cas Cremers
fb28a98086 BUGFIX: In case sources are compiled outside of git, ran into error where trying to strip None. 2012-12-14 15:35:01 +01:00
Cas Cremers
ba5166bd84 NEW: Added environment variable "SCYTHERCACHEDIR" to determine cache usage.
If this variable is unset, Scyther writes into /tmp/Scyther-cache (or similar).
If this variable is set to "", caching is disabled.
Otherwise, Scyther writes into $SCYTHERCACHEDIR/Scyther-cache
2012-12-06 10:17:53 +01:00
Cas Cremers
6c7493838c Implemented well-formedness check as in the 2012 book.
We check that variables occur first in receive events.
2012-12-06 09:52:13 +01:00
Cas Cremers
7a2d354bac Added Wimax models from compositionality paper.
Previously we had not included the IEEE 802.16e Wimax PKM models to the
Scyther distribution, although the models had been around for years.
2012-11-27 21:56:05 +01:00
Cas Cremers
ae155f8169 We now also allow macro definitions in roles, and allow for macro overwrite.
In some cases, macro definitions within roles are more readable, for example for
key exchange protocols where the computations are asymmetrical.
2012-11-23 14:34:06 +01:00
Cas Cremers
a71fe51036 BUGFIX: Occurrence of multiple macro symbols in one tuple could lead to infinite loop.
The mechanism with the next pointers for tac's was working fine as long as all
tac's were unique by construction. The macro mechanism made it possible for
the same tac to occur twice in the tree. This could lead to an infinite loop.

Now we make explicit copies of the top-level tac. This should fix the problem
caused by the tuple parsing.

A more fundamental solution is to make a deep copy of the substituted terms.
2012-11-23 14:34:04 +01:00
Cas Cremers
1b4eb7cb54 BUILD: Added flag for Mac builds to enable building on 10.8 but allow also execution on 10.6 and 10.7. 2012-11-23 09:25:27 +01:00
Cas Cremers
d1537b1848 Catching other error message for wrong architecture.
Current wxPython packages only work in 32-bit mode. If we detect that there is
an error message complaining about the architecture, we restart scyther-gui.py using
python in 32-bit mode.
2012-11-23 09:25:19 +01:00
Cas Cremers
1648d14d98 Dropped Mac PPC support for now; only Intel binaries will be available. 2012-11-22 14:35:28 +01:00
Cas Cremers
0fb7e9e24e Added support for macro definitions.
It is now possible to declare syntactic macros at the global level.

  macro ID = TERM;

After this definition, every occurrence of ID will be replaced by TERM.
For example, this can be used to avoid duplicating message definitions
among roles:

  macro M1 = { nI, I}pk(R) ;

  protocol X(I,R) {
    role I {
      send (I,R, M1);
    }
    role R {
      recv (I,R, M1);
    }
  }
2012-11-22 12:30:00 +01:00
Cas Cremers
25da320128 BUGFIX to list-length code: classical case of uninitialized variable. 2012-11-22 12:27:05 +01:00
Cas Cremers
fedd729ab2 Added support for inequality tests.
There is a new event:

  not match(t1,t2)

where t1,t2 are terms.

They are implemented by using a special claim that simply stores the
intended inequality. The pruning theorems (prune_theorems.c) ensure that
these terms never become equal. If there are equal, the constraint is
violated. As long as they are not equal, there exists a solution using
groung terms such that their instantiation is not equal.

Currently not very efficient implemented and the graph out output is
also ugly for now.

Conflicts:
	gui/Scyther/Trace.py
	src/compiler.c
	src/scanner.l
2012-11-21 13:40:15 +01:00
Cas Cremers
d4faeacd1e Implemented equality/pattern matching support.
Introduced a new event:

  match(pattern,groundterm)

This event can only be executed if pattern can be matched to groundterm.
Variable substitutions are persistent with respect to later events in
the same role.

Currently implemented as syntactic sugar, essentially unfolded in role R to:

  fresh x;
  send ( R,R, { groundterm }x );
  recv ( R,R, { pattern }x );

This work is not complete yet in the send that the output still contains
the unfolding. Ideally, the graph rendered detects this syntactic sugar
and renders a simplified event. This should be possible on the basis of
the label name prefix.

Conflicts:
	src/compiler.c
	src/parser.y
	src/scanner.l
	src/tac.h
2012-11-21 13:34:56 +01:00
Cas Cremers
9c9c6758f2 Removing obsolete file. 2012-11-15 16:50:42 +01:00
Cas Cremers
51495be80d Cleanup and restructuring of testing directory setup. 2012-11-15 16:47:08 +01:00
Cas Cremers
1860527960 Added softlink to protocols directory. 2012-11-15 13:41:02 +01:00
Cas Cremers
6642782b0d Moved development protocol files to a better named directory. 2012-11-15 13:40:14 +01:00