andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
546 Commits 1 Branch 0 Tags 21 MiB
46974091dc
Commit Graph

388 Commits

Author SHA1 Message Date
ccremers
fd3769d683 - Agreement test for Archne implemented (untested). 2004-08-27 14:41:06 +00:00
ccremers
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.
 2004-08-27 13:40:46 +00:00
ccremers
dfeaf83327 - Added 'termlistFind' function, which is more generic than inTermlist 2004-08-27 13:10:46 +00:00
ccremers
d8e0e93bcf - Fixed a condition check in termlistAddNew. 
- Roles are now computed from prec for each claim.
 2004-08-27 12:36:23 +00:00
ccremers
542044e36f - Added preliminary labellist support to the system. 2004-08-27 11:52:43 +00:00
ccremers
275743c1a3 - Fixed a bug where labels where not generated nicely if the symbols 
already had been declared in another role.
 2004-08-27 10:24:19 +00:00
ccremers
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.
 2004-08-27 10:08:03 +00:00
ccremers
959c8d2c8b - Added termlist_to_tuple function. 2004-08-26 12:36:01 +00:00
ccremers
6c38253559 - Turned the exit codes into enum types, making it more generic. 2004-08-24 13:09:39 +00:00
ccremers
7d0be35658 - Bugfix: term output now correctly displays local constants of a run 
before it is bound.
 2004-08-23 13:46:48 +00:00
ccremers
0fc008fe33 - Added keylevels to symbols. This is to help pruning the proofs, for 
terms and patterns that do not originate on regular nodes.
 2004-08-20 19:16:56 +00:00
ccremers
98bff1e5e2 - Solved the TERM_Hidden issue for the keys in termMguSubTerm. Yields 
cleaner behaviour for MguSubterm.
 2004-08-20 15:09:49 +00:00
ccremers
d7e49028c1 - Added pruning of functions the intruder does not know (e.g. SK) 2004-08-20 14:55:34 +00:00
ccremers
851044ecd0 - Improved the SK lemma, but it is NOT correct yet. 2004-08-20 11:47:00 +00:00
ccremers
72d52a6e12 - Key goals now have priority. This strategy yields complete proofs for 
e.g. bke, and reduces states for NSL.
 2004-08-20 10:52:40 +00:00
ccremers
baae7ef94a - The proofs now also show a list of open goals at each step. 2004-08-20 09:53:44 +00:00
ccremers
bf2cbb5540 - Updated the todo list. 2004-08-20 09:26:34 +00:00
ccremers
be44ed047a - Fixed some goal selection issues. 
- Added note about mirroring model checker semantics.
 2004-08-20 09:21:39 +00:00
ccremers
7308791c83 - More todos. 2004-08-20 08:01:35 +00:00
ccremers
bd84625ae4 - Fixed some more problems. Seems to be stable, although pruning is not 
sufficient. Investigate bke-broken.
 2004-08-19 15:30:31 +00:00
ccremers
f2bc78cc1f - Improved proof output. 2004-08-19 14:55:21 +00:00
ccremers
8fa7c4e839 - Fixed bug in printing. 
- Algorithm should work again.
 2004-08-19 14:52:17 +00:00
ccremers
f25f0abd4e - Fixed a memory error. 2004-08-19 14:49:03 +00:00
ccremers
35c55c9483 - Fixed a bug for NULL case in interm/subterm. 
- Fixed a bug where the mgu termlist was never deleted in
  interm/subterm.
 2004-08-19 13:55:16 +00:00
ccremers
5c15c21832 - Reports on completeness of proofs. 2004-08-19 13:09:35 +00:00
ccremers
15580c6ec9 - Added subrun counters. 2004-08-19 12:47:53 +00:00
ccremers
be2df84f91 - Much improvements to the proof output. 2004-08-19 12:35:51 +00:00
ccremers
c993e17597 - Improving proof output. 2004-08-19 11:37:41 +00:00
ccremers
1180d3cf6f - Added --proof switch for Arachne engine, which outputs the (partial) 
proof of correctness.
 2004-08-19 10:46:27 +00:00
