andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
1,691 Commits 1 Branch 0 Tags 21 MiB
de77d2afaa
Commit Graph

931 Commits

Author SHA1 Message Date
ccremers
f333fb8276 - Explicit casts. 2006-02-23 10:44:44 +00:00
ccremers
8f896432d1 - Added some stuff on the new graph code. 2006-02-22 16:58:11 +00:00
ccremers
f376260512 - Changed default heuristic to 34. 2006-02-22 15:57:55 +00:00
ccremers
41e797413c - Added new heuristics based on hidelevel results. 
Preliminary results:
  1. For typed matching, either heuristic 32 or 34 are best, and far
  superior to the previous best (3).
  2. For untyped matching, partial tests indicate that heuristic 1 is
  best, which is rather interesting.
 2006-02-22 15:48:58 +00:00
ccremers
921c82876d - experimental=4 now disables some things. Weirdly enough, they don't 
seem to make much difference.
 2006-02-22 09:53:50 +00:00
ccremers
dbc0a3583d - Better setup for --experimental= switch using bit masks. 2006-02-22 08:55:42 +00:00
ccremers
10b6793d97 - More cleaning of switches. 2006-02-22 08:47:22 +00:00
ccremers
5ddcdfed22 - Added --long-help and -E, --expert switches. 2006-02-22 08:41:06 +00:00
ccremers
b2e40e07f3 - Some more work on hidelevel backbone. 
- Added '--count-states' switch for the Arachne engine.
 2006-02-22 08:24:29 +00:00
ccremers
d3f2971181 - Reindent script was improved (and consequences added) 2006-02-21 21:35:14 +00:00
ccremers
5d2d836d07 - Much work for the skeleton of the Hidelevel lemma. 2006-02-21 20:29:05 +00:00
ccremers
bb7259a1ad - Removed some too interesting pruning methods that really need theorems 
first. Revealed by the certified e-mail protocol by Abadi and
  Blanchet.
 2006-01-17 16:18:26 +00:00
ccremers
3ed59b867a - Added an idea. 2006-01-17 12:30:16 +00:00
ccremers
f0715c030d - Stored good idea. 2006-01-09 11:56:44 +00:00
ccremers
baf1856943 - Added some tokens for future usage: 'function', 'hashfunction', 
'knows', 'trusted'.
 2006-01-09 09:38:17 +00:00
ccremers
8b30526a57 - Added a note about inversekeys in a role definition. 2006-01-07 13:28:13 +00:00
ccremers
96e7a32bff - Added '--unbounded' switch. 2006-01-06 12:46:04 +00:00
ccremers
99861d3e03 - Added '--untyped' switch which is to be preferred above the older 
--match=2 notation.
 2006-01-06 12:23:11 +00:00
ccremers
d9b0f412e4 - Added a good idea. 2006-01-06 12:11:32 +00:00
ccremers
92342683f5 - Cleanup of unused structure. 2006-01-03 11:34:48 +00:00
ccremers
c9eaf1f95f - Minor stuff. 2006-01-03 11:34:27 +00:00
ccremers
066bc810d8 - Notes on the warshall algorithm that is currently taking a third of 
processing time, which is way too much.
 2006-01-02 21:19:53 +00:00
ccremers
da75862d82 - Huge code documentation effort. 2006-01-02 21:06:08 +00:00
ccremers
6676266f4a - More refactoring to improve the code. 2006-01-02 20:18:47 +00:00
ccremers
e6505a72a3 - Further refactoring. 
- Some cleanup.
 2006-01-02 19:55:34 +00:00
ccremers
a5acc4984a - More refactoring for Arachne. Slowly we're getting somewhere. 2006-01-02 19:19:23 +00:00
ccremers
e592a0a432 - Refactoring code: splitting stuff out of arachne.c 2006-01-02 18:43:25 +00:00
ccremers
4023ef237e - Some reindentation. Nothing interesting, just syntax. 2006-01-02 16:07:56 +00:00
ccremers
e21627442a - Added 'singular' directive for roles. Syntax: 
protocol ns3 (I,R)
  {
    singular role I:
    {
    }
  }
 2006-01-02 16:05:53 +00:00
ccremers
724faa8949 - Cleaned up some printf's and warnings in compiler.c 
- Added warning for unspecified roles.
 2006-01-02 15:29:41 +00:00
ccremers
6516741983 - More notes. 2006-01-02 15:10:40 +00:00
ccremers
25fe5b210e - Idea about timestamps added. 2006-01-02 14:34:46 +00:00
ccremers
28f13aff26 - Added some final-day notes for 2005. 2005-12-31 19:34:50 +00:00
ccremers
441644e6d2 - Fixed the ECSS version copy. 2005-12-30 15:56:05 +00:00
ccremers
8c04a7517c - Added script to copy the latest Scyther version to the ecss 
repository.
 2005-12-30 15:54:32 +00:00
ccremers
d2ac518234 - Fixed typo in --help (noted by Sjouke) 
- State-space should generate classes.
 2005-12-30 15:11:39 +00:00
ccremers
6f670d7ab6 - In xml output, renamed 'attack' tag to 'state', which in general 
reflects better what it describes.
 2005-12-30 12:17:25 +00:00
ccremers
4a363aa33c - Bugfix: the single attack output adaptions from revision 1447 had 
broken some of the xml output.
 2005-12-30 12:03:19 +00:00
ccremers
ebf50b5252 - Removed the bold for complete proof. 2005-12-29 13:36:01 +00:00
ccremers
3b897c3872 - Added '--check' switch, to see whether your protocol terminates at all 
if there is no intruder.
- Restructered many switches.
 2005-12-29 12:52:51 +00:00
