- Revised dot output.

- Reintroduced intruder events.
  - Added colors.
This commit is contained in:
ccremers 2006-03-14 11:37:28 +00:00
parent f823399a73
commit 16a59624fe
5 changed files with 976 additions and 468 deletions

View File

@ -2065,22 +2065,27 @@ iterate ()
btup = select_tuple_goal (); btup = select_tuple_goal ();
if (btup != NULL) if (btup != NULL)
{ {
// Expand tuple goal /* Substitution or something resulted in a tuple goal: we immediately split them into compounds.
*/
int count; int count;
Term tupletermbuffer;
// mark as blocked for iteration tupletermbuffer = btup->term;
binding_block (btup);
// simply adding will detect the tuple and add the new subgoals /*
* We solve this by replacing the tuple goal by the left term, and adding a goal for the right term.
*/
btup->term = TermOp1 (tupletermbuffer);
count = count =
goal_add (btup->term, btup->run_to, btup->ev_to, goal_add (TermOp2 (tupletermbuffer), btup->run_to,
btup->level); btup->ev_to, btup->level);
// Show this in output // Show this in output
if (switches.output == PROOF) if (switches.output == PROOF)
{ {
indentPrint (); indentPrint ();
eprintf ("Expanding tuple goal "); eprintf ("Expanding tuple goal ");
termPrint (btup->term); termPrint (tupletermbuffer);
eprintf (" into %i subgoals.\n", count); eprintf (" into %i subgoals.\n", count);
} }
@ -2089,7 +2094,7 @@ iterate ()
// undo // undo
goal_remove_last (count); goal_remove_last (count);
binding_unblock (btup); btup->term = tupletermbuffer;
} }
else else
{ {

View File

@ -361,7 +361,7 @@ valid_binding (Binding b)
return false; return false;
} }
//! Iterate over valid bindings //! Iterate over all bindings
/** /**
* Iterator should return true to proceed * Iterator should return true to proceed
*/ */
@ -375,14 +375,10 @@ iterate_bindings (int (*func) (Binding b))
Binding b; Binding b;
b = (Binding) bl->data; b = (Binding) bl->data;
if (valid_binding (b)) if (!func (b))
{ {
if (!func (b)) return false;
{
return false;
}
} }
} }
return true; return true;
} }

View File

@ -816,10 +816,12 @@ roleCompile (Term nameterm, Tac tc)
* in which case we assume that the agent names are possibly received as variables * in which case we assume that the agent names are possibly received as variables
*/ */
thisRole->initiator = 0; thisRole->initiator = 0;
firstEvent = 0;
} }
commEvent (READ, tc); commEvent (READ, tc);
break; break;
case TAC_SEND: case TAC_SEND:
firstEvent = 0;
commEvent (SEND, tc); commEvent (SEND, tc);
break; break;
case TAC_CLAIM: case TAC_CLAIM:
@ -836,7 +838,6 @@ roleCompile (Term nameterm, Tac tc)
} }
break; break;
} }
firstEvent = 0;
tc = tc->next; tc = tc->next;
} }
} }

File diff suppressed because it is too large Load Diff

View File

@ -1,12 +1,11 @@
- If no attack/state output is needed, maybe the attack heuristic should
be simpler (which means just weighting the trace length etc.) in order
to avoid uneccesary continuation of the search. Maybe even stop
altogether after finding *an* attack.
- For the TimeStamps etc, we can implement an 'auto-leak' of such local - For the TimeStamps etc, we can implement an 'auto-leak' of such local
constants. This should works also with a modifier of sorts (e.g. constants. This should works also with a modifier of sorts (e.g.
'predictable') and such constants should be leaked to the intruder at 'predictable') and such constants should be leaked to the intruder at
the start of the run, possibly by prefixing a send. the start of the run, possibly by prefixing a send.
- best heuristic currently for -t8: ignore sendsfirst, just look at the
previous event and continue at that run.
- termPrint must currently be encapsulated in a math environment to work in
latex output, I wil change this later to some ensure mathmode construct,
probably with something like latexTermPrint.
- The trace incremental search should start at something like 'distance of - The trace incremental search should start at something like 'distance of
first claim + SOMECONST * runs'. SOMECONST relates to the partial-order first claim + SOMECONST * runs'. SOMECONST relates to the partial-order
induced trace prolonings. induced trace prolonings.
@ -14,35 +13,6 @@
- Because the properties checked are related to the partial order reductions, - Because the properties checked are related to the partial order reductions,
it makes sense to check 'all secrecy claims' or 'all synchronisation claims' it makes sense to check 'all secrecy claims' or 'all synchronisation claims'
at once. at once.
- Once an attack is generated, we know the actual scenario and the trace
length. We might re-use this information to generate the shortest attack
using no partial order reduction. Note that choosing a wise method of
finding that is a mathematical issue: searching -t1 is exponential, so how
do we step trough these traces in order to find the shortest trace in the
quickest way? This can be determined under some (statistical) assumptions.
- The incremental check can be done much easier, by just retrying the main
loop explore with different parameters. It keeps everything nicely intact.
We must check for fails however, and how pruning is affected.
- Incremental check can at least be done in two ways: either by limiting the
number of runs (big axe method) or by limiting the trace length (nice).
There is a drawback to trace length only: the superfluous sends of the
algorithm in a scenario with many runs might interfere with the usefulness
of short traces. Maybe some heuristic that reduces the runs automatically is
required. (e.g. 'number of runs is at most MaxTraceLength/MaxRoleLength' or
something like that). Do analysis.
- If synch checking is expensive, introduce a limit (for -p0 stuff).
Basically, after the limit (if -p0 is set), we stop checking synch claims.
This then is default behaviour, to be overridden or changed by a switch.
- clp does not yet consider the matching for variables that have not been
instantiated. This *might* lead to some improvement, e.g. when there is only
one candidate for the variable. In general, I don't think it will help.
- match_clp.c 1.25 introduced the variable_in_invkey brancher, which hasn't
been thoroughly tested yet. Please do test.
- Brutus is slower than -t4. CLP is much, much faster however than both.
- It is very important to have variables in the run agent list, because it
dramatically decreases the complexity of the system, as opposed to just
creating runs for all possibilities. However, this explicitly introduces the
clp problem of var encryptions (see above).
- Given originator assumptions and such, we might want to implement the - Given originator assumptions and such, we might want to implement the
compiler, that for non-typed matching, it will ignore all type definitions compiler, that for non-typed matching, it will ignore all type definitions
in the code (as in, putting them in stype, but still considering Function). in the code (as in, putting them in stype, but still considering Function).