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

637 Commits

Author SHA1 Message Date
ccremers
0184b6277b - Better handling of function from M0 collapse in dot output. 2006-07-02 12:51:19 +00:00
ccremers
aeac3d6616 - M_0 function application is now absorbed. 2006-07-02 12:03:57 +00:00
ccremers
c52a340d8e - Improved heuristics. Default is now 162 (but 99 performs equally well) 2006-06-29 07:49:23 +00:00
ccremers
d87d9ede30 - Fixed some comments. 2006-06-12 14:48:57 +00:00
ccremers
780ca9880f - Added feature to ensure include files come from the right place. The 
order in which Scyther searches for files is now.
   1. From the prefix of the previously found file.
   2. Current directory.
   3. Anything in SPDLDIRS
  Here, 1 is new.
- When using -E (--expert), scyther shows any files it reads on stderr.
 2006-06-11 15:22:20 +00:00
ccremers
6ac5e2a428 - Added '--lightness' switch. 2006-05-26 12:57:27 +00:00
ccremers
07cc2c2b55 - Minor updates in output format. 2006-05-26 12:34:37 +00:00
ccremers
2e94dd065e - "--clusters" output is quite advanced, but still dot makes a bit of a 
mess out of it. One of the reasons is that the intruder events
  cannot be used along with the normal ranking, because they no longer
  correspond to real events.
 2006-05-26 11:27:05 +00:00
ccremers
e3b84a0f67 - New '--clusters' switch: needs some work. 2006-05-26 09:39:10 +00:00
ccremers
0679cbc3b8 - Added '--monochrome' switch, to be used in thesis output. There is a 
hardcoded lightness factor in dotout.c (MONOCHROMEFACTOR)
 2006-05-25 20:35:01 +00:00
ccremers
6a74883adf - Restricted the syntax somewhat, to avoid people typing crap. 
(Cf. Golsteijn)
 2006-05-16 15:00:21 +00:00
ccremers
6dff931dbc - Term identifiers can now contain primes (SM) 
- If labels start with a bang (!), they are ignored in synch/agree
  claims.
 2006-04-25 13:58:14 +00:00