ccremers
a50245734d - Fixed the broken '--no-intruder' switch. 2005-12-29 12:14:21 +00:00
ccremers
c79c9eb73f - Added color output but forgot to add the sources files, fixed. 
- Note: ~ is not expanded in SCYTHERDIR because it is not handled by the
  shell; thus $HOME should be used.
 2005-12-29 11:03:18 +00:00
ccremers
515dec7f8b - Added note on usage of '~' in SCYTHERDIR. 2005-12-29 10:56:09 +00:00
ccremers
ab2f2469c0 - Added help text for the environment variables. 2005-12-29 09:35:08 +00:00
ccremers
1aca8460a3 - SCYTHERDIR environment variable is now used: colon-separated list of 
directories to search. Oblivious to trailing slashes.
 2005-12-29 09:25:42 +00:00
ccremers
efb3ec232b - Added some new thoughts, cleaned up old ones. 2005-12-28 22:52:22 +00:00
ccremers
d21f292330 - Renamed '--monochrome' to '--plain', which is nicer and shorter. 2005-12-28 18:40:58 +00:00
ccremers
3686a69869 - Added SCYTHERFLAGS environment variable. 2005-12-28 16:33:08 +00:00
ccremers
ab75acea62 - Added colour output, with --monochrome switch to disable this. 2005-12-28 15:27:22 +00:00
ccremers
e19f8bddd1 - Improved Reachable claims output 
- Use square brackets for remark output instead of normal brackets.
 2005-12-28 14:42:46 +00:00
ccremers
bceaca28f0 - Improved some type of warnings for e.g. empty prec sets andsoforth. 2005-12-28 14:25:06 +00:00
ccremers
72162e82c6 - Some cleanup. 2005-12-28 12:13:17 +00:00
ccremers
39adf85c6a - Reverted previous version: Tickets can possibly be secret as well 
(although this is dubious, as the claiming role will not know the
  contents in many cases)
 2005-12-28 12:04:00 +00:00
ccremers
dce2befd50 - Don't add secrecy claims for ticket types. 2005-12-28 11:59:39 +00:00
ccremers
0505aaacd6 - New claim: CLAIM_Reachable 
- Added new switches:
  -G,--generate-statespace
  -C,--generate-claims
- Claims are now allowed to have no label (they will be generated
  automatically)
- Output summary shows parameter of claims
- Internally, new symbols can now be generated by
  symbolNextFree(prefixsymbol)
 2005-12-28 11:50:17 +00:00
ccremers
ccc4c34823 - Added '--remove-claims' switch to cut off all existing claims. 2005-12-27 13:53:49 +00:00
ccremers
ca4c5674ac - Added check for non-used variables. 2005-12-27 13:44:12 +00:00
ccremers
397298290b - Improved output significantly. 2005-12-27 12:24:12 +00:00
ccremers
5ff71fa661 - Some cleanup. 
- Added 'all-atacks' switch.
 2005-12-27 12:01:17 +00:00
ccremers
28774cb94c - Moved dot output (finally) into a separate file, and made some minor 
improvements.
 2005-12-27 11:50:46 +00:00
ccremers
c4628e8be6 - Added support for more intelligent bounding. Fairly untested at the 
moment.
 2005-12-27 11:19:45 +00:00
ccremers
c20810def5 - Added preliminary support for singular attack output. 2005-12-27 10:49:22 +00:00
ccremers
ff503b24af - Added some todo stuff for the very near future. 2005-12-26 16:45:16 +00:00
ccremers
cb2aef3915 - Old state/time info has now been removed. This was only needed for the 
POR engine anyway, so that's where it is shown now.
 2005-12-26 16:28:45 +00:00
ccremers
32f226f782 - Better switches explanation. 2005-12-22 12:33:35 +00:00
ccremers
aae3cd70cb - Lowered default number of runs to 5. 2005-12-22 12:27:34 +00:00
ccremers
0259b2302c - Changed default behaviour: -d is needed to get dot output. 2005-12-22 12:24:27 +00:00
ccremers
e82ce8b962 - Added --no-intruder switch, but it is currently broken. 2005-12-21 19:02:41 +00:00
ccremers
aab5328a9b - Added a note. 2005-12-09 13:15:34 +00:00
ccremers
6543a8f659 - Added '--extravert' switch, which avoids initiator Alice to talk to 
Alice.
 2005-11-29 09:15:16 +00:00
ccremers
5276630007 - FIX: DOS newlines are now also accepted. 2005-11-28 08:27:05 +00:00
ccremers
e51b54af23 - FIX: Instantiation of variables is now the default. 
- NEW: -C --class switch to reset this.
- NEW: max runs is now 6 by default for usability. For unbounded search,
  use -r 0 or --maxruns=0
 2005-11-12 21:26:50 +00:00
ccremers
41132afea3 - Finally fixed the 'IV', 'RV' nuissance for global variables such as 
the role names.
 2005-11-12 21:16:02 +00:00
ccremers
76666404b0 - Added '--concrete' switch to fill in to pick readable names for 
variables.
 2005-11-12 21:13:00 +00:00
ccremers
c1c0b856de CHG: Changed default behaviour to Arachne engine. 
NEW: Added 'S' switch for --summary things.
 2005-11-04 13:23:30 +00:00
ccremers
5e1ca56f87 - Added experimental feature: explicit unique origination. This has to 
be investigated further, because it seems to reduce just a few states.
  Note to Gijs: stay away from this, you should be writing your thesis.
 2005-10-08 20:57:39 +00:00
ccremers
9f8f04c41c - Switched to the new consistency checking base. 2005-10-08 20:47:31 +00:00
ccremers
2ead7ab2ff - Improved code for new preferred order swapping of substitutions. Also 
included more comments.
 2005-10-08 20:22:24 +00:00
