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

Commit Graph

  • d7e49028c1 - Added pruning of functions the intruder does not know (e.g. SK) ccremers 2004-08-20 14:55:34 +00:00
  • 851044ecd0 - Improved the SK lemma, but it is NOT correct yet. ccremers 2004-08-20 11:47:00 +00:00
  • 72d52a6e12 - Key goals now have priority. This strategy yields complete proofs for e.g. bke, and reduces states for NSL. ccremers 2004-08-20 10:52:40 +00:00
  • baae7ef94a - The proofs now also show a list of open goals at each step. ccremers 2004-08-20 09:53:44 +00:00
  • bf2cbb5540 - Updated the todo list. ccremers 2004-08-20 09:26:34 +00:00
  • be44ed047a - Fixed some goal selection issues. - Added note about mirroring model checker semantics. ccremers 2004-08-20 09:21:39 +00:00
  • 7308791c83 - More todos. ccremers 2004-08-20 08:01:35 +00:00
  • bd84625ae4 - Fixed some more problems. Seems to be stable, although pruning is not sufficient. Investigate bke-broken. ccremers 2004-08-19 15:30:31 +00:00
  • f2bc78cc1f - Improved proof output. ccremers 2004-08-19 14:55:21 +00:00
  • 8fa7c4e839 - Fixed bug in printing. - Algorithm should work again. ccremers 2004-08-19 14:52:17 +00:00
  • f25f0abd4e - Fixed a memory error. ccremers 2004-08-19 14:49:03 +00:00
  • 35c55c9483 - Fixed a bug for NULL case in interm/subterm. - Fixed a bug where the mgu termlist was never deleted in interm/subterm. ccremers 2004-08-19 13:55:16 +00:00
  • 5c15c21832 - Reports on completeness of proofs. ccremers 2004-08-19 13:09:35 +00:00
  • 15580c6ec9 - Added subrun counters. ccremers 2004-08-19 12:47:53 +00:00
  • be2df84f91 - Much improvements to the proof output. ccremers 2004-08-19 12:35:51 +00:00
  • c993e17597 - Improving proof output. ccremers 2004-08-19 11:37:41 +00:00
  • 1180d3cf6f - Added --proof switch for Arachne engine, which outputs the (partial) proof of correctness. ccremers 2004-08-19 10:46:27 +00:00
  • d73351ace7 - Added a good idea for the output. ccremers 2004-08-18 21:44:30 +00:00
  • c929fa6ea3 - Debug info should be encapsulated. ccremers 2004-08-18 20:22:55 +00:00
  • 85ac32fbd1 - Claim counting now works. ccremers 2004-08-18 20:22:33 +00:00
  • b1259e4b03 - Updated todo list. ccremers 2004-08-18 20:13:13 +00:00
  • 046eb67e78 - Some stuff has been fixed, so can be removed from the todo list. ccremers 2004-08-18 19:46:25 +00:00
  • c95630f93b - Improved pruning. ccremers 2004-08-18 19:43:58 +00:00
  • 0f75efc787 - Fixed bug in interm relation. - Commented flag for normal version. ccremers 2004-08-18 18:41:49 +00:00
  • 8583b4ef5c BROKEN - Improved algorithm. ccremers 2004-08-18 18:22:59 +00:00
  • 341f519bbb BROKEN - Works better all the time. Huge shift of main logic. Much better. ccremers 2004-08-18 15:46:33 +00:00
  • b2d21f0a8a BROKEN - Working on new algorithm. Some memory error can occur. ccremers 2004-08-18 14:06:14 +00:00
  • c5695d6fe8 - Added more generic term iterators. ccremers 2004-08-18 12:12:29 +00:00
  • eb5a39522b - Compilation again. Now we have the sufficient components, and can start to reconnect. ccremers 2004-08-18 09:57:01 +00:00
  • b2838ed1e4 - Made a start with the new version. ccremers 2004-08-17 15:52:52 +00:00
  • bb78c71c90 - Introduced termInTerm (bigterm, smallterm) ccremers 2004-08-17 14:11:25 +00:00
  • a2cc46bb34 - Added test ns3 thing. ccremers 2004-08-17 11:30:58 +00:00
  • 8869477cf0 - Broken first attempt to work towards simplified method. ccremers 2004-08-17 11:30:03 +00:00
  • 5dd6127e4b - Added term to binding relation. ccremers 2004-08-17 11:03:18 +00:00
  • 9ec1bdc8eb - Merged with old version of warshall.c. Some minor improvements. ccremers 2004-08-17 09:48:29 +00:00
  • f384042bfe - Switched -r n behaviour for Arachne, effectively turning it into the upper bound on runs. ccremers 2004-08-16 14:49:41 +00:00
  • 536e5bf237 - Fixed some errors in length detection. - Added more bounds checking. ccremers 2004-08-16 13:18:04 +00:00
  • 05ee3f7f0a - Added a new warshall. Compare with previous version at home. - Rewrote the bind_to_*_run functions. ccremers 2004-08-16 09:50:37 +00:00
  • c518e68881 BROKEN - Added broken attempt to solve to problem, where a new instance has to be bound, but older variables point to role terms, e.g. RV#1->RV. What should happen, is that it becomes RV#1->RV#new. I thought of a solution, but it is still somewhat broken. Maybe I should ignore any mappings of variables such as RV, which might be included. ccremers 2004-08-15 19:58:26 +00:00
  • 91a679a129 - Made the output of the semistate include the bindings. ccremers 2004-08-15 17:50:41 +00:00
  • 071b9bd735 - Improved semistate printing. ccremers 2004-08-15 17:16:13 +00:00
  • 1f99b16ee8 - Much better implementation of M_0. ccremers 2004-08-15 17:07:38 +00:00
  • ca2eeb7235 - Implemented better matching. - Pruning for untrusted agent lists in the claim run as well. - Sloppy M_0 implementation; needs to be fixed. ccremers 2004-08-15 16:44:54 +00:00
  • c3d5123ab0 - Matching is now typed. ccremers 2004-08-15 16:08:53 +00:00
  • c7e290197c - Cycle detection seems to be working. ccremers 2004-08-15 14:57:50 +00:00
  • 28782548b0 - Implemented cycle detection. Untested. ccremers 2004-08-15 14:07:34 +00:00
  • ffe20fb168 - Integrated new binding relation. No closure as yet. ccremers 2004-08-15 12:24:27 +00:00
  • ef2586236c - Added bindings module. ccremers 2004-08-15 11:55:22 +00:00
  • 0fee6b5797 - Secrecy claims are now handled fairly okayish, as long as only one term is in the claim. This should be tupling-or, really, for convenience. ccremers 2004-08-14 19:19:23 +00:00
  • 18415c95a2 - Fixed bug in run forcing. ccremers 2004-08-14 18:38:43 +00:00
  • 68d3bab305 - Improved indenting. ccremers 2004-08-14 18:11:30 +00:00
  • b6598ea8f4 - Fixed a bug in subst reporting, when substitutions are compund terms. ccremers 2004-08-14 18:08:59 +00:00
  • 911e9e4e94 - Updated todo list. ccremers 2004-08-14 18:08:23 +00:00
  • bf75e93f4c - Substitutions from roles have to be reset to compare existing runs. ccremers 2004-08-14 16:26:57 +00:00
  • 1b3ef9e4ac - Improved debugging output by adhering to the level setup. ccremers 2004-08-14 16:12:32 +00:00
  • 53cb869426 - Claim iteration works nicely now. ccremers 2004-08-14 15:59:14 +00:00
  • 68b2aa16e7 - Improved semistate printing. ccremers 2004-08-14 14:38:30 +00:00
  • 74851e0393 - Consistency improvements. ccremers 2004-08-14 14:27:46 +00:00
  • f219461c8d - After some trouble, nonce binding is working nicely. ccremers 2004-08-14 14:23:21 +00:00
  • e3d16947ee - Output cleanup. ccremers 2004-08-14 13:17:37 +00:00
  • afda4f355e - Added much debug info, so we can see send iteration is going wrong. But why? ccremers 2004-08-13 20:56:51 +00:00
  • fe16785982 - Fixed error in error reporting :-\ - Added intruder construction nodes. - Several cleanups. ccremers 2004-08-13 20:09:12 +00:00
  • a3828a028f - Fixed the very annoying bug! The problem was in roleInstance for Arachne. When a subst was carried out by an Rolename->compoundTerm substitution, the compound term was not duplicated, and this caused problems at roledef destruction. ccremers 2004-08-13 14:35:22 +00:00
  • ff224fee8a - Some cleanup. - Added iteration limit, just enough to show the error. ccremers 2004-08-13 13:25:25 +00:00
  • eb55dbe35d - Fixed another '&' error. ccremers 2004-08-13 12:14:58 +00:00
  • 887b2f3a80 - Made indentDepth availabe in non-debug modes. ccremers 2004-08-13 11:11:59 +00:00
  • 43caf1707e - Stupid layout fix. ccremers 2004-08-13 10:52:20 +00:00
  • 54d857ca3c - Fixed a bug in mgu.c (& instead of &&) - scons shared=yes is now okay for Valgrind. ccremers 2004-08-13 10:50:56 +00:00
  • 758cb88c8c - Some POR optimizations in roleInstance were disabled for Arachne. ccremers 2004-08-13 10:28:20 +00:00
  • 70e5b98d37 - Added more intruder constructs. ccremers 2004-08-13 10:25:23 +00:00
  • 9153b06012 - Cleanup, improvements across the board. ccremers 2004-08-13 08:29:11 +00:00
  • 8fcdc9384e - Removed crappy debug effort. ccremers 2004-08-12 13:23:21 +00:00
  • b9f4d11d0a - Some cleanup writes, e.g. making initalisation code order correspond to struct field order. ccremers 2004-08-12 13:22:49 +00:00
  • 032d322952 - Fixed a bug with role destruction: the intruder goal term was not duplicated, but destroyed nevertheless. ccremers 2004-08-12 12:37:30 +00:00
  • 0862ce20da - Added more detailed debug output for Arachne. - Fixed a header problem for compiler.c. ccremers 2004-08-12 12:28:57 +00:00
  • 2005aa929e - Removed some obsolete commenting. ccremers 2004-08-12 12:03:20 +00:00
  • 7df10cf568 - Added role/protocol adding constructs for the intruder with Arachne. ccremers 2004-08-12 11:55:03 +00:00
  • 293c29b88e - Added generic indent for Arachne. - Some more error reporting. ccremers 2004-08-12 11:35:13 +00:00
  • 1791699c01 - Moved roledef_shift to role.c ccremers 2004-08-12 11:22:49 +00:00
  • fe960cfb6a - Added termlist iterator. - Fixed role instance resetting role var substitutions. ccremers 2004-08-12 09:28:50 +00:00
  • 0f470cf6a2 - Rewrote roleInstance to cope with Arachne needs. - Introduced some iterators for e.g. term leaves and roledefs. These are not used everywhere yet. ccremers 2004-08-12 09:14:31 +00:00
  • ac174b8130 - The work for the non-intruder Arachne part is now mostly done. ccremers 2004-08-11 21:04:52 +00:00
  • ec8b515218 - Added more important bits. ccremers 2004-08-11 15:05:13 +00:00
  • 2191d80885 - Lots of stuff starts to take shape. Nice. ccremers 2004-08-11 14:09:12 +00:00
  • f30207b059 - More logic. ccremers 2004-08-11 12:08:10 +00:00
  • b74567b2e0 - Added more outlining for the arachne system. ccremers 2004-08-11 11:22:20 +00:00
  • 9cf3bf3da3 - Setup main arachne infrastructure. ccremers 2004-08-11 09:51:17 +00:00
  • 0008b58739 - Fixed wrong comment. ccremers 2004-08-11 08:20:22 +00:00
  • 742a65bac1 - Added claim symmetry reduction; this doesn't help much for lower number of runs. It is on by default. ccremers 2004-08-11 08:17:49 +00:00
  • 1f96c9077a - Added bind_run and bind_index for goal bindings to the roledef stuff. ccremers 2004-08-10 15:17:00 +00:00
  • 7fbd43986f Preparations for Arachne. - roleInstanceDestroy is very much needed. - fixed bug in maxruns maintenance for incRuns. - Arachne does not use run knowledge. ccremers 2004-08-10 15:02:37 +00:00
  • 028c3a03f2 - Bugfix. ccremers 2004-08-10 11:26:14 +00:00
  • ca4c0c8869 - Added shift and length operations for generic lists. ccremers 2004-08-09 21:44:16 +00:00
  • 01d914314e - Promoted sys to the global system state. Convenient for arachne iterations. ccremers 2004-08-09 21:43:55 +00:00
  • 246c0c1c23 - Added termMguSubTerm and termMguInTerm ccremers 2004-08-09 21:22:24 +00:00
  • a096aac6dd - Added a note with inverseKey as for how to remove it. ccremers 2004-08-09 21:22:06 +00:00
  • acc29656c6 - Added generic list library. ccremers 2004-08-09 20:15:05 +00:00
  • 8f501b1620 - Improved status output. ccremers 2004-08-09 10:41:25 +00:00
  • 71c658051e - Reindented everything, so the layout is up to date again. ccremers 2004-08-09 10:05:58 +00:00
  • 4d1362cb1b - Implemented --check=Secret switch, which allows checking of specific properties. - Fixed a bug in the symbol table, where symbols were never inserted into the hash table. ccremers 2004-08-09 09:42:58 +00:00