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

1543 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
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
939ece7500 - Improvements in the scenarios. 2004-08-27 19:08:31 +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
dfdea5b0bf - Finished the protocol. 2004-08-23 11:59:42 +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