ccremers
2e495099bb - Added functions to globally check variable substitution consistency. 2005-10-08 20:03:31 +00:00
ccremers
2452a34671 - Added 'termlistMinusTermlist' function. 
- Added TERMLISTERROR constant, and corresponding tests.
  Note that this will not work in many contexts, because only NULL is
  usually considered to be a special value. It is purely intended for
  the new type evaluation functions in type.c.
 2005-10-08 19:56:04 +00:00
ccremers
fe730716ca - Added 'agenttypecheck' switch. 2005-10-08 19:54:30 +00:00
ccremers
a3b009f119 - The state of sys->variables was not maintained correctly, because 
terms were destroyed before it could be tested whether they were in
  sys->variables. Thus, garbage was left in sys->variables. This has
  gone undetected because it was never really used. Hmpf.
 2005-10-08 19:53:10 +00:00
ccremers
ea5bc6893f - Slightly smarter substitution in the symmetric case, when we make Var1 
equivalent to Var2.
 2005-10-07 20:38:41 +00:00
ccremers
83bf0ec704 - Added tuple_to_termlist function. 2005-10-07 14:02:46 +00:00
ccremers
1c075db161 - Added '--experimental=<int>' switch for debug version. 2005-10-07 13:09:07 +00:00
ccremers
5b73d707a0 - Rewrite of actor/agent type consitency code: now more aware of 
initiator/responder difference.
 2005-09-09 10:05:29 +00:00
ccremers
5c0c5d3333 - Better XML output for variables section. 2005-09-08 13:30:00 +00:00
ccremers
01a45f87d2 - Rewrote variables section, integrated typeflaw info. 
Note that for variables that are not instantiated, only the variable
  and the type info is shown. For instantiated variables, both are
  shown.
  In this output the attribute 'free' should be ignored, as its
  output is not accurate here.
 2005-09-08 12:55:32 +00:00
ccremers
48574de13e - Minor improvement to type flaw output: now also shows the type of the 
substituted term.
 2005-09-07 07:21:13 +00:00
ccremers
e104dddbfb - Added a switch to number the limit of intruder actions. 
Initial testing suggests it does not influence the number of states
  much for values of 2 and higher.
 2005-08-21 21:38:32 +00:00
ccremers
c330a5b719 - Added some thoughts. 2005-08-21 21:36:00 +00:00
ccremers
1ee77472a0 - --max-attacks=AnyGijsNumber. 2005-08-15 12:49:32 +00:00
gijs
998e4852ba - Allow ^ and - in identifies which will be used in protocol names 
in future naming conventions
 2005-08-15 11:27:46 +00:00
ccremers
2e9e43742e - Added more fine-grained control for the associativity of tupling: 
--tupling=n	* 0: right-associative; 1: left-associative; others are
  reserved for future use.
  --ra-tupling	* Sets the default, but is there for symmetry.
 2005-08-12 12:59:25 +00:00
ccremers
cb315aafc8 - Added '--extend-trivial' switch. This is not a complete '--extend' 
algorithm, as it is pretty dumb, but it works in most cases. Use with
  care.
 2005-08-12 12:13:50 +00:00
ccremers
56f7cf5df2 - Added switch '--la-tupling' to enforce left-associative tupling 
instead of the default right-associative tupling. Note that this only
  matters for full typeflaw matching.
- Adapted multi-nsl test script to test for both association variants.
 2005-08-12 07:28:44 +00:00
ccremers
cee11bc0af - Extra checks: 
* For incomplete protocols, better handling of dangling labels.
  * For termSubTerm better handling of NULL cases.
 2005-08-11 12:56:36 +00:00
gijs
c8d2222c58 - Allow identifiers to start with @ so that internal protocols 
such as key compromise and swapkey can be prefixed with @ to indicate
  that they should be ignored by the classification tool.
 2005-08-11 12:24:36 +00:00
ccremers
2cd9cf4148 - Added random goal picker. Untested. 2005-08-01 12:59:30 +00:00
ccremers
4cbf2383f7 - Addition. 2005-08-01 12:59:05 +00:00
ccremers
da1b759dc0 - Added shortcut script for Arachne engine. 2005-07-26 10:13:16 +00:00
ccremers
f7f2bf27bb - Added type flaw information (just after the variables section) 
In pseudo-xml:
  <typeflaws><run id="1"><typeflaw><term variable /><termlist type(s) /><term value of variable /></typeflaw></run></typeflaws>
 2005-07-06 14:33:05 +00:00
ccremers
a1fdbe119f - Incorporated untrusted agents list (<untrusted> element in attack, 
containing a <termlist>)
- <commandline><arg>./scyther</arg> <arg>-x</arg>... is now available.
 2005-07-01 13:46:18 +00:00
ccremers
6a3e57913c - Quick addition of Gijs' suggestions. 2005-07-01 13:27:38 +00:00
ccremers
164e325659 - New attack attribute. 2005-07-01 13:25:54 +00:00
ccremers
464920907b - Added '--extend-nonreads' switch. It is totally untested, and I hope 
Gijs will have a look at it and tell me whether it actually works.
 2005-06-21 11:04:34 +00:00
ccremers
b6e9841c0f - Moved special terms into their own (very) special file. 2005-06-16 14:10:07 +00:00
ccremers
db18b203a9 - Added "Empty" claim type, which is ignored. 
Syntax example:   claim_x(I, Empty);
 2005-06-16 11:59:44 +00:00
