Commit Graph

1537 Commits

Author SHA1 Message Date
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
Cas Cremers
49e34e5167 CLEANUP: Forgotten garbage collection. 2012-05-01 14:27:38 +02:00
Cas Cremers
d713ac400d More 'read'->'recv' conversion. 2012-04-26 16:40:01 +02:00
Cas Cremers
3a6d65463f Improving error reporting on wx import errors. 2012-04-26 14:27:00 +02:00
Cas Cremers
5b985af776 Refactoring order of module loading for better error reporting. 2012-04-26 13:41:07 +02:00
Cas Cremers
98dd606404 Adding agreement etc. to NS/NSL protocol. 2012-04-25 22:09:46 +02:00
Cas Cremers
9b0915441f Synchronising MPA branch with compromise branch where possible. 2012-04-25 17:03:51 +02:00
Cas Cremers
19359f9ba9 Inherited tempfile setup from compromise branch. 2012-04-25 16:19:21 +02:00
Cas Cremers
ab324fcea8 Added syntax check for usage of agreement. 2012-04-25 15:30:15 +02:00
Cas Cremers
2242a5fcbd Fixing read->recv conventions. 2012-04-25 09:53:07 +02:00
Cas Cremers
64e70ea4ea Fixing artefact with 'read' commands. 2012-04-24 13:33:00 -06:00
Cas Cremers
1cbe9826ac Updated dates. 2012-04-24 13:56:51 +02:00
Cas Cremers
626385821a Minor restructuring and fallback error even even tkInter is not installed. 2012-04-24 12:34:42 +02:00
Cas Cremers
755c4519c6 Large pass on protocol specification files to get rid of deprecated constructions. 2012-04-23 15:53:28 +02:00
Cas Cremers
30006b732a Fix Python 3 deprecated issues that cannot be resolved by 2to3. 2012-04-23 15:02:06 +02:00
Cas Cremers
b6ab044cd6 BUGFIX: 'Default' color not known to newer wxPython versions.
The statement was redundant anyway.
2012-04-09 21:14:41 +02:00