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
Cas Cremers
08ae9a2ac9
MPA: Added code for testing self-initiator stuff.
2010-11-15 17:39:03 +01:00
Cas Cremers
edba6aac7f
MPA: Added --extravert option to pass on to backend.
2010-11-15 10:18:20 +01:00
Cas Cremers
135fbaf726
MPA: More detailed reporting of results.
2010-11-15 10:18:01 +01:00
Cas Cremers
31a1635a07
MPA: Added switch for the max number of parallel protocols in MPA attacks found.
2010-11-15 10:17:29 +01:00
Cas Cremers
f97afc4a62
MPA: Added --plain option for output to text files (disables progress bars)
2010-11-15 10:16:17 +01:00
Cas Cremers
b1f993a6c9
BUGFIX: Use /usr/bin/env to locate the correct Python interpreter.
2010-11-12 14:20:53 +01:00
Cas Cremers
9a04264d39
MPA: Improving test script with basic command-line options.
2010-11-12 14:12:23 +01:00
Cas Cremers
225a839dbc
Improving summary output.
2010-11-12 13:28:22 +01:00
Cas Cremers
573f581800
Updating test script to isolate --init-uniq cases as well.
2010-11-12 10:37:48 +01:00
Cas Cremers
270eef6a39
BUGFIX: Progressbar dummy should exist for MPA script.
2010-11-11 12:19:35 +01:00
Cas Cremers
266e5fb26b
BRUTUS: Added special build script.
...
Originates in newCompromise branch.
2010-11-11 12:14:49 +01:00
Cas Cremers
8ddd955415
MPA: Better test setup.
2010-11-11 12:08:53 +01:00
Cas Cremers
65074352c3
MPA: Improving the summaries given by the test script.
2010-11-11 11:16:59 +01:00
Cas Cremers
01eb5854cf
EFFICIENCY: If a new dependency overlaps with an old one, we don't have to recompute the closure.
2010-11-11 10:37:18 +01:00
Cas Cremers
6cd8007ab0
EFFICIENCY: New (default) heuristic.
...
Given that sk/pk/k are now hardcoded, we can exploit their occurrences with this
new heuristic.
The heuristic can now scan for the lowest term depth at which either sk or k occur.
This will cause the heuristic to favor looking for sk, then sk(x), and only later
other terms. In a small test this was twice as fast. For protocols based on pk only
the performance loss should be negligible.
The old heuristic was 162, now it is 162+512 = 674.
2010-11-11 10:37:18 +01:00
Cas Cremers
e42aa1215e
Scyther.py: Added Caching to Scyther's Python interface.
...
Cached data is stored in:
Cache/XX/YYYYY.out (stdout)
Cache/XX/YYYYY.err (stderr)
Where XX^YYYYY is the sha256 hexdigest of the concatenation of the input spdl and
the arguments.
2010-11-11 10:37:18 +01:00
Cas Cremers
cbb66ea794
Scyther.py: Improving Scyther python interface by giving options and filenames when reporting an error.
2010-11-11 10:37:18 +01:00
Cas Cremers
fac14fc950
Added a new subdirectory with protocols for MPA experiments.
2010-11-11 10:37:18 +01:00