ccremers
013afc99aa - Fixed a newly introduced bug. When the decryptor sequence unfolding 
code was added (two weeks ago), bindings were changed without changing
  the state of the graph closure buffer. This resulted in possible
  missed loops: thus, reports of broken claims could be found in the
  output, in inconsistent states. (Reported bij Gijs Hollestelle.)
  Note that this only influences the current development release, and
  not any previous results.
 2005-06-08 13:51:40 +00:00
ccremers
1bdaf7b5d9 - Large rewrite of switch code. Instead of having switch parameters in 
the (monstrously large) system structure, there is now a global
  'switchdata' structure originating in switches.c. This makes it much
  easier to see what's happening.
  * Note: although this code has been tested, there might be some
    hiccups, because doing multiple search&replace actions over all
    files is bound to cause some problems.
 2005-06-07 15:02:27 +00:00
ccremers
c4fad31f25 - Executable. 2005-06-07 14:57:52 +00:00
ccremers
eb36abee75 - Indent any changed .c / .h files. 
Intended to be used just before a commit.
 2005-06-07 14:56:17 +00:00
ccremers
1331f5e7a3 - Added a global attack id, starting at one. Currently only shown in 
XML and Dot output. For Dot, it is included in the label. For XML, it
  is an added attribute of the 'attack' tag.
 2005-06-07 13:40:56 +00:00
ccremers
22a0d2adfb - Some cleanup. 2005-06-02 12:42:10 +00:00
ccremers
4a42604cb6 - Added Ticket basic term type. Note that this only has consequences for 
the Arachne type checking. The net result is that a variable of type
  'Ticket' can always contain any term, even with -m0 or -m1 matching.
 2005-06-02 12:14:28 +00:00
ccremers
cd2ef14e4e - [Syntactical changes only] 
Fixed the indentation of some files.
 2005-06-02 09:40:05 +00:00
ccremers
01124e2104 - Modified a number of things related to the attack analysis tools. 
* removed <term> wrappers
  * added <const> wrappers
  * removed <role><term> construct, now <rolename>R</rolename>
    constructs.
  * added <variables> section.
  * variable substitutions are followed through in runs. Thus, only
    unbound variables occur in the semitrace.
  * added the untested claims back in, so that all events in a
    role/semitrace are now shown. Note that they can be disabled
    again by using the new '-H' switch.
 2005-06-02 08:25:45 +00:00
ccremers
0540b744e2 - Repaired a pruning method that still needed a lemma. It was a bit 
overzealous and killed a woolam-mutual attack.
 2005-05-19 14:43:32 +00:00
ccremers
f22ce0dcb9 - Big change in the Arachne algorithm: decryptor sequences now get 
expanded explicitly. This solves a long-standing issue with {k}k
  decryption to yield k. Needs some testing to ensure that it did not
  introduce any new errors.
 2005-05-17 18:45:01 +00:00
ccremers
b5af43294e - Added inverse keys to output. 2005-05-17 13:00:45 +00:00
ccremers
ffaf0d2ded - Filtered out uninteresting claim events in attack descriptions. This 
was already being done in the script by Gijs. I only added it to make
  the XML output more readable for humans.
 2005-05-13 13:40:37 +00:00
ccremers
8b51593cf5 - Each attack now includes 
* Initial knowledge
  * Role definitions for protocols involved
 2005-05-12 14:52:50 +00:00
ccremers
a856e795b0 - Reindented stuff (this was needed, really) 2005-05-12 13:19:32 +00:00
ccremers
d02621c608 - Added XML term output to Scyther. This meant in fact that a lot had to 
be recoded, avoiding e.g. label="<term ..." constructs. Therefore,
  many attributes have changes into elements. Beware.
- Made bindings implicit to events using <follows> and <after>
  constructs. Also added a new <choose> for unbound simple variables.
 2005-05-12 13:18:37 +00:00
