sylv/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Commit Graph

  • 19b3c74e65 - Remove obsolete child parameter. ccremers 2004-10-18 13:06:22 +00:00
  • 94b3ac7c96 - Added debug code for dot output. - Push/pop goals are counted now, making the child parameter obsolete. ccremers 2004-10-18 13:04:34 +00:00
  • 4b10c7f151 - Added priorities. ccremers 2004-10-16 22:03:33 +00:00
  • abad7044dd - Added thingy. ccremers 2004-10-15 19:53:04 +00:00
  • 7247335e5b - Much nicer naming for the files. ccremers 2004-10-15 14:46:23 +00:00
  • 622b28520e - error output is also stored now. ccremers 2004-10-15 12:11:13 +00:00
  • 0f68fcb8d6 - Added a generic test generator script. ccremers 2004-10-15 08:45:59 +00:00
  • 795f28006d - Added some thoughts. ccremers 2004-10-14 20:49:49 +00:00
  • 46ce2f37ee - Cut off tab at the end of a line for xargs ccremers 2004-10-14 20:17:01 +00:00
  • 19d7b42b14 - ...but don't forget to remove the debug output... ccremers 2004-10-14 20:11:19 +00:00
  • 02e1ccb186 - Tuple generator now works great. ccremers 2004-10-14 20:09:11 +00:00
  • dfe16fa306 - First skeleton for tuple printer. ccremers 2004-10-14 18:18:01 +00:00
  • d33ec486ce - Modified -l switch to also serve as proof depth limit. ccremers 2004-10-14 15:25:28 +00:00
  • ba832159b1 - Added a new prioritylevel for seemingly public keys, but the splice-as problem remains. ccremers 2004-10-14 15:09:48 +00:00
  • 29445bbd5f - Added two (SPORE) splice-AS variants. ccremers 2004-10-14 14:50:49 +00:00
  • 15ed7a99fa - Prevent stupid clashes. ccremers 2004-10-14 14:41:54 +00:00
  • 884db51a4b - Added (false) Nisynch, Niagree claims. - Shortened the names. ccremers 2004-10-14 14:41:27 +00:00
  • c717262e20 - Fixed the types. ccremers 2004-10-14 14:35:01 +00:00
  • 09ffaad340 - Fixed a claim role. ccremers 2004-10-14 14:34:47 +00:00
  • 9ac12f9198 - More serious problem found. ccremers 2004-10-14 14:33:22 +00:00
  • 123b12a1c0 - Problems with Splice/AS suggest heuristic improvements. ccremers 2004-10-14 14:30:27 +00:00
  • 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 +00:00
  • 87a75106d1 - Printing the protocol tab-separated from the role is more useful for script-based parsing. ccremers 2004-10-14 13:29:28 +00:00
  • 2bc1df6135 - Improved readability of printed claims. - Fixed comment. ccremers 2004-10-14 13:19:36 +00:00
  • 0efd39e028 - This script now only outputs summary to stdout. ccremers 2004-10-14 11:52:13 +00:00
  • c7b06fc0f1 - Added Nisynch claims. ccremers 2004-10-14 11:51:49 +00:00
  • 6eecef9806 - I can't remember why I needed this protocol, but here goes. ccremers 2004-10-13 13:29:38 +00:00
  • 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 +00:00
  • 46e46abb84 - Added andrew-ban and made the naming more consistent. ccremers 2004-10-13 12:25:01 +00:00
  • 0df4662a4a - Fixed claim labelling. ccremers 2004-10-13 12:24:34 +00:00
  • decf9f36c2 - Added test script. ccremers 2004-10-13 12:24:18 +00:00
  • 1387fd1d50 - Fixed claim labelling. ccremers 2004-10-13 12:23:55 +00:00
  • 0db90f4243 - Fixed some agent issue. ccremers 2004-10-13 12:23:35 +00:00
  • d7bcd18fb0 - Fixed a claim label. ccremers 2004-10-13 12:23:05 +00:00
  • 40584ba6bd - Noted some stuff about graph computations, so that I won't forget this. ccremers 2004-10-12 18:08:01 +00:00
  • 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 +00:00
  • d64badefdc - Found a problem with type flaw attacks. ccremers 2004-10-12 15:23:03 +00:00
  • 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 +00:00
  • ef34e0080e - Counterexample for Bart's logic. ccremers 2004-10-06 09:10:04 +00:00
  • 3b4b367a4a - Minor correction. Probably redundant for a good compiler ;) ccremers 2004-09-20 17:41:53 +00:00
  • 02e99761ae - Split roleInstance into two more managable parts. ccremers 2004-09-20 12:40:01 +00:00
  • 500710519e - Added protocols for Bertinoro VODCA talk. ccremers 2004-09-10 07:46:00 +00:00
  • 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 +00:00
  • be366afa0e - A good reduction idea for secrecy added to the todo list. ccremers 2004-09-07 09:56:06 +00:00
  • c293c3bac8 - Added a new counter ref version. ccremers 2004-09-02 13:50:45 +00:00
  • 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 +00:00
  • 8570465e48 - More todo. ccremers 2004-09-01 19:11:06 +00:00
  • 78e68f3c17 - Added claim label. ccremers 2004-08-31 14:35:47 +00:00
  • 5ed9fefa7e - Improved these scenarios. ccremers 2004-08-31 14:32:31 +00:00
  • 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 +00:00
  • 0e9b7dcf11 - Some added error/bounds detection all around. ccremers 2004-08-31 12:35:05 +00:00
  • a673ea4ad1 - Write down, so that we don't forget. ccremers 2004-08-31 08:58:50 +00:00
  • 3687bff185 - Fixed kaochow - Niek Palm version. ccremers 2004-08-30 22:12:18 +00:00
  • f5ab30995c - Removed the debugging output. ccremers 2004-08-30 22:09:44 +00:00
  • 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 +00:00
  • b04bc86185 - Some minor cleanups. ccremers 2004-08-30 21:49:51 +00:00
  • 4832e9116c - Added pruning theorem for untrusted actors. ccremers 2004-08-30 21:07:45 +00:00
  • 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 +00:00
  • 8f441ac913 - Fixed some minor issues. - Fixed type flaw in labellist type. ccremers 2004-08-30 20:08:11 +00:00
  • 20a38f79c5 BROKEN - Protocol is not done yet. ccremers 2004-08-30 14:40:12 +00:00
  • 44f394d098 - Improvement. ccremers 2004-08-30 14:39:52 +00:00
  • f5548b82cc - Added protocol. ccremers 2004-08-30 14:30:17 +00:00
  • 4b3de5f9fb - Added BAN modified version of andrew-ban. ccremers 2004-08-30 14:17:11 +00:00
  • 02041cfbab - Fixed binding displays. - Improved attack dot output. - goal_graph_create now takes originator assumption into account. ccremers 2004-08-30 13:57:16 +00:00
  • 1d431dc6f1 - Attack output is a bit broken now for Arachne. Fix. ccremers 2004-08-30 06:07:17 +00:00
  • ee5ddea4d0 - Added a new test. - Fixed some notations. ccremers 2004-08-30 06:06:37 +00:00
  • 5035a35d51 - Bug spotted. ccremers 2004-08-28 17:28:14 +00:00
  • 25fa261e30 - Added some comments. ccremers 2004-08-28 14:05:38 +00:00
  • c907c1f657 - Added prefixed start nodes to indicate agent initiative in dot output. ccremers 2004-08-28 14:00:48 +00:00
  • 08f2155527 - Denoting 'empty term' with '*' from now on, yields more compact output. ccremers 2004-08-28 14:00:22 +00:00
  • 391c939b83 - New algorithm to draw bindings between runs. Much cleaner. ccremers 2004-08-28 13:47:37 +00:00
  • b349b6cef2 - More improvements to the dot output. ccremers 2004-08-28 12:42:11 +00:00
  • 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 +00:00
  • 2ddd1eee13 - Improved dot output for Arachne attacks. ccremers 2004-08-28 11:43:06 +00:00
  • 9d64b837db - Improved roledef printing for NULL, NULL roles (intruder) - Added graph output in dot format. ccremers 2004-08-28 09:24:30 +00:00
  • 6c2730af1a - Added some todo stuff. ccremers 2004-08-27 19:29:41 +00:00
  • 4420e06e4e - Ignore choose actions when determining Arachne trace length. ccremers 2004-08-27 19:15:24 +00:00
  • 939ece7500 - Improvements in the scenarios. ccremers 2004-08-27 19:08:31 +00:00
  • 4f534410bd - Implemented ordering checks. Need some test to validate this though. ccremers 2004-08-27 19:06:15 +00:00
  • 957b920b98 - Added extra Arachne check for -r0. ccremers 2004-08-27 18:26:19 +00:00
  • 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 +00:00
  • 198afa135e - Implemented attack length scanner per claim. Not stored yet. ccremers 2004-08-27 18:09:09 +00:00
  • 6ccb09297a - Better prune adherence. ccremers 2004-08-27 17:37:43 +00:00
  • 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 +00:00
  • 21b2c27320 - Niagree claim seems to be working fine now. ccremers 2004-08-27 17:25:38 +00:00
  • 2decf44bd2 - Checks are now in. Untested though. ccremers 2004-08-27 15:02:33 +00:00
  • 68bbdc2794 - Added interfaces for the more interesting Arachne claim checks. ccremers 2004-08-27 14:48:58 +00:00
  • fd3769d683 - Agreement test for Archne implemented (untested). ccremers 2004-08-27 14:41:06 +00:00
  • 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 +00:00
  • dfeaf83327 - Added 'termlistFind' function, which is more generic than inTermlist ccremers 2004-08-27 13:10:46 +00:00
  • d8e0e93bcf - Fixed a condition check in termlistAddNew. - Roles are now computed from prec for each claim. ccremers 2004-08-27 12:36:23 +00:00
  • 542044e36f - Added preliminary labellist support to the system. ccremers 2004-08-27 11:52:43 +00:00
  • 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 +00:00
  • 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 +00:00
  • 959c8d2c8b - Added termlist_to_tuple function. ccremers 2004-08-26 12:36:01 +00:00
  • 6c38253559 - Turned the exit codes into enum types, making it more generic. ccremers 2004-08-24 13:09:39 +00:00
  • 7d0be35658 - Bugfix: term output now correctly displays local constants of a run before it is bound. ccremers 2004-08-23 13:46:48 +00:00
  • dfdea5b0bf - Finished the protocol. ccremers 2004-08-23 11:59:42 +00:00
  • 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 +00:00
  • 98bff1e5e2 - Solved the TERM_Hidden issue for the keys in termMguSubTerm. Yields cleaner behaviour for MguSubterm. ccremers 2004-08-20 15:09:49 +00:00