dbb35a3ec9- Added the splice-AS protocol. The modelchecker finds an attack, but the arachne methods causes some problems.
ccremers
2004-10-14 14:22:59 +0000
87a75106d1- Printing the protocol tab-separated from the role is more useful for script-based parsing.
ccremers
2004-10-14 13:29:28 +0000
6eecef9806- I can't remember why I needed this protocol, but here goes.
ccremers
2004-10-13 13:29:38 +0000
1effb2ca99- Added original Kao-Chow protocol. There is something strange with the Arachne method though, that needs investigating.
ccremers
2004-10-13 12:55:23 +0000
46e46abb84- Added andrew-ban and made the naming more consistent.
ccremers
2004-10-13 12:25:01 +0000
0db90f4243- Fixed some agent issue.
ccremers
2004-10-13 12:23:35 +0000
d7bcd18fb0- Fixed a claim label.
ccremers
2004-10-13 12:23:05 +0000
40584ba6bd- Noted some stuff about graph computations, so that I won't forget this.
ccremers
2004-10-12 18:08:01 +0000
487212a9f9- The TMN protocol was wrongly reporting an error in the protocol. This turned out to be caused by an over-protective first-read detection.
ccremers
2004-10-12 16:58:29 +0000
d64badefdc- Found a problem with type flaw attacks.
ccremers
2004-10-12 15:23:03 +0000
0de3320009- Fixed a memory leak in termLocal. This did not cause any problems for the modelchecker, as it calls it only once, but it caused major problems for the arachne engine, which creates and destroys semiruns all the time.
ccremers
2004-10-12 15:12:20 +0000
ef34e0080e- Counterexample for Bart's logic.
ccremers
2004-10-06 09:10:04 +0000
3b4b367a4a- Minor correction. Probably redundant for a good compiler ;)
ccremers
2004-09-20 17:41:53 +0000
02e99761ae- Split roleInstance into two more managable parts.
ccremers
2004-09-20 12:40:01 +0000
f771d3ef4c- Testing to see what the gains are of using one regular agent. Turns out to be half of the states, thus twice as fast.
ccremers
2004-09-07 10:20:20 +0000
be366afa0e- A good reduction idea for secrecy added to the todo list.
ccremers
2004-09-07 09:56:06 +0000
c293c3bac8- Added a new counter ref version.
ccremers
2004-09-02 13:50:45 +0000
947fe654f1- Testing with this protocol didn't yet reveal the desired behaviour, as Arachne -m2 strategies aren't working fully yet.
ccremers
2004-09-01 20:24:39 +0000
8570465e48- More todo.
ccremers
2004-09-01 19:11:06 +0000
5ed9fefa7e- Improved these scenarios.
ccremers
2004-08-31 14:32:31 +0000
8b48aade68- Huge effort to make match type 2 (typeflaw generic) matching work. Problem with goals that turn into tuples, will have to be solved.
ccremers
2004-08-31 14:31:06 +0000
0e9b7dcf11- Some added error/bounds detection all around.
ccremers
2004-08-31 12:35:05 +0000
a673ea4ad1- Write down, so that we don't forget.
ccremers
2004-08-31 08:58:50 +0000
f5ab30995c- Removed the debugging output.
ccremers
2004-08-30 22:09:44 +0000
5c90522c55- Fixed a bug in the pruning algorithm, where intruder runs were also checked for agent lists, which is false.
ccremers
2004-08-30 22:08:44 +0000
b04bc86185- Some minor cleanups.
ccremers
2004-08-30 21:49:51 +0000
d43e3d432f- Ignoring singular variables seems to be a smart choice, although it implies that the intruder can generate any type. That is not conform the usual semantics. So we either change the usual semantics (wise) or we make this choice optional.
ccremers
2004-08-30 20:48:11 +0000
8f441ac913- Fixed some minor issues. - Fixed type flaw in labellist type.
ccremers
2004-08-30 20:08:11 +0000
20a38f79c5BROKEN - Protocol is not done yet.
ccremers
2004-08-30 14:40:12 +0000
25fa261e30- Added some comments.
ccremers
2004-08-28 14:05:38 +0000
c907c1f657- Added prefixed start nodes to indicate agent initiative in dot output.
ccremers
2004-08-28 14:00:48 +0000
08f2155527- Denoting 'empty term' with '*' from now on, yields more compact output.
ccremers
2004-08-28 14:00:22 +0000
391c939b83- New algorithm to draw bindings between runs. Much cleaner.
ccremers
2004-08-28 13:47:37 +0000
b349b6cef2- More improvements to the dot output.
ccremers
2004-08-28 12:42:11 +0000
acb89922f1- Singular variables need to be bound as well (to ensure ordering is correct w.r.t. e.g. nonces, if the intruder cannot construct them.)
ccremers
2004-08-28 12:20:50 +0000
939ece7500- Improvements in the scenarios.
ccremers
2004-08-27 19:08:31 +0000
4f534410bd- Implemented ordering checks. Need some test to validate this though.
ccremers
2004-08-27 19:06:15 +0000
957b920b98- Added extra Arachne check for -r0.
ccremers
2004-08-27 18:26:19 +0000
17ad6de97b- Semistate printing now reports trace length. - Pruning was wrong, so the shortest attack wasn't always found. Now it is.
ccremers
2004-08-27 18:18:16 +0000
198afa135e- Implemented attack length scanner per claim. Not stored yet.
ccremers
2004-08-27 18:09:09 +0000
f90f16fe93- Arachne engine now respects --prune=2 (and thus the default setting) somewhat. There is no good definition of length yet, so we don't do this yet.
ccremers
2004-08-27 17:35:23 +0000
21b2c27320- Niagree claim seems to be working fine now.
ccremers
2004-08-27 17:25:38 +0000
2decf44bd2- Checks are now in. Untested though.
ccremers
2004-08-27 15:02:33 +0000
68bbdc2794- Added interfaces for the more interesting Arachne claim checks.
ccremers
2004-08-27 14:48:58 +0000
fd3769d683- Agreement test for Archne implemented (untested).
ccremers
2004-08-27 14:41:06 +0000
4009ca86ed- Added some sanity checks for read/send/claim role parameters. - The cl->roles are now distance-ordered. This, the first role is at distance 0, etc. This is useful for checking e.g. synchronisation.
ccremers
2004-08-27 13:40:46 +0000
dfeaf83327- Added 'termlistFind' function, which is more generic than inTermlist
ccremers
2004-08-27 13:10:46 +0000
d8e0e93bcf- Fixed a condition check in termlistAddNew. - Roles are now computed from prec for each claim.
ccremers
2004-08-27 12:36:23 +0000
542044e36f- Added preliminary labellist support to the system.
ccremers
2004-08-27 11:52:43 +0000
275743c1a3- Fixed a bug where labels where not generated nicely if the symbols already had been declared in another role.
ccremers
2004-08-27 10:24:19 +0000
d58fc5ab43- Made the label naming unique, by adding tuple info with the protocol name. Now, we can simply test multiple protocol names by concatenation. - Removed the pointer equality leaf hypothesis, as it didn't hold anymore.
ccremers
2004-08-27 10:08:03 +0000
6c38253559- Turned the exit codes into enum types, making it more generic.
ccremers
2004-08-24 13:09:39 +0000
7d0be35658- Bugfix: term output now correctly displays local constants of a run before it is bound.
ccremers
2004-08-23 13:46:48 +0000
dfdea5b0bf- Finished the protocol.
ccremers
2004-08-23 11:59:42 +0000
0fc008fe33- Added keylevels to symbols. This is to help pruning the proofs, for terms and patterns that do not originate on regular nodes.
ccremers
2004-08-20 19:16:56 +0000
98bff1e5e2- Solved the TERM_Hidden issue for the keys in termMguSubTerm. Yields cleaner behaviour for MguSubterm.
ccremers
2004-08-20 15:09:49 +0000
ccremers