andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
770 Commits 1 Branch 0 Tags 21 MiB
4a363aa33c
Commit Graph

494 Commits

Author SHA1 Message Date
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