ccremers
d73351ace7 - Added a good idea for the output. 2004-08-18 21:44:30 +00:00
ccremers
c929fa6ea3 - Debug info should be encapsulated. 2004-08-18 20:22:55 +00:00
ccremers
85ac32fbd1 - Claim counting now works. 2004-08-18 20:22:33 +00:00
ccremers
b1259e4b03 - Updated todo list. 2004-08-18 20:13:13 +00:00
ccremers
046eb67e78 - Some stuff has been fixed, so can be removed from the todo list. 2004-08-18 19:46:25 +00:00
ccremers
c95630f93b - Improved pruning. 2004-08-18 19:43:58 +00:00
ccremers
0f75efc787 - Fixed bug in interm relation. 
- Commented flag for normal version.
 2004-08-18 18:41:49 +00:00
ccremers
8583b4ef5c BROKEN 
- Improved algorithm.
 2004-08-18 18:22:59 +00:00
ccremers
341f519bbb BROKEN 
- Works better all the time. Huge shift of main logic. Much better.
 2004-08-18 15:46:33 +00:00
ccremers
b2d21f0a8a BROKEN 
- Working on new algorithm. Some memory error can occur.
 2004-08-18 14:06:14 +00:00
ccremers
c5695d6fe8 - Added more generic term iterators. 2004-08-18 12:12:29 +00:00
ccremers
eb5a39522b - Compilation again. Now we have the sufficient components, and can 
start to reconnect.
 2004-08-18 09:57:01 +00:00
ccremers
b2838ed1e4 - Made a start with the new version. 2004-08-17 15:52:52 +00:00
ccremers
bb78c71c90 - Introduced termInTerm (bigterm, smallterm) 2004-08-17 14:11:25 +00:00
ccremers
a2cc46bb34 - Added test ns3 thing. 2004-08-17 11:30:58 +00:00
ccremers
8869477cf0 - Broken first attempt to work towards simplified method. 2004-08-17 11:30:03 +00:00
ccremers
5dd6127e4b - Added term to binding relation. 2004-08-17 11:03:18 +00:00
ccremers
9ec1bdc8eb - Merged with old version of warshall.c. Some minor improvements. 2004-08-17 09:48:29 +00:00
ccremers
f384042bfe - Switched -r n behaviour for Arachne, effectively turning it into the 
upper bound on runs.
 2004-08-16 14:49:41 +00:00
ccremers
536e5bf237 - Fixed some errors in length detection. 
- Added more bounds checking.
 2004-08-16 13:18:04 +00:00
ccremers
05ee3f7f0a - Added a new warshall. Compare with previous version at home. 
- Rewrote the bind_to_*_run functions.
 2004-08-16 09:50:37 +00:00
ccremers
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.
 2004-08-15 19:58:26 +00:00
ccremers
91a679a129 - Made the output of the semistate include the bindings. 2004-08-15 17:50:41 +00:00
ccremers
071b9bd735 - Improved semistate printing. 2004-08-15 17:16:13 +00:00
ccremers
1f99b16ee8 - Much better implementation of M_0. 2004-08-15 17:07:38 +00:00
ccremers
ca2eeb7235 - Implemented better matching. 
- Pruning for untrusted agent lists in the claim run as well.
- Sloppy M_0 implementation; needs to be fixed.
 2004-08-15 16:44:54 +00:00
ccremers
c3d5123ab0 - Matching is now typed. 2004-08-15 16:08:53 +00:00
ccremers
c7e290197c - Cycle detection seems to be working. 2004-08-15 14:57:50 +00:00
ccremers
28782548b0 - Implemented cycle detection. Untested. 2004-08-15 14:07:34 +00:00
ccremers
ffe20fb168 - Integrated new binding relation. No closure as yet. 2004-08-15 12:24:27 +00:00
ccremers
ef2586236c - Added bindings module. 2004-08-15 11:55:22 +00:00
ccremers
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.
 2004-08-14 19:19:23 +00:00
