Commit Graph

343 Commits

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