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

Commit Graph

  • 0a15692124 - Oops. ccremers 2006-08-02 09:35:18 +00:00
  • b6d8930438 - More non-linux compatibility stuff. ccremers 2006-08-02 09:32:29 +00:00
  • 0c1684e1f2 - Windows-compatible (by disabling, duh..) ccremers 2006-08-02 09:27:09 +00:00
  • 203b652bab - Updated syntax for claim xml output. ccremers 2006-08-01 11:20:53 +00:00
  • 4b671384af - Some fixes to compile under Cygwin ccremers 2006-08-01 09:13:55 +00:00
  • 18d4b94b1e - Reverted to manual flex push/pup structure for include files. ccremers 2006-08-01 09:09:44 +00:00
  • 5e10206df1 - Added encapsulated dot output and claim reporting to the XML output. ccremers 2006-08-01 07:31:40 +00:00
  • 9a98e66671 - Claim status is now reported after each claim. ccremers 2006-08-01 06:10:12 +00:00
  • 92a98a85cc - Single claim check branched. ccremers 2006-08-01 06:04:01 +00:00
  • ff87bf180f - Claim reporting moved into claim.c ccremers 2006-08-01 05:58:02 +00:00
  • 80eafb7374 - Additional --check output should go to stderror. ccremers 2006-07-31 11:31:52 +00:00
  • cc358c5df3 - Misc fixes, some reporting with --check. ccremers 2006-07-31 11:30:08 +00:00
  • e902aaa260 - Added well-formedness checks. This will only be enabled if a role uses the 'knows' keyword. ccremers 2006-07-31 11:08:51 +00:00
  • ff21e9e572 - Added function shortcuts in M_0 derivation. ccremers 2006-07-27 14:19:19 +00:00
  • df1a56c780 - Iteration seems to work nicely, thank you. ccremers 2006-07-27 11:55:24 +00:00
  • 4e085f0eb8 - Initial knowledge displayed when running --check. ccremers 2006-07-27 10:45:26 +00:00
  • f00392ac3e - Added functional 'knows' keyword. ccremers 2006-07-27 10:44:12 +00:00
  • 12f2168c6c - Not quite ready, but a start. ccremers 2006-07-18 21:57:19 +00:00
  • 30b629909b - Added note on --chec- Added note on --checkk ccremers 2006-07-15 19:32:15 +00:00
  • f31b5bfe9c - Started rewrite of main algorithm, by removing dynamic addition of M_0 nodes, and simply restricting it to a single M_0 send node. ccremers 2006-07-09 15:08:42 +00:00
  • 7409a38d12 - Note regarding pruning. ccremers 2006-07-06 15:55:43 +00:00
  • dcb1625c3a - Changed my mind. --prune 0 : all attacks --prune 1 : select first attack --prune 2+: use heuristic (currently only 2 supported) ccremers 2006-07-06 15:54:14 +00:00
  • a8dee79504 - Added support for different attack heuristics. Disable with --prune=2. ccremers 2006-07-06 15:52:13 +00:00
  • 784304ed65 - Bugfix: separators between local constants were not printed correctly. ccremers 2006-07-02 23:44:18 +00:00
  • fc8b0de971 - Added special weights in dot output for M_0 originating terms. ccremers 2006-07-02 13:38:20 +00:00
  • 4ec62ddad9 - Fixed an empty balloon which might confuse people, in the dot output. ccremers 2006-07-02 13:10:46 +00:00
  • 0184b6277b - Better handling of function from M0 collapse in dot output. ccremers 2006-07-02 12:51:19 +00:00
  • aeac3d6616 - M_0 function application is now absorbed. ccremers 2006-07-02 12:03:57 +00:00
  • 639146c4f9 - Added heuristics results. ccremers 2006-07-01 12:12:42 +00:00
  • fc6923a7be - Added new results (typo fix). ccremers 2006-07-01 11:53:26 +00:00
  • 3b330d40de - Added preliminary results, which will be used in the thesis. - Modified heuristics test for stuff in the thesis. ccremers 2006-07-01 10:11:08 +00:00
  • b85d2e2270 - Added first attack analysis. ccremers 2006-07-01 09:48:06 +00:00
  • 7686ea4f64 - Added some further tests. ccremers 2006-07-01 09:34:37 +00:00
  • c52a340d8e - Improved heuristics. Default is now 162 (but 99 performs equally well) ccremers 2006-06-29 07:49:23 +00:00
  • d87d9ede30 - Fixed some comments. ccremers 2006-06-12 14:48:57 +00:00
  • 780ca9880f - Added feature to ensure include files come from the right place. The order in which Scyther searches for files is now. 1. From the prefix of the previously found file. 2. Current directory. 3. Anything in SPDLDIRS Here, 1 is new. - When using -E (--expert), scyther shows any files it reads on stderr. ccremers 2006-06-11 15:22:20 +00:00
  • 6ac5e2a428 - Added '--lightness' switch. ccremers 2006-05-26 12:57:27 +00:00
  • 07cc2c2b55 - Minor updates in output format. ccremers 2006-05-26 12:34:37 +00:00
  • 2e94dd065e - "--clusters" output is quite advanced, but still dot makes a bit of a mess out of it. One of the reasons is that the intruder events cannot be used along with the normal ranking, because they no longer correspond to real events. ccremers 2006-05-26 11:27:05 +00:00
  • e3b84a0f67 - New '--clusters' switch: needs some work. ccremers 2006-05-26 09:39:10 +00:00
  • 0679cbc3b8 - Added '--monochrome' switch, to be used in thesis output. There is a hardcoded lightness factor in dotout.c (MONOCHROMEFACTOR) ccremers 2006-05-25 20:35:01 +00:00
  • 6a74883adf - Restricted the syntax somewhat, to avoid people typing crap. (Cf. Golsteijn) ccremers 2006-05-16 15:00:21 +00:00
  • 6dff931dbc - Term identifiers can now contain primes (SM) - If labels start with a bang (!), they are ignored in synch/agree claims. ccremers 2006-04-25 13:58:14 +00:00
  • 54810cf4d3 - Updated numbers. ccremers 2006-04-13 12:48:37 +00:00
  • 974e5f7315 - Reset encryption level issue. ccremers 2006-04-13 12:43:13 +00:00
  • 08f705234b - Added `include "dinges";' command, that is aware of Scytherdirs. ccremers 2006-04-12 12:42:04 +00:00
  • db8e72f37e - Misc fixes to heuristic. ccremers 2006-04-03 08:21:52 +00:00
  • d2058d937b - Revised cost heuristic. Trace length is no longer the real optimization. ccremers 2006-04-02 12:29:02 +00:00
  • e1890ddc9f - Improved cost function: now also avoids using initiators when possible. ccremers 2006-04-02 12:07:25 +00:00
  • 52708d09b4 - MakeTraceConcrete now yields nicer choices, e.g. "Agent1" or "Nonce2". ccremers 2006-04-02 11:56:22 +00:00
  • 8c03bba02a - Fixed a bug in output overwrite for de-class code. ccremers 2006-03-31 12:24:32 +00:00
  • 4d7b744e1b - Discovered ugly bit in de-class code, which causes what seem to be errors with --extravert: even if Alice is already occurring in the system, the name can be used. - Added explicit level 2 encryption bound. This is technically incorrect, but for now it should work. ccremers 2006-03-31 10:12:58 +00:00
  • cb440700e3 - Added --unique responder/initiator switches, which are both implied by --extravert. ccremers 2006-03-31 08:24:41 +00:00
  • 5fe55d35cf - Code refactoring. ccremers 2006-03-28 14:45:02 +00:00
  • b224344b59 - Bugfixed --extravert. ccremers 2006-03-28 14:24:46 +00:00
  • dff7fcaee3 - Updated readme for beta2. ccremers 2006-03-27 20:31:19 +00:00
  • ac87af60c1 - More improvements. Current drawbacks: Intruder choice still not clear. ccremers 2006-03-20 09:54:45 +00:00
  • f3d4e8c350 - Some improvements to the intruder nodes. ccremers 2006-03-20 09:40:45 +00:00
  • 543e430e6c - In the light of recent discoveries on Athena method, I reinstated the --match switch. ccremers 2006-03-20 08:47:12 +00:00
  • 881eccd6be - Fixed --disable-intruder: it now also uses no tupling shortcuts. ccremers 2006-03-19 12:59:26 +00:00
  • a35a618a27 - Cleanup; make headers more compact. ccremers 2006-03-16 16:15:14 +00:00
  • 84d7841d91 - More work on testing. ccremers 2006-03-16 13:58:45 +00:00
  • f11f1fff0b - Bugfix for dot output. ccremers 2006-03-16 13:26:46 +00:00
  • 3241c0c828 - Better class printing for the headers. ccremers 2006-03-16 08:49:10 +00:00
  • 1ce03104c5 Major: - Added rho/sigma/constants fields to the runs, on which the new code is based. Over time, .locals should be deprecated in favour of these better variants. - Untyped variant is out of grace for the time being (cf. Athena interm problems) - Improved graph output further. ccremers 2006-03-15 21:30:19 +00:00
  • 5624f7e7b6 - Added some comments. ccremers 2006-03-15 08:56:23 +00:00
  • 25244c5b23 - Fixed bug in new tuple expansion code (again, caused by the intricate "realX" versus "isX" distinction.) - Added structures for rho, sigma, constants, but did not activate them yet. ccremers 2006-03-15 08:51:08 +00:00
  • 2b9246bb64 - Bug report: this should be fixed. ccremers 2006-03-15 08:33:09 +00:00
  • 16a59624fe - Revised dot output. - Reintroduced intruder events. - Added colors. ccremers 2006-03-14 11:37:28 +00:00
  • f823399a73 - Minor improvements. ccremers 2006-03-13 16:26:53 +00:00
  • f7ee9743d2 - Bugfix for self-initiator detection. Woops. ccremers 2006-03-13 14:19:01 +00:00
  • 74052cf226 - Code cleanup for intruder count. ccremers 2006-03-10 14:52:45 +00:00
  • af07f0cc3f - Removed obsolete stuff. ccremers 2006-03-10 14:51:05 +00:00
  • 895852de89 - Added iterators. - More space in encryption notation for better readability. ccremers 2006-03-10 14:48:40 +00:00
  • 2280187b32 - Improved dot class output. ccremers 2006-03-08 15:12:58 +00:00
  • 5487d3ae90 - From this version onwards, Scyther no longer supports the modelchecker method. A big cleanup has been started, but is not finished yet, so minor artefacts might still remain. These are to be cleaned up later. ccremers 2006-03-08 13:58:46 +00:00
  • 2830c8e8ff - Fixed some Doxygen documentation errors. ccremers 2006-03-08 12:38:39 +00:00
  • 1678577ce0 - Improved proof reports. - Minor (epsilon type) efficiency improvement. ccremers 2006-03-05 15:18:39 +00:00
  • c7605d03a3 - Added problem. ccremers 2006-03-01 08:36:09 +00:00
  • 527bf8baa5 - Better error reporting for local order constraints. ccremers 2006-02-28 15:33:12 +00:00
  • 4064d8ca65 - Improvements to the testing suite. ccremers 2006-02-28 15:06:21 +00:00
  • f3d94b8e0d - Removed old hack lemmas by clean ones. ccremers 2006-02-28 15:01:58 +00:00
  • 282c0d5094 - --experimental is now available in the normal version, but for experts only. ccremers 2006-02-28 14:06:12 +00:00
  • a4429d548f - Turned 'hidden' term lemma back on by default. ccremers 2006-02-28 13:57:38 +00:00
  • 00616e45ed - Bit masking was incorrect: & binds less strong than == ! This caused many of the --experimental switches not to work. ccremers 2006-02-28 13:41:36 +00:00
  • cf832ca1b1 - Seems to work again, but further testing is needed. ccremers 2006-02-27 22:27:09 +00:00
  • b49d13b6ee - [[[ Broken commit. ]]] Stuff seems to be working again, slightly less efficient though (count states). ccremers 2006-02-27 16:08:17 +00:00
  • bb16bd755e - Print states in a more countable format. ccremers 2006-02-27 15:20:37 +00:00
  • c22173e5ee - [[[ Broken commit ]]] More work on the arachne multiple-decryptor. Horrific. ccremers 2006-02-26 20:01:22 +00:00
  • 95df010a54 - [[[ Broken commit ]]] More intermediate work. ccremers 2006-02-26 17:18:59 +00:00
  • 0ce88af6ac - [[[ Broken commit ]]] Committing partial new Warshall work because it is getting too big. ccremers 2006-02-26 15:00:58 +00:00
  • 8995bc4d28 - Better reporting, better analysis. - End result now weighed according to undecided^2 * states, making the decidability a more important factor. ccremers 2006-02-24 12:50:04 +00:00
  • 1d3d154a2f - If the timebound is hit, it should be reported anyway, because the results are not to be trusted anymore. ccremers 2006-02-23 16:21:25 +00:00
  • bc61255a78 - Added timeout information. ccremers 2006-02-23 16:10:52 +00:00
  • 1aa77eec27 - Limit heuristics to sensible values. ccremers 2006-02-23 15:54:26 +00:00
  • b16023bf0e - Cleaned up heuristic code. Note that there is a "hidden" heuristic: implicitly, older goals are resolved first, if some goals have equal weights. This is encoded in the "w <=" comparison; if this is set to "w <", the heuristic becomes much less effective. ccremers 2006-02-23 15:03:43 +00:00
  • 10d44ad611 - Added cache clearing script. ccremers 2006-02-23 10:54:11 +00:00
  • 5d8bc6bb0e - Default is to only test protocols from SPORE. ccremers 2006-02-23 10:51:18 +00:00
  • 819b12b759 - Space instead of comma for testing. ccremers 2006-02-23 10:50:32 +00:00
  • c3a42e7df4 - Added protocol counter. ccremers 2006-02-23 10:49:53 +00:00