ccremers
974e5f7315 - Reset encryption level issue. 2006-04-13 12:43:13 +00:00
ccremers
08f705234b - Added `include "dinges";' command, that is aware of Scytherdirs. 2006-04-12 12:42:04 +00:00
ccremers
db8e72f37e - Misc fixes to heuristic. 2006-04-03 08:21:52 +00:00
ccremers
d2058d937b - Revised cost heuristic. Trace length is no longer the real 
optimization.
 2006-04-02 12:29:02 +00:00
ccremers
e1890ddc9f - Improved cost function: now also avoids using initiators when 
possible.
 2006-04-02 12:07:25 +00:00
ccremers
52708d09b4 - MakeTraceConcrete now yields nicer choices, e.g. "Agent1" or "Nonce2". 2006-04-02 11:56:22 +00:00
ccremers
8c03bba02a - Fixed a bug in output overwrite for de-class code. 2006-03-31 12:24:32 +00:00
ccremers
4d7b744e1b - Discovered ugly bit in de-class code, which causes what seem to be 
errors with --extravert: even if Alice is already occurring in the
  system, the name can be used.
- Added explicit level 2 encryption bound. This is technically
  incorrect, but for now it should work.
 2006-03-31 10:12:58 +00:00
ccremers
cb440700e3 - Added --unique responder/initiator switches, which are both implied by 
--extravert.
 2006-03-31 08:24:41 +00:00
ccremers
5fe55d35cf - Code refactoring. 2006-03-28 14:45:02 +00:00
ccremers
b224344b59 - Bugfixed --extravert. 2006-03-28 14:24:46 +00:00
ccremers
ac87af60c1 - More improvements. Current drawbacks: Intruder choice still not clear. 2006-03-20 09:54:45 +00:00
ccremers
f3d4e8c350 - Some improvements to the intruder nodes. 2006-03-20 09:40:45 +00:00
ccremers
543e430e6c - In the light of recent discoveries on Athena method, I reinstated the 
--match switch.
 2006-03-20 08:47:12 +00:00
ccremers
881eccd6be - Fixed --disable-intruder: it now also uses no tupling shortcuts. 2006-03-19 12:59:26 +00:00
ccremers
a35a618a27 - Cleanup; make headers more compact. 2006-03-16 16:15:14 +00:00
ccremers
f11f1fff0b - Bugfix for dot output. 2006-03-16 13:26:46 +00:00
ccremers
3241c0c828 - Better class printing for the headers. 2006-03-16 08:49:10 +00:00
ccremers
1ce03104c5 Major: 
- Added rho/sigma/constants fields to the runs, on which the new code is
  based. Over time, .locals should be deprecated in favour of these
  better variants.
- Untyped variant is out of grace for the time being (cf. Athena interm
  problems)
- Improved graph output further.

Minor:
- Added TERMLISTADD and APPEND macros for more concise code.
 2006-03-15 21:30:19 +00:00
ccremers
5624f7e7b6 - Added some comments. 2006-03-15 08:56:23 +00:00
ccremers
25244c5b23 - Fixed bug in new tuple expansion code (again, caused by the intricate 
"realX" versus "isX" distinction.)
- Added structures for rho, sigma, constants, but did not activate them
  yet.
 2006-03-15 08:51:08 +00:00
ccremers
2b9246bb64 - Bug report: this should be fixed. 2006-03-15 08:33:09 +00:00
ccremers
16a59624fe - Revised dot output. 
- Reintroduced intruder events.
  - Added colors.
 2006-03-14 11:37:28 +00:00
ccremers
f7ee9743d2 - Bugfix for self-initiator detection. Woops. 2006-03-13 14:19:01 +00:00
ccremers
74052cf226 - Code cleanup for intruder count. 2006-03-10 14:52:45 +00:00
ccremers
af07f0cc3f - Removed obsolete stuff. 2006-03-10 14:51:05 +00:00
ccremers
895852de89 - Added iterators. 
- More space in encryption notation for better readability.
 2006-03-10 14:48:40 +00:00
ccremers
2280187b32 - Improved dot class output. 2006-03-08 15:12:58 +00:00
ccremers
5487d3ae90 - From this version onwards, Scyther no longer supports the modelchecker 
method. A big cleanup has been started, but is not finished yet, so
  minor artefacts might still remain. These are to be cleaned up later.
 2006-03-08 13:58:46 +00:00
ccremers
2830c8e8ff - Fixed some Doxygen documentation errors. 2006-03-08 12:38:39 +00:00
ccremers
1678577ce0 - Improved proof reports. 
- Minor (epsilon type) efficiency improvement.
 2006-03-05 15:18:39 +00:00
ccremers
527bf8baa5 - Better error reporting for local order constraints. 2006-02-28 15:33:12 +00:00
ccremers
f3d94b8e0d - Removed old hack lemmas by clean ones. 2006-02-28 15:01:58 +00:00
ccremers
282c0d5094 - --experimental is now available in the normal version, but for experts 
only.
 2006-02-28 14:06:12 +00:00
ccremers
a4429d548f - Turned 'hidden' term lemma back on by default. 2006-02-28 13:57:38 +00:00
ccremers
00616e45ed - Bit masking was incorrect: & binds less strong than == ! 
This caused many of the --experimental switches not to work.
 2006-02-28 13:41:36 +00:00
ccremers
cf832ca1b1 - Seems to work again, but further testing is needed. 2006-02-27 22:27:09 +00:00
ccremers
b49d13b6ee - [[[ Broken commit. ]]] 
Stuff seems to be working again, slightly less efficient though (count
  states).
 2006-02-27 16:08:17 +00:00
ccremers
bb16bd755e - Print states in a more countable format. 2006-02-27 15:20:37 +00:00
ccremers
c22173e5ee - [[[ Broken commit ]]] 
More work on the arachne multiple-decryptor. Horrific.
 2006-02-26 20:01:22 +00:00
ccremers
95df010a54 - [[[ Broken commit ]]] 
More intermediate work.
 2006-02-26 17:18:59 +00:00
ccremers
0ce88af6ac - [[[ Broken commit ]]] 
Committing partial new Warshall work because it is getting too big.
 2006-02-26 15:00:58 +00:00
ccremers
1d3d154a2f - If the timebound is hit, it should be reported anyway, because the 
results are not to be trusted anymore.
 2006-02-23 16:21:25 +00:00
ccremers
b16023bf0e - Cleaned up heuristic code. Note that there is a "hidden" heuristic: 
implicitly, older goals are resolved first, if some goals have equal
  weights. This is encoded in the "w <=" comparison; if this is set to
  "w <", the heuristic becomes much less effective.
 2006-02-23 15:03:43 +00:00
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