ccremers
3fba68b240 - Whoops, stupid sloppy switch code rewriters ought to be punished. 2005-05-12 11:59:31 +00:00
ccremers
934eb3fd2a - Oops, sloppy. (It's good to have a beta tester homey.) 2005-05-04 12:06:30 +00:00
ccremers
3bbaf0fc97 - Added scyther wrapper tag (cf. GH bug report) 
- Fixed binding closure (cf. GH bug report)
- Reduced indenting to two instead of three spaces.
 2005-05-03 09:45:54 +00:00
ccremers
71558706a6 - XML output should be workable now. 2005-05-02 13:38:45 +00:00
ccremers
924abc065d - Added xml output switch (-x, check scyther --help). It's not complete 
yet, to be finished tomorrow.
 2005-05-01 13:32:50 +00:00
ccremers
f206d4258f - Events now always require a label. 2005-04-29 13:25:43 +00:00
ccremers
38f6f42351 - Fail increases of claims moved to violateClaim; thus, other references 
were in fact redundant.
 2005-04-27 13:48:00 +00:00
ccremers
7c0507a900 - Fixed bug where claim fails were not counted in the modelchecker, as 
reported bij GH. Attacks were indicated, though, so this only caused
  problems for users using --summary and not looking at the "attack:
  L:?" field.
 2005-04-27 11:43:47 +00:00
ccremers
18d523d8a4 - Fixed segfault when modelchecker was called on an empty scenario. 2005-04-22 16:03:58 +00:00
ccremers
8e1041b567 - Minor output fixes. 2005-04-21 12:04:45 +00:00
ccremers
9271cc7624 - Matching method propagation was wrong in new switch code. 
- Some fixes for protocols that do not include matching send/read
  combo's. In particular, the max encryption level method ranged over
  the sends; now over all events. Maybe it can range over read events
  only?
 2005-04-18 05:51:25 +00:00
ccremers
f9a97fb481 - Stupid typo fix. 2005-04-15 14:33:18 +00:00
ccremers
771fa8cc92 - Some more interface improvements. 
- Hardcoded reference to wiki pages.
 2005-04-15 14:31:32 +00:00
ccremers
1f8d9dbe5e - Performad a big cleanup of the switches, making the resulting list more compact and more useful. 
* Hiding of 'discouraged' options: these should not be used by e.g. students.
  * Hiding of 'unimportant' options: not harmful, but not often used either.
 2005-04-15 10:04:05 +00:00
ccremers
a06b3037a4 - Added Scons suggestion. 2005-04-15 10:02:22 +00:00
ccremers
3ba39a3a51 - Removed some older debug stuff. 2005-04-10 15:40:33 +00:00
ccremers
4919cf2a2d - Some consistency fixes after removing argtable2 dependency. 2005-04-10 15:36:41 +00:00
ccremers
738a2b5859 - Rewrote complete switch code. Scyther now no longer depends on 
argtable2. Great.
 2005-04-10 15:30:47 +00:00
ccremers
88e2f3d26c - Added a better reverse-engineered variation of the Athena goal 
selector.
- Added an idea that might make searches somewhat faster.
 2005-03-11 20:41:59 +00:00
ccremers
560acb220d - Removed an obsolete warning about -m2 2005-03-08 13:54:13 +00:00
ccremers
c8df32c7a2 - Minor improvements. 
* Old bindings detections (immediately binds them to older binding)
  * Know_only derivation for keylevel lemmas.
 2005-03-08 13:02:16 +00:00
ccremers
291353a14f - Improved version of the latex renderer of arachne attacks. Still not 
usable, however.
 2005-03-07 19:02:08 +00:00
ccremers
197117f2fe - Made a start with the arachne latex output. It's a mess currently. 2005-03-07 15:38:01 +00:00
ccremers
351d619324 - Out of the wiki, back into the source. 2005-02-25 14:54:28 +00:00
ccremers
b1c1ba455e - Added a good idea. 2005-02-21 15:15:22 +00:00
ccremers
5c90a5af29 - Improved the .dot output format quite a bit. 2005-02-21 15:12:59 +00:00
ccremers
b675b101bf - Added Arachne tuple claims warning. Exits for now at Secrecy tuples. 2005-02-19 14:31:15 +00:00
ccremers
e36392b1d2 - Rewrote the way the version number is imported into the source. Much 
better now.
 2005-02-01 20:05:41 +00:00
ccremers
56caa2c1e4 - Fixed the svn version number registering. Still needs some work 
though, as the -SVNVERSION thing only needs to be passed to the
  builder of main.c.
 2005-02-01 19:39:03 +00:00
ccremers
820c2caed8 - Revisited type matching conditions. 
- Introduced tuple unfolding stuff for Arachne. -m2 should work now.
 2005-01-14 18:18:40 +00:00
ccremers
d5cdac84cc - Some unfolding of tuple goals towards getting -m2 Arachne to work. 2005-01-14 14:08:01 +00:00
ccremers
b607b1e260 - If we run into the time bound, report it. 2005-01-14 13:01:31 +00:00
ccremers
9df1bfed5b - Made the output more easily machine-parsed. 2005-01-14 12:48:26 +00:00
ccremers
bd0069886c - "correct" output for claims that are not encountered, as one would 
expect.
 2005-01-14 12:38:43 +00:00
ccremers
9a5e9d674a - Removed some debugging output. 2005-01-11 10:03:34 +00:00
ccremers
e0e56964d1 - Added a --timer=x switch to abort Arachne proofs after x seconds. 2005-01-05 15:29:27 +00:00
ccremers
45c42408dd - Added weight level to proof output in <..> notation. 
- Added selection factor for singular variables (not rolenames)
 2004-12-29 19:40:12 +00:00
ccremers
54ccd5179e - Added a new selector that picks goals that are local variables. 2004-12-29 16:05:32 +00:00
ccremers
d425bdb850 - For now, set equal weights to the parameters. 2004-12-29 14:24:33 +00:00
ccremers
7309bb5550 - Fixed debug comment. 2004-12-29 14:18:13 +00:00
ccremers
5e695097f2 - Reimplemented the weight functions for goal selection. 
- Added --goal-select function, defaults to 3.
 2004-12-29 14:17:49 +00:00
ccremers
93ab6a29f4 - Omitted some addnew tests, although they ought to work. 2004-12-09 15:45:14 +00:00
ccremers
635470d976 - Added -d switch. 2004-12-09 15:27:50 +00:00
ccremers
b56c01c422 - Added '--max-depth=X' switch (which is equal to the old '-l X -a') 
- Modified semantics of -l with -a : this corresponds more to the
  intuition and introduces the new option to prune proofs based on trace
  length.
 2004-12-09 15:11:45 +00:00
ccremers
4f36181c3c - Removed debugging stuff, now that the memory stuff is solved. It 
turned out that I solved the memory leak first, and then spent an
  afternoon finding the 8 blocks. These were simply not being given back
  by memrealloc, which I should have guessed.
 2004-12-09 13:34:36 +00:00
ccremers
c7d9517eac - Fixed some errors. No more memory leaks. 2004-12-09 13:23:26 +00:00
ccremers
c690b0622a - More cleanup and comments. 2004-12-08 19:30:26 +00:00
ccremers
1c5a9986f6 - Added many comments. 2004-12-08 16:41:43 +00:00
ccremers
3ca180d968 - Despite a full afternoon of debugging, semiRunCreate/Destroy still 
lose 8 blocks. I'm fairly confused.
 2004-12-08 16:25:27 +00:00
ccremers
f2a2c8ea14 - Moved role creation into the protocol creation. This will make it 
easier to add MSC-style input to the input language compiler later.
 2004-11-16 12:51:23 +00:00
ccremers
506e42f841 - Re-indented the files. 2004-11-16 12:07:55 +00:00
ccremers
a38925c9c2 - Added some useful macros to term.h to address subparts (e.g. 
TermOp1(t)). Renamed all uses.
 2004-11-16 12:06:36 +00:00
ccremers
343314896b - Added version info to compilation process. 2004-11-01 14:52:52 +00:00
ccremers
b6af2f9dac - First try for diff function. 2004-11-01 14:06:26 +00:00
ccremers
c195ab95a1 - Now in the wiki. 2004-10-30 10:07:21 +00:00
ccremers
bdc336d7f9 - Todo list is now handled by the wiki: 
http://www.win.tue.nl/~ccremers/twiki/bin/view.pl/Scyther/ScytherBug
 2004-10-29 14:15:35 +00:00
ccremers
aaa0d415f9 - Graph closure fixed. 2004-10-28 15:37:13 +00:00
ccremers
0ec70b9de0 - Added lots of debugging info. 2004-10-28 15:23:16 +00:00
ccremers
3673fc689d - Improved roledef printing by adding roledefPrintShort. 2004-10-28 12:56:13 +00:00
ccremers
61457b5f3d - Fixed the agentsOfRunPrint output. It was caused by the agent adding 
order.
- Fixed the pruning bug, which was related to this.
 2004-10-28 12:33:57 +00:00
ccremers
234edae741 - Added sort of bug report. 2004-10-27 16:32:44 +00:00
ccremers
9a24bb0f21 - Somehow, agentOfRunRole is playing up. I found a bug in the pruning 
(untrusted actors), but the fix did not work. It's maybe due to the
  roleInstance variants.
 2004-10-27 16:20:12 +00:00
ccremers
461a040d29 - Revised Arachne dot output significantly. It is now based on explicit 
ranking instead of the subgraphs. This will make it easier to layout
  e.g. LaTeX MSCs using the same algorithm.
 2004-10-27 16:10:58 +00:00
ccremers
2680a2ca7a - Added rank calculation and output. If the subgraphs are removed, this 
will allow for better positioning of the graphs. It also helps a lot
  for latex output. In fact, latex output is fairly trivial now.
 2004-10-25 14:28:53 +00:00
ccremers
3cda6e53fa - Another important issue. 2004-10-20 15:59:23 +00:00
ccremers
fce9fae9c3 - Removed warnings from the compiler for conflicting types: not to 
stdout anymore, but now in the normal tradition of eprintf and
  globalError.
 2004-10-19 12:03:40 +00:00
ccremers
7b3cb4dfb9 - To test. 2004-10-18 14:36:43 +00:00
ccremers
8a7369a84e - Some stuff about empty preceding label sets and Arachne. 2004-10-18 13:49:41 +00:00
ccremers
67673cb608 - No more warning for output in standard debug mode. 2004-10-18 13:49:20 +00:00
ccremers
19b3c74e65 - Remove obsolete child parameter. 2004-10-18 13:06:22 +00:00
ccremers
94b3ac7c96 - Added debug code for dot output. 
- Push/pop goals are counted now, making the child parameter obsolete.
 2004-10-18 13:04:34 +00:00
ccremers
4b10c7f151 - Added priorities. 2004-10-16 22:03:33 +00:00
ccremers
abad7044dd - Added thingy. 2004-10-15 19:53:04 +00:00
ccremers
795f28006d - Added some thoughts. 2004-10-14 20:49:49 +00:00
ccremers
d33ec486ce - Modified -l switch to also serve as proof depth limit. 2004-10-14 15:25:28 +00:00
ccremers
ba832159b1 - Added a new prioritylevel for seemingly public keys, but the splice-as 
problem remains.
 2004-10-14 15:09:48 +00:00
ccremers
9ac12f9198 - More serious problem found. 2004-10-14 14:33:22 +00:00
ccremers
123b12a1c0 - Problems with Splice/AS suggest heuristic improvements. 2004-10-14 14:30:27 +00:00
ccremers
87a75106d1 - Printing the protocol tab-separated from the role is more useful for 
script-based parsing.
 2004-10-14 13:29:28 +00:00
ccremers
2bc1df6135 - Improved readability of printed claims. 
- Fixed comment.
 2004-10-14 13:19:36 +00:00
ccremers
40584ba6bd - Noted some stuff about graph computations, so that I won't forget 
this.
 2004-10-12 18:08:01 +00:00
ccremers
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.
 2004-10-12 16:58:29 +00:00
ccremers
d64badefdc - Found a problem with type flaw attacks. 2004-10-12 15:23:03 +00:00
ccremers
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.
 2004-10-12 15:12:20 +00:00
ccremers
3b4b367a4a - Minor correction. Probably redundant for a good compiler ;) 2004-09-20 17:41:53 +00:00
ccremers
02e99761ae - Split roleInstance into two more managable parts. 2004-09-20 12:40:01 +00:00
ccremers
be366afa0e - A good reduction idea for secrecy added to the todo list. 2004-09-07 09:56:06 +00:00
ccremers
8570465e48 - More todo. 2004-09-01 19:11:06 +00:00
ccremers
8b48aade68 - Huge effort to make match type 2 (typeflaw generic) matching work. 
Problem with goals that turn into tuples, will have to be solved.
 2004-08-31 14:31:06 +00:00