ccremers
18415c95a2 - Fixed bug in run forcing. 2004-08-14 18:38:43 +00:00
ccremers
68d3bab305 - Improved indenting. 2004-08-14 18:11:30 +00:00
ccremers
b6598ea8f4 - Fixed a bug in subst reporting, when substitutions are compund terms. 2004-08-14 18:08:59 +00:00
ccremers
911e9e4e94 - Updated todo list. 2004-08-14 18:08:23 +00:00
ccremers
bf75e93f4c - Substitutions from roles have to be reset to compare existing runs. 2004-08-14 16:26:57 +00:00
ccremers
1b3ef9e4ac - Improved debugging output by adhering to the level setup. 2004-08-14 16:12:32 +00:00
ccremers
53cb869426 - Claim iteration works nicely now. 2004-08-14 15:59:14 +00:00
ccremers
68b2aa16e7 - Improved semistate printing. 2004-08-14 14:38:30 +00:00
ccremers
74851e0393 - Consistency improvements. 2004-08-14 14:27:46 +00:00
ccremers
f219461c8d - After some trouble, nonce binding is working nicely. 2004-08-14 14:23:21 +00:00
ccremers
e3d16947ee - Output cleanup. 2004-08-14 13:17:37 +00:00
ccremers
afda4f355e - Added much debug info, so we can see send iteration is going wrong. 
But why?
 2004-08-13 20:56:51 +00:00
ccremers
fe16785982 - Fixed error in error reporting :-\ 
- Added intruder construction nodes.
- Several cleanups.
 2004-08-13 20:09:12 +00:00
ccremers
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.
 2004-08-13 14:35:22 +00:00
ccremers
ff224fee8a - Some cleanup. 
- Added iteration limit, just enough to show the error.
 2004-08-13 13:25:25 +00:00
ccremers
eb55dbe35d - Fixed another '&' error. 2004-08-13 12:14:58 +00:00
ccremers
887b2f3a80 - Made indentDepth availabe in non-debug modes. 2004-08-13 11:11:59 +00:00
ccremers
43caf1707e - Stupid layout fix. 2004-08-13 10:52:20 +00:00
ccremers
54d857ca3c - Fixed a bug in mgu.c (& instead of &&) 
- scons shared=yes is now okay for Valgrind.
 2004-08-13 10:50:56 +00:00
ccremers
758cb88c8c - Some POR optimizations in roleInstance were disabled for Arachne. 2004-08-13 10:28:20 +00:00
ccremers
70e5b98d37 - Added more intruder constructs. 2004-08-13 10:25:23 +00:00
ccremers
9153b06012 - Cleanup, improvements across the board. 2004-08-13 08:29:11 +00:00
ccremers
8fcdc9384e - Removed crappy debug effort. 2004-08-12 13:23:21 +00:00
ccremers
b9f4d11d0a - Some cleanup writes, e.g. making initalisation code order correspond 
to struct field order.
 2004-08-12 13:22:49 +00:00
ccremers
032d322952 - Fixed a bug with role destruction: the intruder goal term was not 
duplicated, but destroyed nevertheless.
 2004-08-12 12:37:30 +00:00
ccremers
0862ce20da - Added more detailed debug output for Arachne. 
- Fixed a header problem for compiler.c.
 2004-08-12 12:28:57 +00:00
ccremers
2005aa929e - Removed some obsolete commenting. 2004-08-12 12:03:20 +00:00
ccremers
7df10cf568 - Added role/protocol adding constructs for the intruder with Arachne. 2004-08-12 11:55:03 +00:00
ccremers
293c29b88e - Added generic indent for Arachne. 
- Some more error reporting.
 2004-08-12 11:35:13 +00:00
ccremers
1791699c01 - Moved roledef_shift to role.c 2004-08-12 11:22:49 +00:00
ccremers
fe960cfb6a - Added termlist iterator. 
- Fixed role instance resetting role var substitutions.
 2004-08-12 09:28:50 +00:00
ccremers
0f470cf6a2 - Rewrote roleInstance to cope with Arachne needs. 
- Introduced some iterators for e.g. term leaves and roledefs. These are
  not used everywhere yet.
 2004-08-12 09:14:31 +00:00
