Commit Graph

1563 Commits

Author SHA1 Message Date
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
Cas Cremers
a911f56705 Added ISO/IEC 9798 models. 2012-11-15 12:10:06 +01:00
Cas Cremers
65713fd508 Merge branch 'master' of github.com:cascremers/scyther 2012-11-15 11:49:37 +01:00
Cas Cremers
03f49d3b29 Added IKE .spdl files (auto-generated from the .cpp files) for reference. 2012-11-15 11:48:46 +01:00
Cas Cremers
34d7cba293 Added IKE base models.
Modelers: Adrian Kyburz and Cas Cremers
2012-11-15 11:48:14 +01:00
Cas Cremers
e76c8cfb6f Added README.md for Github. 2012-11-14 22:10:05 +01:00
Cas Cremers
5918bf1a3c Fixed MAC 32-bit problem in a nicer way. 2012-10-24 16:13:05 +02:00
Cas Cremers
1bbd2f1ab7 Introduced markers in proof output for consistency with book description. 2012-10-02 13:43:30 +02:00
Cas Cremers
10c62a6863 BUGFIX: Opening files was not always performing as expected. Fixed now. 2012-10-02 13:42:48 +02:00
Cas Cremers
fc72b5f6ff Removed remaining 'Const' declarations. 2012-07-12 13:36:40 +02:00
Cas Cremers
bb3cea7548 BUGFIX: Adversary was weakened in a previous commit wrt symmetric-key protocols.
After we merged some concepts from the compromise branch, we forgot to add
for the hardcoded PKI that the adversary also should have access to (some) symmetric
keys.
2012-07-09 11:24:42 +02:00
Cas Cremers
d44e131f63 Improved goal selection heuristic and trivial goal skipping.
After the various changes, we were no longer correctly skipping terms like pk(IV#0),
even though it is a trivial goal. This patch fixes the issue.
2012-06-12 23:12:15 +02:00
Cas Cremers
61c451d7f8 Added public functions list to knowledge structure and added AddFunction for it. 2012-06-12 23:12:15 +02:00
Cas Cremers
214e3ed09f BUGFIX: 'Empty' claims can have any arguments. 2012-06-12 23:12:14 +02:00
Cas Cremers
b81db8e9b7 Fixing remaining 'read's to 'recv'. 2012-06-12 23:12:14 +02:00