Commit Graph

1702 Commits

Author SHA1 Message Date
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
Cas Cremers
727e813c77 Fixed obsolete notation in protocol specification files.
Not everything is fixed yet.
However, we fixed:
- 'const' -> 'fresh'
- Removed lines specifying 'runs'
- Removed some specifications of compromised Eve and its long-term keys
  being compromised.
2012-06-12 23:12:14 +02:00
Cas Cremers
2ba0de6abc New refactoring of build system for linux, should be clearer.
We also avoid building the w32 binary by default.
2012-06-12 23:12:14 +02:00
Cas Cremers
f408e61b00 Removed obsolete script. 2012-06-12 23:12:14 +02:00
Cas Cremers
b26482feca Started script to describe version. 2012-06-12 23:12:14 +02:00
Cas Cremers
163a915a6d Added regression test script. 2012-06-12 23:12:14 +02:00
Cas Cremers
588ae30bef Removing obsolete 'c-minimal' terminology. 2012-05-02 10:15:45 +02:00
Cas Cremers
ca5c7eaa49 Adding weakagree claim to nsl3. 2012-05-02 10:15:33 +02:00
Cas Cremers
6fabb3b1b4 Improved checking of required parameters for various claims with informative error reporting. 2012-05-01 16:37:28 +02:00
Cas Cremers
8d0b704635 Added weak agreement claims to NS. 2012-05-01 16:37:04 +02:00
Cas Cremers
ccae884942 Rephrasing comments. 2012-05-01 15:02:45 +02:00
Cas Cremers
5608b29dc0 Refactored first_origination code. 2012-05-01 14:46:01 +02:00