From 9f97e1e5d7b9c107fb7b5814efbce4e123436758 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Fri, 25 May 2007 11:18:45 +0200 Subject: [PATCH] Moved todo text into a more sensible place. --- src/todo.txt | 54 ---------------------------------------------------- 1 file changed, 54 deletions(-) delete mode 100644 src/todo.txt diff --git a/src/todo.txt b/src/todo.txt deleted file mode 100644 index 595b7c1..0000000 --- a/src/todo.txt +++ /dev/null @@ -1,54 +0,0 @@ -- When saving a file after 'file changed' warning, an overwrite of the - same file should not necessarily generate a warning. -- Output (claim summary) might have a parameter summary somewhere. -- Error should have an additional line number parameter (that might be - -1 to ignore it) forcing people to use numbers :) - Format: "error: [%i] %s\n" -- Nested functions should be avoided: their implementation requires an - executable stack, which is bad for security purposes. However, many of - the iterator functions need to pass a function and possibly some - variables. Currently, the variables are handled by the nested function - mechanism (the iterated nested function and address variables of the - function it is part of), which would not work anymore. A possible - solution seems variable argument count functions, but this is fairly - cumbersome and might impact on performance. Alternatively, iterators - can be implemented as macros, which is probably the fastest, but maybe - less readable. -- --check is slightly f***ed up because there is no good semantics for - the --disable intruder check. As a result, it is now too strict can - cause correct protocols to fail. Fix. -- When *not* asking for attack output, maybe we should default to - --prune = 1. Then, if we ask for --xml output or --dot, we do: - if --prune == 1 then --prune == 2 now :) unless otherwise specified. - (This should be done after switch checking) -- Old version enforced some extra orders: - 1. M_0 roles were ordered before any other roles. - 2. Local constants order: if a run has a local variable instantiated by - somebody else's variable, that should occur then after the initial sending - of that value... -- Test 'sk(x)' in goals, somewhere before assessing a state (dus at the - beginning of iterate), immediately reduce to 'sk(Eve)'. Test with - --experimental. To that end, reintroduce a state-reporting switch. -- It is currently not well-defined to define inversekeys within a role: - this requires some work at instantiation, because instantiated term - couples should be added to the inverses list, and removed at - descruction. -- Simple timestamps could be added by prefixing send message before the - role, sending any timestamp constants out first to the intruder. These - should of course be hidden in the output somehow. -- Notes on the new attack group displays: - * We want to group runs into consistent protocol runs. - * Minimal req. for protocol run: equal \rho. - * If two runs are candidates for a role in a protocol run, - use a metric based on order and data. Maybe data is more important: - if equal data, than order might be irrelevant. - * Maybe we should refactor the xmlOut code first. In an extreme case, - we first factor out all logic, and ranking, and grouping, in to a - prepareAttackOutput structure; with a separate source file. Later we - can convert this to either ASCII or DOT or XML or something. - Now that I think of it; XML should be a plain state probably, and we - could add a switch to also output more detailed attack things (is - that relevant?) -- SConstruct file should check whether ctags actually exists (avoiding - errors) -- Proof output should be XML, with an external converter to dot format.