ccremers
0e9b7dcf11 - Some added error/bounds detection all around. 2004-08-31 12:35:05 +00:00
ccremers
a673ea4ad1 - Write down, so that we don't forget. 2004-08-31 08:58:50 +00:00
ccremers
f5ab30995c - Removed the debugging output. 2004-08-30 22:09:44 +00:00
ccremers
5c90522c55 - Fixed a bug in the pruning algorithm, where intruder runs were also 
checked for agent lists, which is false.
 2004-08-30 22:08:44 +00:00
ccremers
b04bc86185 - Some minor cleanups. 2004-08-30 21:49:51 +00:00
ccremers
4832e9116c - Added pruning theorem for untrusted actors. 2004-08-30 21:07:45 +00:00
ccremers
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.
 2004-08-30 20:48:11 +00:00
ccremers
8f441ac913 - Fixed some minor issues. 
- Fixed type flaw in labellist type.
 2004-08-30 20:08:11 +00:00
ccremers
02041cfbab - Fixed binding displays. 
- Improved attack dot output.
- goal_graph_create now takes originator assumption into account.
 2004-08-30 13:57:16 +00:00
ccremers
1d431dc6f1 - Attack output is a bit broken now for Arachne. Fix. 2004-08-30 06:07:17 +00:00
ccremers
5035a35d51 - Bug spotted. 2004-08-28 17:28:14 +00:00
ccremers
25fa261e30 - Added some comments. 2004-08-28 14:05:38 +00:00
ccremers
c907c1f657 - Added prefixed start nodes to indicate agent initiative in dot output. 2004-08-28 14:00:48 +00:00
ccremers
08f2155527 - Denoting 'empty term' with '*' from now on, yields more compact 
output.
 2004-08-28 14:00:22 +00:00
