From 02041cfbab855b196c189b712fb9654013493f61 Mon Sep 17 00:00:00 2001 From: ccremers Date: Mon, 30 Aug 2004 13:57:16 +0000 Subject: [PATCH] - Fixed binding displays. - Improved attack dot output. - goal_graph_create now takes originator assumption into account. --- src/arachne.c | 65 ++++++++++++-------------- src/binding.c | 124 ++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 154 insertions(+), 35 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 965e4cc..4c0442a 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -523,6 +523,9 @@ bind_existing_to_goal (const Binding b, const int run, const int index) found++; flag = 1; + /** + * Now create the new bindings + */ if (goal_bind (b, run, index)) { int keycount; @@ -692,7 +695,7 @@ dotSemiState () // Open graph attack_number++; eprintf ("digraph semiState%i {\n", attack_number); - eprintf ("\tcomment = \"Protocol "); + eprintf ("\tlabel = \"Protocol "); p = (Protocol) current_claim->protocol; termPrint (p->nameterm); eprintf (", role "); @@ -717,10 +720,10 @@ dotSemiState () eprintf ("\tsubgraph cluster_run%i {\n", run); eprintf ("\t\tlabel = \""); - eprintf ("run #%i, protocol ", run); + eprintf ("#%i: ", run); termPrint (sys->runs[run].protocol->nameterm); - eprintf (", role "); - termPrint (sys->runs[run].role->nameterm); + eprintf (", "); + agentsOfRunPrint (sys, run); eprintf ("\";\n", run); if (run == 0) { @@ -738,7 +741,8 @@ dotSemiState () eprintf (" ["); if (run == 0 && index == current_claim->ev) { - eprintf ("shape=doubleoctagon,"); + eprintf + ("style=filled,fillcolor=mistyrose,color=salmon,shape=doubleoctagon,"); } else { @@ -757,6 +761,7 @@ dotSemiState () node (run, index - 1); eprintf (" -> "); node (run, index); + eprintf (" [style=\"bold\", weight=\"2.0\"]"); eprintf (";\n"); } else @@ -798,9 +803,9 @@ dotSemiState () { // Sends first. // Show this explicitly in the graph by adding a prefix start node - eprintf - ("\t\ts%i [label=\"Agent start\", shape=diamond];\n", - run); + eprintf ("\t\ts%i [label=\"Start ", run); + agentsOfRunPrint (sys, run); + eprintf ("\", shape=diamond];\n"); eprintf ("\t\ts%i -> ", run); node (run, index); eprintf (";\n"); @@ -843,18 +848,24 @@ dotSemiState () { // Is this run before the event? int ev2; + int ev2_found; int found; found = 0; - ev2 = sys->runs[run2].length - 1; - while ((ev2 >= 0) && (found == 0)) + ev2 = 0; + ev2_found = 0; + while (ev2 < sys->runs[run2].length) { if (graph[graph_nodes (nodes, run2, ev2, run, ev)] != 0) - found = 1; - else - ev2--; + { + found = 1; + ev2_found = ev2; + } + ev2++; } + ev2 = ev2_found; + if (found == 1) { // It is before the event, and thus we would like to draw it. @@ -863,20 +874,22 @@ dotSemiState () * Note that this algorithm is similar to Floyd's algorithm for all shortest paths. * The goal here is to select only the path with distance 1 (as viewed from the regular runs), * so we can simplify stuff a bit. + * Nevertheless, using Floyd first would probably be faster. */ int run3; int other_route; other_route = 0; run3 = 0; - while (run3 < sys->maxruns) + while (other_route == 0 && run3 < sys->maxruns) { if (sys->runs[run3].protocol != INTRUDER) { int ev3; ev3 = 0; - while (ev3 < sys->runs[run3].length) + while (other_route == 0 + && ev3 < sys->runs[run3].length) { if (graph [graph_nodes @@ -888,38 +901,20 @@ dotSemiState () { // other route found other_route = 1; - // abort - ev3 = sys->runs[run3].length; - run3 = sys->maxruns; } ev3++; } } run3++; } - if (!other_route) + if (other_route == 0) { - eprintf ("\t\t"); + eprintf ("\t"); node (run2, ev2); eprintf (" -> "); node (run, ev); eprintf (";\n"); } - else - { - eprintf ("\t\t"); - node (run2, ev2); - eprintf (" -> "); - node (run, ev); - eprintf (" [style=dotted];\n"); - } - } - else - { - // not found - eprintf ("\t\tNOPREV -> "); - node (run, ev); - eprintf (" [label=\"#%i\"];\n", run2); } } run2++; diff --git a/src/binding.c b/src/binding.c index 7b9b65f..9c671bb 100644 --- a/src/binding.c +++ b/src/binding.c @@ -155,6 +155,130 @@ goal_graph_create () } bl = bl->next; } + // Setup local constants order + run = 0; + while (run < sys->maxruns) + { + if (sys->runs[run].protocol != INTRUDER) + { + int run2; + + run2 = 0; + while (run2 < sys->maxruns) + { + if (sys->runs[run].protocol != INTRUDER && run != run2) + { + // For these two runs, we check whether run has any variables that are mapped + // to constants from run2 + Termlist tl; + + tl = sys->runs[run].locals; + while (tl != NULL) + { + Term t; + + t = tl->term; + if (t->type == VARIABLE && t->right.runid == run + && t->subst != NULL) + { + // t is a variable of run + Termlist tl2; + + tl2 = sys->runs[run2].locals; + while (tl2 != NULL) + { + Term t2; + + t2 = tl2->term; + if (realTermLeaf (t2) && t2->type != VARIABLE + && t2->right.runid == run2) + { + // t2 is a constant of run2 + if (isTermEqual (t, t2)) + { + // Indeed, run depends on the run2 constant t2. Thus we must store this order. + // The first send of t2 in run2 must be before the first (read) event in run with t2. + int ev2; + int done; + Roledef rd2; + + done = 0; + ev2 = 0; + rd2 = sys->runs[run2].start; + while (!done + && ev2 < sys->runs[run2].step) + { + if (rd2->type == SEND + && termSubTerm (rd2->message, + t2)) + { + // Allright, we send it here at ev2 first + int ev; + Roledef rd; + + ev = 0; + rd = sys->runs[run].start; + while (!done + && ev < + sys->runs[run].step) + { + if (termSubTerm + (rd->message, t2)) + { + // Term occurs here in run + if (rd->type == READ) + { + // It's read here first. + // Order and be done with it. + graph[graph_nodes + (nodes, run2, + ev2, run, + ev)] = 1; +#ifdef DEBUG + if (DEBUGL (5)) + { + eprintf + ("* [local originator] term "); + termPrint (t2); + eprintf + (" is bound using %i, %i before %i,%i\n", + run2, ev2, + run, ev); + } +#endif + done = 1; + } +#ifdef DEBUG + else + { + // It doesn't occur first in a READ, which shouldn't be happening + error + ("Term from run %i occurs in run %i before it is read?", + run2, run); + } +#endif + } + rd = rd->next; + ev++; + } + done = 1; + } + rd2 = rd2->next; + ev2++; + } + } + } + tl2 = tl2->next; + } + } + tl = tl->next; + } + } + run2++; + } + } + run++; + } }