ccremers
ac174b8130 - The work for the non-intruder Arachne part is now mostly done. 2004-08-11 21:04:52 +00:00
ccremers
ec8b515218 - Added more important bits. 2004-08-11 15:05:13 +00:00
ccremers
2191d80885 - Lots of stuff starts to take shape. Nice. 2004-08-11 14:09:12 +00:00
ccremers
f30207b059 - More logic. 2004-08-11 12:08:10 +00:00
ccremers
b74567b2e0 - Added more outlining for the arachne system. 2004-08-11 11:22:20 +00:00
ccremers
9cf3bf3da3 - Setup main arachne infrastructure. 2004-08-11 09:51:17 +00:00
ccremers
0008b58739 - Fixed wrong comment. 2004-08-11 08:20:22 +00:00
ccremers
742a65bac1 - Added claim symmetry reduction; this doesn't help much for lower 
number of runs. It is on by default.
 2004-08-11 08:17:49 +00:00
ccremers
1f96c9077a - Added bind_run and bind_index for goal bindings to the roledef stuff. 2004-08-10 15:17:00 +00:00
ccremers
7fbd43986f Preparations for Arachne. 
- roleInstanceDestroy is very much needed.
- fixed bug in maxruns maintenance for incRuns.
- Arachne does not use run knowledge.
 2004-08-10 15:02:37 +00:00
ccremers
028c3a03f2 - Bugfix. 2004-08-10 11:26:14 +00:00
ccremers
ca4c0c8869 - Added shift and length operations for generic lists. 2004-08-09 21:44:16 +00:00
ccremers
01d914314e - Promoted sys to the global system state. Convenient for arachne 
iterations.
 2004-08-09 21:43:55 +00:00
ccremers
246c0c1c23 - Added termMguSubTerm and termMguInTerm 2004-08-09 21:22:24 +00:00
ccremers
a096aac6dd - Added a note with inverseKey as for how to remove it. 2004-08-09 21:22:06 +00:00
ccremers
acc29656c6 - Added generic list library. 2004-08-09 20:15:05 +00:00
ccremers
8f501b1620 - Improved status output. 2004-08-09 10:41:25 +00:00
ccremers
71c658051e - Reindented everything, so the layout is up to date again. 2004-08-09 10:05:58 +00:00
ccremers
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.
 2004-08-09 09:42:58 +00:00
ccremers
4d154e8126 - Added knowledgePrintShort for knowledge displays without newlines. 2004-08-06 11:59:27 +00:00
ccremers
cd0dce31f3 - Minor cleanup. 2004-07-30 12:11:05 +00:00
ccremers
15fcbf8090 - Added scen_st to the output, which lists the number of states in the 
specific scenario.
 2004-07-30 12:04:38 +00:00
ccremers
d75e3af55c - Added the trace prefix cutter. Goody. 2004-07-29 14:47:46 +00:00
ccremers
331569c9a8 - Added '--echo' to stdout the commandline. Useful for reporting. 2004-07-29 13:15:29 +00:00
ccremers
c88c1d4461 - Removed --claims flag again. 
- Now new reporting on stderr, with claim details.
- Added '--summary' to redirect this report to stdout.
 2004-07-29 13:08:27 +00:00
ccremers
17c6fe5136 - Fixed some more printf usages, that should now be handled by eprintf. 2004-07-29 12:47:57 +00:00
ccremers
523b0ffd32 - Added --claims flag for some detailed output on claim violations. 2004-07-29 12:36:24 +00:00
ccremers
d2a639b314 - More informative claim displays. 2004-07-29 12:04:53 +00:00
ccremers
d181365e3e - Removed some old-fashioned defines, replacing them with enum constants. 2004-07-29 11:26:59 +00:00
ccremers
b22667a791 - Fixed termlist printing. 2004-07-29 11:15:07 +00:00
ccremers
75ecbf4346 - Reordered some switches. 
- Inverted progress bar behaviour: default is off. Enable with -b.
 2004-07-29 11:02:07 +00:00