ccremers
391c939b83 - New algorithm to draw bindings between runs. Much cleaner. 2004-08-28 13:47:37 +00:00
ccremers
b349b6cef2 - More improvements to the dot output. 2004-08-28 12:42:11 +00:00
ccremers
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.)
 2004-08-28 12:20:50 +00:00
ccremers
2ddd1eee13 - Improved dot output for Arachne attacks. 2004-08-28 11:43:06 +00:00
ccremers
9d64b837db - Improved roledef printing for NULL, NULL roles (intruder) 
- Added graph output in dot format.
 2004-08-28 09:24:30 +00:00
ccremers
6c2730af1a - Added some todo stuff. 2004-08-27 19:29:41 +00:00
ccremers
4420e06e4e - Ignore choose actions when determining Arachne trace length. 2004-08-27 19:15:24 +00:00
ccremers
4f534410bd - Implemented ordering checks. Need some test to validate this though. 2004-08-27 19:06:15 +00:00
ccremers
957b920b98 - Added extra Arachne check for -r0. 2004-08-27 18:26:19 +00:00
ccremers
17ad6de97b - Semistate printing now reports trace length. 
- Pruning was wrong, so the shortest attack wasn't always found. Now it
  is.
 2004-08-27 18:18:16 +00:00
ccremers
198afa135e - Implemented attack length scanner per claim. Not stored yet. 2004-08-27 18:09:09 +00:00
ccremers
6ccb09297a - Better prune adherence. 2004-08-27 17:37:43 +00:00
ccremers
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.
 2004-08-27 17:35:23 +00:00
ccremers
21b2c27320 - Niagree claim seems to be working fine now. 2004-08-27 17:25:38 +00:00
ccremers
2decf44bd2 - Checks are now in. Untested though. 2004-08-27 15:02:33 +00:00
ccremers
68bbdc2794 - Added interfaces for the more interesting Arachne claim checks. 2004-08-27 14:48:58 +00:00
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
ccremers
1ecdd1eb5a - Made explicit chooses the default behaviour. 2004-07-20 21:31:28 +00:00
ccremers
81e715d612 - More cleanup and structuring in the modelchecker code. 2004-07-20 20:58:32 +00:00
ccremers
4d60acf431 - Rewrote all main traversal logics to use inline functions. 
- Added -t12. This is much faster than -t10, but yields equal states,
  and made it the default choice.
 2004-07-20 20:42:53 +00:00
ccremers
cfda7da8d9 - Remove some automake artefacts. 2004-07-20 14:17:22 +00:00
ccremers
d9d94073d1 - Finally solved the stupid warning. 2004-07-20 13:01:58 +00:00
ccremers
b570ca2d8a - Made all references to system explicit const references. 
- Removed config.h reference.
 2004-07-20 12:41:56 +00:00
ccremers
2065c89add - Added some more macro unfolding. 
- More efficient term equality test.
 2004-07-20 12:21:01 +00:00
ccremers
837fb4d8e1 - Corrected an inline definition, propagating it to the header file. 2004-07-20 09:47:06 +00:00
ccremers
d74d70218f - Improved candidates throughput. 2004-07-20 09:07:43 +00:00
ccremers
a588c90952 - Added some code optimizations after using gprof. 2004-07-20 08:51:23 +00:00
ccremers
ff0c29142e - Some modified options. Doxygen is not working currently, I don't know why. 2004-07-19 14:01:43 +00:00
ccremers
ffecc1a1ac - Added some doxygen documentation. 2004-07-19 13:31:44 +00:00
ccremers
03c19a4774 - Improved handling of pruning in explorify. Now, when pruning is done 
in explorify, the signal is passed back, and match_basic etc. will
  signal that the event was not enabled.
 2004-07-19 12:03:29 +00:00
ccremers
b412e56c7b - Traversal 10 is now the default. 2004-07-19 11:54:48 +00:00
ccremers
514848a10e - Implemented --no-noclaims-red and --no-endgame-red 2004-07-19 09:44:54 +00:00
ccremers
ee0501d82d - Implemented --no-agent-symm to disable agent symmetry reductions. 2004-07-19 09:34:46 +00:00
ccremers
7ad99f977c - Fixed weird behaviour of executeStep restoration. 2004-07-19 09:32:12 +00:00
ccremers
7769fdbdf6 - Useful shortcut script for all this bke testing. 2004-07-19 09:25:40 +00:00
ccremers
5be15eb73b - Added state space display script. 2004-07-19 08:55:23 +00:00
ccremers
23b4d167c8 - Removed some warnings to the debug version only. 
- Added -t11.
 2004-07-17 21:11:35 +00:00
