Cas Cremers
9f60184ba7
Add isTermlistSetEqual code to compare sets that are encoded as lists.
2011-04-26 11:49:40 +02:00
Cas Cremers
8ec1908306
Added cost code to match compromise branch.
...
Includes some refactoring in cost.c.
2011-04-26 11:49:05 +02:00
Cas Cremers
e23c79f59d
CLEANUP: Refactored code.
2011-04-06 10:50:54 +02:00
Cas Cremers
d2375cdd2f
Added template for commits.
2011-04-06 10:50:43 +02:00
Cas Cremers
61c905e922
For consistency added termlist prepend macro.
2011-04-01 15:24:55 +02:00
Cas Cremers
93cbb3e0f8
NEW: Added --role-unique switch to enforce that an agent can perform only one role.
2011-04-01 15:24:14 +02:00
Cas Cremers
4ec5ea4232
Added helper protocol support.
...
This is not a full copy from the compromise branch. In particular,
some counts (in arachne.c) are missing, as well as the modified dot output (dotout.c).
2011-04-01 15:23:20 +02:00
Cas Cremers
2e7328e0df
Updated install document.
2011-03-31 15:03:58 +02:00
Cas Cremers
bc667f3f32
Improving some scripts; exploit cache better.
2011-03-31 15:02:49 +02:00
Cas Cremers
c2662abaef
More comments.
2011-03-31 15:01:50 +02:00
Cas Cremers
9959baf926
More ignore patterns.
2011-03-31 15:01:13 +02:00
Cas Cremers
da616c1198
Adding missing scripts.
2011-03-31 15:00:56 +02:00
Cas Cremers
a03f06ea41
BUGFIX: Auto-claim naming scheme was context dependent.
...
The automatic mechanism to assign labels to claims was dependent on the
context. In practice, a claim could get a different label when analyzed in
isolation compared to when analyzed in parallel with some other protocols. This
caused problems for the multi-protocol analysis.
2011-01-27 14:12:51 +01:00
Cas Cremers
810fc9eece
Fixed wiper display.
2011-01-27 10:57:54 +01:00
Cas Cremers
c02ce53227
Adding make-bsub.py, which is needed by batcher.sh.
2011-01-26 13:21:02 +01:00
Cas Cremers
6cb4313bec
Brutus support restored the batcher script.
2011-01-26 13:18:29 +01:00
Cas Cremers
fea2bcf477
Reindenting code.
2011-01-25 17:33:12 +01:00
Cas Cremers
68409e14ad
Synchronise test batch files.
2011-01-25 17:32:54 +01:00
Cas Cremers
214c607529
Slightly nicer code.
2011-01-25 17:32:19 +01:00
Cas Cremers
1814a2d7b3
BUGFIX: Removed obsolete code that was destroying commit/agreement functionality when filtering.
...
This is now (and has been for a while) handled by other code.
2011-01-25 17:30:59 +01:00
Cas Cremers
6286a2c810
Added test scripts for book and iso.
2011-01-25 10:24:37 +01:00
Cas Cremers
88ee944c4b
BUGFIX: Problem when progressbar.py missing, problem with zero correct claims.
2011-01-24 21:39:35 +01:00
Cas Cremers
19749e0293
Being more careful about adding scripts etc.
2011-01-24 20:58:53 +01:00
Cas Cremers
f883499d07
CHANGE: Changed setup of running & commit.
...
Now:
claim(A,Commit,B,data) => claim(B,Running,A,data) and also B is running the right protocol and role.
2011-01-24 17:32:24 +01:00
Cas Cremers
b01bfc4dcd
Merge branch 'MPA' of ssh://brutus.ethz.ch/~/src/scyther-MPA into MPA
2011-01-21 17:40:47 +01:00
Cas Cremers
fda39f7eab
BUGFIX: Skipping running/commit signals caused bugs in graphviz output.
2011-01-21 17:40:10 +01:00
Cas Cremers
be6f7b481d
Updating mpa test scripts.
2011-01-21 17:39:05 +01:00
Cas Cremers
985397c8b6
Cache structure change: from Cache/XX/file to Cache/XX/YY/file
2011-01-21 17:38:45 +01:00
Cas Cremers
63aefc1c46
BUGFIX: makedirs wasn't working as expected, reverting to builtin.
2011-01-21 17:38:14 +01:00
Cas Cremers
fa8440c8e5
BUGFIX: Silly typo.
2011-01-18 17:05:07 +01:00
Cas Cremers
5f7138c300
BUGFIX: Partial implementation of chosen name attacks could yield false type flaw attacks.
...
For the typed model, this was not an issue.
2011-01-18 17:03:20 +01:00
Cas Cremers
b7ab9aefeb
NEW: Added default SessionKey type.
2011-01-04 15:50:47 +01:00
Cas Cremers
66e18deb3f
NEW: Added claims: Commit and Running.
...
There are two new claims:
claim(X,Commit,t) : check for agreement on data
claim(X,Running,t) : signaling claim
The property checked is that each claim Commit needs to be preceded by a Running
with an identical term t.
Cherry-picked from commit 99a6be00e9d3d219ec73665607e8a3a7d65d04d1
2011-01-04 15:50:25 +01:00
Cas Cremers
2fb0ecde97
NEW: Added Aliveness and Weak Agreement claims.
2011-01-04 15:50:25 +01:00
Cas Cremers
6afcfe1d10
NEW: Added SID & SKR dummy claims.
...
This allows for input file reuse among branches (i.e. compromise).
2011-01-04 15:50:25 +01:00
Cas Cremers
04787e5516
Re-allowing positional arguments for test-mpa.py, i.e., command line specification of input files.
2011-01-04 14:14:35 +01:00
Cas Cremers
af25cfc9a0
Better MPA scans and added pickle/JSON output options.
2010-12-31 15:43:27 +01:00
Cas Cremers
9624c49885
Disable some aggressive error reporting: unclear why this is actually invalid per se
...
in the presence of agent name variables (role names) with non-basic typing.
2010-12-31 15:43:00 +01:00
Cas Cremers
ed147bbace
Bugfix on empty input.
2010-12-31 15:42:01 +01:00
Cas Cremers
59080a2b5c
Updating protocol descriptions.
2010-12-31 15:41:52 +01:00
Cas Cremers
94c9f1b444
No longer stop at first MPA attack: scan for all.
2010-12-27 22:31:15 +01:00
Cas Cremers
5ee0f7563b
Improving latex output of MPA test, expanding glue functionality.
2010-12-27 22:30:58 +01:00
Cas Cremers
b6c67dec23
Initial latex output option that generations correct claims table.
2010-12-27 13:32:25 +01:00
Cas Cremers
5ffe3d2752
Added more verbosity to some parts with -v switch.
...
In particular, verbose ('-v', '--verbose') now lists protocols with their correct
claims, and also the protocols without such correct claims.
2010-12-26 23:10:39 +01:00
Cas Cremers
a21aeccad0
Fix caching discrepancy when relying on Scyther default options.
2010-12-26 23:09:30 +01:00
Cas Cremers
dd49526e02
Reintroduced ksl protocol description.
2010-12-12 22:13:18 +01:00
Cas Cremers
2ec70106ba
MPA: Improved the attack summaries.
2010-11-24 17:13:26 +01:00
Cas Cremers
d96ffa3354
Added more Woo-Lam-Pi variants.
2010-11-24 17:13:14 +01:00
Cas Cremers
cecff7f55e
Refactoring options.
2010-11-23 15:09:43 +01:00
Cas Cremers
3007887f38
Near complete rewrite of the MPA test script.
2010-11-15 23:20:48 +01:00