ccremers
dda2907492 - Implemented output method selector, sys->output. 
- Changed disable-report switch into --empty.
- --scenario=-1 now displays a list of scenarios. Use wc -l to count
  them.
 2004-07-29 10:13:13 +00:00
ccremers
d5db3ca0e2 - Current Elegast scripts are not suitable for -t9 because scenario 
counting through the exit code is too limited. Fix.
 2004-07-28 23:47:22 +00:00
ccremers
a86e44dac6 Modifications for Elegast cluster. 2004-07-28 13:40:09 +00:00
ccremers
7aaed2dc90 - Added a reporting script, intended for parallel computations. 2004-07-28 12:40:16 +00:00
ccremers
d62a8d89e1 - Of course, errors have a higher priority. 2004-07-28 12:23:42 +00:00
ccremers
42e5efedac - When counting scenarios, the exit code reflects the number of 
scenarios.
 2004-07-28 12:22:40 +00:00
ccremers
1ba63d16d4 - Scyther now reports a 1 exit code (error) when a scenario number is 
selected that is too large.
 2004-07-28 12:03:42 +00:00
ccremers
472de3b526 - Added switch --choose-first. 
- Added switch --scenario (-s), to enable scenario exploration only.
  Use --scenario=-1 to count the number of possible scenarios.
 2004-07-28 11:39:08 +00:00
ccremers
289f71846b - Improved graph output for printing purposes. 2004-07-26 12:43:19 +00:00
ccremers
0ffa7b81ec - Fixed a bug with --pp=100. 2004-07-26 08:32:01 +00:00
ccremers
38a3fdb320 - Moved doxyconfig to the refman directory, which makes much more sense. 
However, it still needs an SConstruct script.
 2004-07-25 20:39:49 +00:00
ccremers
3ddedb6f7f - Totally untested. Otherwise, niagree should work ;) 2004-07-25 18:24:50 +00:00
ccremers
9723fff382 - Added termlistAddNew function to mimic set behaviour. 2004-07-25 18:14:21 +00:00
ccremers
f8aacee6ad - Improved some minor stuff regarding synchronisation checking and 
debugging info.
- '--pp=100' switch in debug mode now allows for disabling of
  synchronising_labels set.
 2004-07-25 15:30:58 +00:00
ccremers
4f1c9ecb48 - Amazingly, I think I implemented ni-synch partial order reduction. It 
still needs some careful analysis though.
 2004-07-24 20:30:00 +00:00
ccremers
60b02eea0e - Renamed nearly all files. Now, we try to use singular terms. 
Exception: states.h is the plural form.
 2004-07-24 19:07:29 +00:00
ccremers
bf991aa993 - Buggy: Broken intermediate version. 2004-07-24 19:00:43 +00:00
ccremers
ace16a896f - Renamed runs.[c|h] to system.[c|h], which makes much more sense. 2004-07-24 15:08:35 +00:00
ccremers
3ac2a8d9bb - Moved some parts of runs.c into roles.c 2004-07-24 15:05:20 +00:00
ccremers
1c234e3cee - Bugfixed claims.c (r722 log), although the reason for fixing and the 
error itself is quite irreproducable.
 2004-07-22 11:57:15 +00:00
ccremers
7ce5736af3 - Added attack script. 
- Worked on ni-synch claims.
  Todo: weirdness with: ./scyther ../spdl/nsl3-nisynch.spdl -t1 -r2
 2004-07-21 14:26:28 +00:00
ccremers
7e80d048d7 - Added reminder of this strange behaviour to todo.txt. 2004-07-21 14:06:03 +00:00
ccremers
056b5c245f - Big cleanup in modelchecker.c; threw out a lot of obsolete methods. 2004-07-21 12:42:04 +00:00
ccremers
6e8dcf8598 - Minor update to state progress bar cleaner. 2004-07-21 11:03:49 +00:00
ccremers
45950e3e56 - Lots of renaming on switches, to make it more readable. 2004-07-21 11:01:57 +00:00
ccremers
de1d114f86 - Much work on the new states counter abstractions. 2004-07-21 10:35:39 +00:00