ccremers
6a3edd06c2 - Cleaned up -t10, removed the inclination towards chooses. 2004-07-17 20:18:55 +00:00
ccremers
ff178f46a5 - The yywrap solution was wrong; it should return 1. Fixed now. 2004-07-17 19:52:07 +00:00
ccremers
ca975ed970 - Rollback of commit r674, because stuff was pretty broken. Work at that 
in phases.
 2004-07-17 19:43:20 +00:00
ccremers
570933612f - Fixed the yywrap dependency warning in scanner.l 2004-07-17 19:35:54 +00:00
ccremers
b70255ddbc - Fix symmetry reductions, choose might interfere with this. 2004-07-16 21:17:32 +00:00
ccremers
73f3b4d4ad - Fixed an error, where exit was used instead of error. 2004-07-16 14:11:56 +00:00
ccremers
a7a2ed2fbd - Added a preliminary SCons script. 2004-07-16 14:11:19 +00:00
ccremers
1e7ef8f11d - Lots of rewrites and code cleanups. 2004-07-16 13:09:46 +00:00
ccremers
5d42bf40df - State progress bar needs less updating. 2004-07-16 09:03:37 +00:00
ccremers
6cf65f068f - Implemented --symm-order reduction. This clashes with --read-symm, but 
it actually faster.
 2004-07-15 13:32:09 +00:00
ccremers
62b2eca8da - Implemented read symmetries reduction as a switch '--read-symm'. Works with e.g. t8. t10 is also implemented as a test. 2004-07-15 11:04:15 +00:00
ccremers
982b5e7ffd - Made some small, but very important, comments. 2004-07-14 13:18:08 +00:00
ccremers
27d3bb4061 - Previous entry was buggy; killing the roledef removed very extensive 
parts of the tree. Solved by restoring it after recursing, which is
  waht should have happened in the first place.
- It's still a good improvement though.
 2004-07-14 12:46:11 +00:00
ccremers
32c4183315 - Added some (commented out) better reporting code. 2004-07-14 12:17:38 +00:00
ccremers
82b2603263 - Implemented the irrelevancy cutter, which immensely improves 
performance.
 2004-07-14 12:10:39 +00:00
ccremers
269b5c7646 - Introduced the 'force-choose' switch, which helps the symmetry 
reduction algorithm along, notably.
 2004-07-14 09:33:55 +00:00
ccremers
1efa77859f - Removed choose warnings for now. 2004-07-14 08:33:28 +00:00
ccremers
81c6be826e - Initial symmetry reduction. Gives a lot of warnings currently. 2004-07-14 08:17:49 +00:00
ccremers
a5efc6106a - Static run symmetry detection seems to work just fine. 
- Added 'warning' call to error.h
 2004-07-14 07:31:01 +00:00
ccremers
508d49efbb - Added local step index to runs. 2004-07-14 06:55:05 +00:00
ccremers
5bb5f610fb - Added -t9 search, which does the chooses first. Doesn't seem to differ 
much from -t8 though.
 2004-07-13 20:20:58 +00:00
ccremers
8dee89217e - Cleanup of todo list. 2004-07-13 15:27:38 +00:00
ccremers
39a2b4878c - Debug of optimization. 
- Put down skeleton of new idea, related to a lemma from Niek Palm's
  work. This needs more investigating though.
 2004-07-13 15:24:47 +00:00
ccremers
b6806f6aaf - Significantly improved state reduction by scanning for states where no 
claim is to be evaluated anymore. This needs some reporting, and
  significantly alters comparisons with previous versions.
 2004-07-13 13:34:04 +00:00
ccremers
6d9c47a029 - Modelchecker now avoids some redundant traces. This should yield a 
25-30 percent decrease of states for most cases tested sofar.
 2004-07-13 12:36:50 +00:00
ccremers
72be9a6441 - Moved the attack path display logic to output.c completely. 
- Adjusting output slightly.
 2004-07-13 12:19:03 +00:00
ccremers
6fa0f3904d - Added more coloring. 2004-07-13 11:37:55 +00:00
ccremers
df9b97e5bc - If the --state-space switch is used, reporting is now always disabled. 2004-07-13 11:11:27 +00:00
ccremers
0c0a5021bb - Improved the trace highlight in the state space, but it isn't as I 
want it yet.
 2004-07-13 11:10:06 +00:00
ccremers
ae6b85f290 - Improved graph coloring etc. 2004-07-13 09:56:19 +00:00
ccremers
410a35f4f4 - Fixed bug in attack output. 
- Re-enabled the noreport switch.
 2004-07-13 09:36:30 +00:00
ccremers
981f0a92b4 - Started working on coloring of the attack trace in the state space. 2004-07-13 09:14:03 +00:00
ccremers
4b4c934b9c - Some hard-coded page sizing code. 2004-07-12 14:47:43 +00:00
ccremers
cd3025e04e - Added preliminary support for state space printing using the dot 
package. Use the "--state-space" switch.
 2004-07-12 13:58:41 +00:00
ccremers
363f95977a - Removed obsolete debugging output. 2004-07-12 13:57:59 +00:00
ccremers
ac4efcd63a - Added todos. 2004-07-12 09:26:25 +00:00
ccremers
ab72755bf5 - Function considerations. 
- M_0 considerations.
 2004-07-09 14:54:14 +00:00