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

89 Commits

Author SHA1 Message Date
ccremers
0fddd9f566 - Some fixes after pedantic tests. What remains: (a) C++ style comments (//) and (b) nested functions. 2007-01-06 18:01:36 +00:00
ccremers
89c3a20acf - Many cleanups to make -Wall happy. Next up is pedantic... 2007-01-06 14:45:29 +00:00
ccremers
ec9bf11719 - New semantics for maxattacks 2006-11-23 10:49:28 +00:00
ccremers
d8414daf95 - Fixed bug in new --max-attacks semantics. 2006-11-23 10:40:10 +00:00
ccremers
e902aaa260 - Added well-formedness checks. This will only be enabled if a role uses 
the 'knows' keyword.
 2006-07-31 11:08:51 +00:00
ccremers
df1a56c780 - Iteration seems to work nicely, thank you. 2006-07-27 11:55:24 +00:00
ccremers
f00392ac3e - Added functional 'knows' keyword. 2006-07-27 10:44:12 +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
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
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
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
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
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
527bf8baa5 - Better error reporting for local order constraints. 2006-02-28 15:33:12 +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
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
5d2d836d07 - Much work for the skeleton of the Hidelevel lemma. 2006-02-21 20:29:05 +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
1ee77472a0 - --max-attacks=AnyGijsNumber. 2005-08-15 12:49:32 +00:00
ccremers
164e325659 - New attack attribute. 2005-07-01 13:25:54 +00:00
ccremers
b6e9841c0f - Moved special terms into their own (very) special file. 2005-06-16 14:10:07 +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
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
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
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
3fba68b240 - Whoops, stupid sloppy switch code rewriters ought to be punished. 2005-05-12 11:59:31 +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
738a2b5859 - Rewrote complete switch code. Scyther now no longer depends on 
argtable2. Great.
 2005-04-10 15:30:47 +00:00
ccremers
5c90a5af29 - Improved the .dot output format quite a bit. 2005-02-21 15:12:59 +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
54ccd5179e - Added a new selector that picks goals that are local variables. 2004-12-29 16:05:32 +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
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
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
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