diff --git a/src/arachne.c b/src/arachne.c index d97bd81..f5ed91f 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -2065,22 +2065,27 @@ iterate () btup = select_tuple_goal (); if (btup != NULL) { - // Expand tuple goal + /* Substitution or something resulted in a tuple goal: we immediately split them into compounds. + */ int count; + Term tupletermbuffer; - // mark as blocked for iteration - binding_block (btup); - // simply adding will detect the tuple and add the new subgoals + tupletermbuffer = btup->term; + + /* + * 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 = - goal_add (btup->term, btup->run_to, btup->ev_to, - btup->level); + goal_add (TermOp2 (tupletermbuffer), btup->run_to, + btup->ev_to, btup->level); // Show this in output if (switches.output == PROOF) { indentPrint (); eprintf ("Expanding tuple goal "); - termPrint (btup->term); + termPrint (tupletermbuffer); eprintf (" into %i subgoals.\n", count); } @@ -2089,7 +2094,7 @@ iterate () // undo goal_remove_last (count); - binding_unblock (btup); + btup->term = tupletermbuffer; } else { diff --git a/src/binding.c b/src/binding.c index fe80f3b..5509c41 100644 --- a/src/binding.c +++ b/src/binding.c @@ -361,7 +361,7 @@ valid_binding (Binding b) return false; } -//! Iterate over valid bindings +//! Iterate over all bindings /** * Iterator should return true to proceed */ @@ -375,14 +375,10 @@ iterate_bindings (int (*func) (Binding b)) Binding b; b = (Binding) bl->data; - if (valid_binding (b)) + if (!func (b)) { - if (!func (b)) - { - return false; - } + return false; } - } return true; } diff --git a/src/compiler.c b/src/compiler.c index a8e7581..fe2fcea 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -816,10 +816,12 @@ roleCompile (Term nameterm, Tac tc) * in which case we assume that the agent names are possibly received as variables */ thisRole->initiator = 0; + firstEvent = 0; } commEvent (READ, tc); break; case TAC_SEND: + firstEvent = 0; commEvent (SEND, tc); break; case TAC_CLAIM: @@ -836,7 +838,6 @@ roleCompile (Term nameterm, Tac tc) } break; } - firstEvent = 0; tc = tc->next; } } diff --git a/src/dotout.c b/src/dotout.c index 3ff423e..ff84961 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -17,6 +17,46 @@ extern Role I_RRSD; #define length step +#define CLAIMTEXTCOLOR "#ffffff" +#define CLAIMCOLOR "#000000" +#define GOODCOMMCOLOR "forestgreen" + +#define INTRUDERCOLORH 18.0 +#define INTRUDERCOLORL 0.65 +#define INTRUDERCOLORS 0.9 +#define RUNCOLORL1 0.90 +#define RUNCOLORL2 0.65 +#define RUNCOLORH1 (INTRUDERCOLORH + 360 - 10.0) +#define RUNCOLORH2 (INTRUDERCOLORH + 10.0) +#define RUNCOLORS1 0.8 +#define RUNCOLORS2 0.6 +#define RUNCOLORDELTA 0.2 // maximum hue delta between roles (0.2): smaller means role colors of a protocol become more similar. +#define RUNCOLORCONTRACT 0.8 // contract from protocol edges: smaller means more distinction between protocols. +#define UNTRUSTEDCOLORS 0.4 + +/* + * Dot output + * + * + * The algorithm itself is not very complicated; because the semi-bundles have + * bindings etcetera, a graph can be draw quickly and efficiently. + * + * Interesting issues: + * + * Binding annotations are only drawn if they don't connect with regular + * events, and when the item does not occur in any previous binding, it might + * be connected to the initial intruder knowledge. + * + * Color management is quite involved. We draw identical protocols in similar + * color schemes. A color scheme is a gradient between two colors, evenly + * spread over all the runs. + */ + + +/* + * code + */ + //! Draw node void node (const System sys, const int run, const int index) @@ -25,11 +65,11 @@ node (const System sys, const int run, const int index) { if (sys->runs[run].role == I_M) { - eprintf ("m0"); + eprintf ("intruder"); } else { - eprintf ("i%i", run); + eprintf ("ri%i", run); } } else @@ -38,6 +78,331 @@ node (const System sys, const int run, const int index) } } +//! Draw arrow +void +arrow (const System sys, Binding b) +{ + node (sys, b->run_from, b->ev_from); + eprintf (" -> "); + node (sys, b->run_to, b->ev_to); +} + +//! Redirect node +void +redirNode (const System sys, Binding b) +{ + eprintf ("redir_"); + node (sys, b->run_from, b->ev_from); + node (sys, b->run_to, b->ev_to); +} + +//! Roledef draw +void +roledefDraw (Roledef rd) +{ + void optlabel (void) + { + Term label; + + label = rd->label; + if (label != NULL) + { + if (realTermTuple (label)) + { + label = TermOp2 (label); + } + eprintf ("_"); + termPrint (label); + } + } + + if (rd->type == READ) + { + eprintf ("read"); + optlabel (); + eprintf (" from "); + termPrint (rd->from); + eprintf ("\\n"); + termPrint (rd->message); + } + if (rd->type == SEND) + { + eprintf ("send"); + optlabel (); + eprintf (" to "); + termPrint (rd->to); + eprintf ("\\n"); + termPrint (rd->message); + } + if (rd->type == CLAIM) + { + eprintf ("claim"); + optlabel (); + eprintf ("\\n"); + termPrint (rd->to); + if (rd->message != NULL) + { + eprintf (" : "); + termPrint (rd->message); + } + } +} + +//! Choose term node +void +chooseTermNode (const Term t) +{ + eprintf ("CHOOSE"); + { + char *rsbuf; + + rsbuf = RUNSEP; + RUNSEP = "x"; + termPrint (t); + RUNSEP = rsbuf; + } +} + +//! Value for hlsrgb conversion +static double +hlsValue (double n1, double n2, double hue) +{ + if (hue > 360.0) + hue -= 360.0; + else if (hue < 0.0) + hue += 360.0; + if (hue < 60.0) + return n1 + (n2 - n1) * hue / 60.0; + else if (hue < 180.0) + return n2; + else if (hue < 240.0) + return n1 + (n2 - n1) * (240.0 - hue) / 60.0; + else + return n1; +} + +//! hls to rgb conversion +void +hlsrgb (int *r, int *g, int *b, double h, double l, double s) +{ + double m1, m2; + + int bytedouble (double d) + { + double x; + + x = 255.0 * d; + if (x <= 0) + return 0; + else if (x >= 255.0) + return 255; + else + return (int) x; + } + + while (h >= 360.0) + h -= 360.0; + while (h < 0) + h += 360.0; + m2 = (l <= 0.5) ? (l * (l + s)) : (l + s - l * s); + m1 = 2.0 * l - m2; + if (s == 0.0) + { + *r = *g = *b = bytedouble (l); + } + else + { + *r = bytedouble (hlsValue (m1, m2, h + 120.0)); + *g = bytedouble (hlsValue (m1, m2, h)); + *b = bytedouble (hlsValue (m1, m2, h - 120.0)); + } +} + +//! print color from h,l,s triplet +void +printColor (double h, double l, double s) +{ + int r, g, b; + + hlsrgb (&r, &g, &b, h, l, s); + eprintf ("#%02x%02x%02x", r, g, b); +} + + +//! Set local buffer with the correct color for this run. +/** + * Determines number of protocols, shifts to the right color pair, and colors + * the run within the current protocol in the fade between the color pair. + * + * This can be done much more efficiently by computing these colors once, + * instead of each time again for each run. However, this is not a + * speed-critical section so this will do just nicely. + */ +void +setRunColorBuf (const System sys, int run, char *colorbuf) +{ + int range; + int index; + double protoffset, protrange; + double roleoffset, roledelta; + double color; + double h, l, s; + int r, g, b; + + // help function: contract roleoffset, roledelta with a factor (<= 1.0) + void contract (double factor) + { + roledelta = roledelta * factor; + roleoffset = (roleoffset * factor) + ((1.0 - factor) / 2.0); + } + + // determine #protocol, resulting in two colors + { + Termlist protocols; + Term refprot; + int r; + int firstfound; + + protocols = NULL; + refprot = sys->runs[run].protocol->nameterm; + index = 0; + range = 1; + firstfound = false; + for (r = 0; r < sys->maxruns; r++) + { + if (sys->runs[r].protocol != INTRUDER) + { + Term prot; + + prot = sys->runs[r].protocol->nameterm; + if (!isTermEqual (prot, refprot)) + { + // Some 'other' protocol + if (!inTermlist (protocols, prot)) + { + // New other protocol + protocols = termlistAdd (protocols, prot); + range++; + if (!firstfound) + { + index++; + } + } + } + else + { + // Our protocol + firstfound = true; + } + } + } + termlistDelete (protocols); + } + + // Compute protocol offset [0.0 ... 1.0> + protrange = 1.0 / range; + protoffset = index * protrange; + + // We now now our range, and we can determine which role this one is. + { + Role rr; + int done; + + range = 0; + index = 0; + done = false; + + for (rr = sys->runs[run].protocol->roles; rr != NULL; rr = rr->next) + { + if (sys->runs[run].role == rr) + { + done = true; + } + else + { + if (!done) + { + index++; + } + } + range++; + } + } + + // Compute role offset [0.0 ... 1.0] + if (range <= 1) + { + roledelta = 0.0; + roleoffset = 0.5; + } + else + { + // range over 0..1 + roledelta = 1.0 / (range - 1); + roleoffset = index * roledelta; + // Now this can result in a delta that is too high (depending on protocolrange) + if (protrange * roledelta > RUNCOLORDELTA) + { + contract (RUNCOLORDELTA / (protrange * roledelta)); + } + } + + // We slightly contract the colors (taking them away from protocol edges) + contract (RUNCOLORCONTRACT); + + // Now we can convert this to a color + color = protoffset + (protrange * roleoffset); + h = RUNCOLORH1 + color * (RUNCOLORH2 - RUNCOLORH1); + l = RUNCOLORL1 + color * (RUNCOLORL2 - RUNCOLORL1); + s = RUNCOLORS1 + color * (RUNCOLORS2 - RUNCOLORS1); + + // If the run is not trusted, we lower the saturation significantly + if (!isRunTrusted (sys, run)) + { + s = UNTRUSTEDCOLORS; + } + + // set to buffer + hlsrgb (&r, &g, &b, h, l, s); + sprintf (colorbuf, "#%02x%02x%02x", r, g, b); + + // compute second color (light version) + /* + l += 0.07; + if (l > 1.0) + l = 1.0; + */ + hlsrgb (&r, &g, &b, h, l, s); + sprintf (colorbuf + 8, "#%02x%02x%02x", r, g, b); +} + +//! Communication status +int +isCommunicationExact (const System sys, Binding b) +{ + Roledef rd1, rd2; + + rd1 = eventRoledef (sys, b->run_from, b->ev_from); + rd2 = eventRoledef (sys, b->run_to, b->ev_to); + + if (!isTermEqual (rd1->message, rd2->message)) + { + return false; + } + if (!isTermEqual (rd1->from, rd2->from)) + { + return false; + } + if (!isTermEqual (rd1->to, rd2->to)) + { + return false; + } + if (!isTermEqual (rd1->label, rd2->label)) + { + return false; + } + return true; +} //! Determine ranks for all nodes /** @@ -136,395 +501,552 @@ iterate_first_regular_occurrences (const System sys, return true; } -//! Iterate over all events that have an incoming arrow to the current one (forgetting the intruder for a moment) +//! Draw a class choice +/** + * \rho classes are already dealt with in the headers, so we should ignore them. + */ void -iterate_incoming_arrows (const System sys, void (*func) (), const int run, - const int ev) +drawClass (const System sys, Binding b) { - /** - * Determine wheter to draw an incoming arrow to this event. - * We check all other runs, to see if they are ordered. - */ - int run2; + Term varterm; - run2 = 0; - while (run2 < sys->maxruns) + // now check in previous things whether we saw that term already + int notSameTerm (Binding b2) + { + return (!isTermEqual (varterm, b2->term)); + } + + varterm = deVar (b->term); + + // Variable? + if (!isTermVariable (varterm)) { - if (run2 != run && sys->runs[run2].protocol != INTRUDER) - { - // Is this run before the event? - int ev2; - int found; - - found = 0; - ev2 = sys->runs[run2].length; - while (found == 0 && ev2 > 0) - { - ev2--; - if (isDependEvent (run2, ev2, run, ev)) - { - found = 1; - } - } - - if (found == 1) - { - // It is before the event, and thus we would like to draw it. - // However, if there is another path along which we can get here, forget it - /** - * 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 other_route; - int run3; - int ev3; - - other_route = 0; - run3 = 0; - ev3 = 0; - while (other_route == 0 && run3 < sys->maxruns) - { - if (sys->runs[run3].protocol != INTRUDER) - { - ev3 = 0; - while (other_route == 0 && ev3 < sys->runs[run3].length) - { - if (isDependEvent (run2, ev2, run3, ev3) - && isDependEvent (run3, ev3, run, ev)) - { - // other route found - other_route = 1; - } - ev3++; - } - } - run3++; - } - if (other_route == 0) - { - func (run2, ev2); - } - - - } - } - run2++; + return; } + + // Agent variable? + { + int run; + + run = TermRunid (varterm); + if ((run >= 0) && (run < sys->maxruns)) + { + if (inTermlist (sys->runs[run].agents, varterm)) + { + return; + } + } + } + + // Seen before? + if (!iterate_preceding_bindings (b->run_to, b->ev_to, notSameTerm)) + { + // We saw the same term before. Exit. + return; + } + + + + + // not seen before: choose class + eprintf ("\t"); + chooseTermNode (varterm); + eprintf (" [label=\"Class:\\nAny "); + termPrint (varterm); + eprintf ("\"];\n"); + eprintf ("\t"); + chooseTermNode (varterm); + eprintf (" -> "); + node (sys, b->run_to, b->ev_to); + eprintf (" [weight=\"2.0\",arrowhead=\"none\",style=\"dotted\"];\n"); } -//! Iterate over all events that have an outgoing arrow from the current one (forgetting the intruder for a moment) +//! Draw a single binding void -iterate_outgoing_arrows (const System sys, void (*func) (), const int run, - const int ev) +drawBinding (const System sys, Binding b) { - /** - * Determine wheter to draw an incoming arrow to this event. - * We check all other runs, to see if they are ordered. - */ - int run2; + int intr_to, intr_from; - run2 = 0; - while (run2 < sys->maxruns) + intr_from = (sys->runs[b->run_from].protocol == INTRUDER); + intr_to = (sys->runs[b->run_to].protocol == INTRUDER); + + if (intr_from) { - if (run2 != run && sys->runs[run2].protocol != INTRUDER) + // from intruder + /* + * Because this can be generated many times, it seems + * reasonable to not duplicate such arrows, especially when + * they're from M_0. Maybe the others are still relevant. + */ + if (1 == 1 || sys->runs[b->run_from].role == I_M) { - // Is this run after the event? - int ev2; - int found; + // now check in previous things whether we saw that term already + int notSameTerm (Binding b2) + { + return (!isTermEqual (b->term, b2->term)); + } - found = 0; - ev2 = 0; - while (found == 0 && ev2 < sys->runs[run2].length) + if (!iterate_preceding_bindings (b->run_to, b->ev_to, notSameTerm)) { - if (isDependEvent (run, ev, run2, ev2)) - { - found = 1; - } - else - { - ev2++; - } - } - - if (found == 1) - { - // It is after the event, and thus we would like to draw it. - // However, if there is another path along which we can get there, forget it - /** - * 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 other_route; - int run3; - int ev3; - - other_route = 0; - run3 = 0; - ev3 = 0; - while (other_route == 0 && run3 < sys->maxruns) - { - if (sys->runs[run3].protocol != INTRUDER) - { - ev3 = 0; - while (other_route == 0 && ev3 < sys->runs[run3].length) - { - if (isDependEvent (run, ev, run3, ev3) - && isDependEvent (run3, ev3, run2, ev2)) - { - // other route found - other_route = 1; - } - ev3++; - } - } - run3++; - } - if (other_route == 0) - { - func (run2, ev2); - } + // We saw the same term before. Exit. + return; } } - run2++; - } -} - -//! Draw the dependencies (returns from_intruder_count) -int -drawBindings (const System sys) -{ - int run; - int from_intruder_count; - - // We now determine them ourselves between existing runs - run = 0; - from_intruder_count = 0; - while (run < sys->maxruns) - { - if (sys->runs[run].protocol != INTRUDER) + // normal from intruder (not M0) + if (intr_to) { - int ev; - - ev = 0; - while (ev < sys->runs[run].length) - { - int incoming_arrow_count; - - void incoming_arrow (int run2, int ev2) - { - Roledef rd, rd2; - - incoming_arrow_count++; - /* - * We have decided to draw this binding, - * from run2,ev2 to run,ev - * However, me might need to decide some colouring for this node. - */ - eprintf ("\t"); - node (sys, run2, ev2); - eprintf (" -> "); - node (sys, run, ev); - eprintf (" "); - // decide color - rd = roledef_shift (sys->runs[run].start, ev); - rd2 = roledef_shift (sys->runs[run2].start, ev2); - if (rd->type == CLAIM) - { - // Towards a claim, so only indirect dependency - eprintf ("[color=cornflowerblue]"); - } - else - { - // Not towards claim should imply towards read, - // but we check it to comply with future stuff. - if (rd->type == READ && rd2->type == SEND) - { - // We want to distinguish where it is from a 'broken' send - if (isTermEqual (rd->message, rd2->message)) - { - if (isTermEqual - (rd->from, rd2->from) - && isTermEqual (rd->to, rd2->to)) - { - // Wow, a perfect match. Leave the arrow as-is :) - eprintf ("[color=darkgreen]"); - } - else - { - // Same message, different people - eprintf - ("[label=\"redirect\",color=darkorange2]"); - } - } - else - { - // Not even the same message, intruder construction - eprintf ("[label=\"construct\",color=red]"); - } - } - } - // close up - eprintf (";\n"); - } - - incoming_arrow_count = 0; - iterate_incoming_arrows (sys, incoming_arrow, run, ev); - - ev++; - } + // intr->intr + eprintf ("\t"); + arrow (sys, b); + eprintf (" [label=\""); + termPrint (b->term); + eprintf ("\"]"); + eprintf (";\n"); } - run++; - } - return from_intruder_count; -} - - -//! Draw simple runs -void -drawSimpleRuns (const System sys) -{ - int run; - - // Draw graph - // First, all simple runs - run = 0; - while (run < sys->maxruns) - { - Roledef rd; - int index; - - index = 0; - rd = sys->runs[run].start; - if (sys->runs[run].protocol != INTRUDER && sys->runs[run].length > 0) + else { - // Regular run - - /* DISABLED subgraphs - eprintf ("\tsubgraph cluster_run%i {\n", run); - eprintf ("\t\tlabel = \""); - eprintf ("#%i: ", run); - termPrint (sys->runs[run].protocol->nameterm); - eprintf (", "); - agentsOfRunPrint (sys, run); - eprintf ("\";\n", run); - if (run == 0) - { - eprintf ("\t\tcolor = red;\n"); - } - else - { - eprintf ("\t\tcolor = blue;\n"); - } + // intr->regular + eprintf ("\t"); + arrow (sys, b); + eprintf (";\n"); + } + } + else + { + // not from intruder + if (intr_to) + { + // regular->intr + eprintf ("\t"); + arrow (sys, b); + eprintf (";\n"); + } + else + { + // regular->regular + /* + * Has this been done *exactly* as we hoped? */ - - - // Display the respective events - while (index < sys->runs[run].length) + if (isCommunicationExact (sys, b)) { - // Print node itself - eprintf ("\t\t"); - node (sys, run, index); - eprintf (" ["); - if (run == 0 && index == sys->current_claim->ev) + eprintf ("\t"); + arrow (sys, b); + eprintf (" [style=bold,color=\"%s\"]", GOODCOMMCOLOR); + eprintf (";\n"); + } + else + { + // Something was changed, so we call this a redirect + eprintf ("\t"); + node (sys, b->run_from, b->ev_from); + eprintf (" -> "); + redirNode (sys, b); + eprintf (" -> "); + node (sys, b->run_to, b->ev_to); + eprintf (";\n"); + + eprintf ("\t"); + redirNode (sys, b); + eprintf (" [style=filled,fillcolor=\""); + printColor (INTRUDERCOLORH, INTRUDERCOLORL, INTRUDERCOLORS); + eprintf ("\",label=\"redirect"); + if (!isTermEqual + (eventRoledef (sys, b->run_from, b->ev_from)->message, + b->term)) { - eprintf - ("style=filled,fillcolor=mistyrose,color=salmon,shape=doubleoctagon,"); + // Only explicitly mention redirect term when it differs from the sent term + eprintf ("\\n"); + termPrint (b->term); } - else - { - eprintf ("shape=box,"); - } - eprintf ("label=\""); - roledefPrintShort (rd); eprintf ("\"]"); eprintf (";\n"); - // Print binding to previous node - if (index > sys->runs[run].firstReal) - { - // index > 0 - eprintf ("\t\t"); - node (sys, run, index - 1); - eprintf (" -> "); - node (sys, run, index); - eprintf (" [style=\"bold\", weight=\"10.0\"]"); - eprintf (";\n"); - } - else - { - // index <= firstReal - if (index == sys->runs[run].firstReal) - { - // index == firstReal - Roledef rd; - int send_before_read; - int done; - - // Determine if it is an active role or note - /** - *@todo note that this will probably become a standard function call for role.h - */ - rd = - roledef_shift (sys->runs[run].start, - sys->runs[run].firstReal); - done = 0; - send_before_read = 0; - while (!done && rd != NULL) - { - if (rd->type == READ) - { - done = 1; - } - if (rd->type == SEND) - { - done = 1; - send_before_read = 1; - } - rd = rd->next; - } - // Draw the first box - // This used to be drawn only if done && send_before_read, now we always draw it. - eprintf ("\t\ts%i [label=\"Run %i: ", run, run); - termPrint (sys->runs[run].protocol->nameterm); - eprintf (", "); - termPrint (sys->runs[run].role->nameterm); - eprintf ("\\n"); - agentsOfRunPrint (sys, run); - eprintf ("\", shape=diamond];\n"); - eprintf ("\t\ts%i -> ", run); - node (sys, run, index); - eprintf (" [weight=\"10.0\"];\n"); - } - } - index++; - rd = rd->next; } - /* DISABLED subgraphs - eprintf ("\t}\n"); - */ } - run++; } } -//! Choose term node -void -chooseTermNode (const Term t) +//! Draw dependecies (including intruder!) +/** + * Returns from_intruder_count + */ +int +drawAllBindings (const System sys) { - eprintf ("CHOOSE"); - { - char *rsbuf; + List bl; + int fromintr; - rsbuf = RUNSEP; - RUNSEP = "x"; - termPrint (t); - RUNSEP = rsbuf; - } + fromintr = 0; + for (bl = sys->bindings; bl != NULL; bl = bl->next) + { + Binding b; + + b = (Binding) bl->data; + if (!b->blocked) + { + // if the binding is not done (class choice) we might + // still show it somewhere. + if (b->done) + { + // done, draw + drawBinding (sys, b); + // from intruder? + if (sys->runs[b->run_from].protocol == INTRUDER) + { + fromintr++; + } + } + else + { + drawClass (sys, b); + } + } + } + return fromintr; +} + +//! Nicely format the role and agents we think we're talking to. +void +agentsOfRunPrintOthers (const System sys, const int run) +{ + Term role = sys->runs[run].role->nameterm; + Termlist roles = sys->runs[run].protocol->rolenames; + + while (roles != NULL) + { + if (!isTermEqual (role, roles->term)) + { + Term agent; + + termPrint (roles->term); + eprintf (" is "); + agent = agentOfRunRole (sys, run, roles->term); + if (isTermVariable (agent)) + { + eprintf ("any "); + } + termPrint (agent); + eprintf ("\\l"); + } + roles = roles->next; + } +} + + + +//! Draw regular runs +void +drawRegularRuns (const System sys) +{ + int run; + int rcnum; + char *colorbuf; + + // two buffers, eight chars each + colorbuf = malloc (16 * sizeof (char)); + + rcnum = 0; + for (run = 0; run < sys->maxruns; run++) + { + if (sys->runs[run].length > 0) + { + if (sys->runs[run].protocol != INTRUDER) + { + Roledef rd; + int index; + int prevnode; + + prevnode = 0; + index = 0; + rd = sys->runs[run].start; + // Regular run + + /* + eprintf ("\tsubgraph cluster_run%i {\n", run); + eprintf ("\t\tlabel = \""); + eprintf ("#%i: ", run); + termPrint (sys->runs[run].protocol->nameterm); + eprintf (", "); + agentsOfRunPrint (sys, run); + eprintf ("\\nTesting the second line\";\n", run); + if (run == 0) + { + eprintf ("\t\tcolor = red;\n"); + } + else + { + eprintf ("\t\tcolor = blue;\n"); + } + */ + + // set color + setRunColorBuf (sys, run, colorbuf); + + // Display the respective events + while (index < sys->runs[run].length) + { + int showthis; + + showthis = true; + if (rd->type == CLAIM) + { + if (run != 0) + { + showthis = false; + } + else + { + if (index != sys->current_claim->ev) + { + showthis = false; + } + } + } + if (showthis) + { + // Print node itself + eprintf ("\t\t"); + node (sys, run, index); + eprintf (" ["); + if (run == 0 && index == sys->current_claim->ev) + { + // The claim under scrutiny + eprintf + ("style=filled,fontcolor=\"%s\",fillcolor=\"%s\",shape=box,", + CLAIMTEXTCOLOR, CLAIMCOLOR); + } + else + { + eprintf ("shape=box,style=filled,"); + // print color of this run + eprintf ("fillcolor=\"%s\",", colorbuf); + } + eprintf ("label=\""); + //roledefPrintShort (rd); + roledefDraw (rd); + eprintf ("\"]"); + eprintf (";\n"); + + // Print binding to previous node + if (index > sys->runs[run].firstReal) + { + // index > 0 + eprintf ("\t\t"); + node (sys, run, prevnode); + eprintf (" -> "); + node (sys, run, index); + eprintf (" [style=\"bold\", weight=\"10.0\"]"); + eprintf (";\n"); + prevnode = index; + } + else + { + // index <= firstReal + if (index == sys->runs[run].firstReal) + { + // index == firstReal + Roledef rd; + int send_before_read; + int done; + + // Determine if it is an active role or note + /** + *@todo note that this will probably become a standard function call for role.h + */ + rd = + roledef_shift (sys->runs[run].start, + sys->runs[run].firstReal); + done = 0; + send_before_read = 0; + while (!done && rd != NULL) + { + if (rd->type == READ) + { + done = 1; + } + if (rd->type == SEND) + { + done = 1; + send_before_read = 1; + } + rd = rd->next; + } + // Draw the first box (HEADER) + // This used to be drawn only if done && send_before_read, now we always draw it. + eprintf ("\t\ts%i [label=\"{ ", run); + + // Print first line + { + Term rolename; + Term agentname; + + rolename = sys->runs[run].role->nameterm; + agentname = + agentOfRunRole (sys, run, rolename); + if (isTermVariable (agentname)) + { + eprintf ("Any "); + } + termPrint (agentname); + eprintf (" in role "); + termPrint (rolename); + eprintf ("\\l"); + } + + // Second line + // Possible protocol (if more than one) + { + int showprotocol; + Protocol p; + int morethanone; + + // Simple case: don't show + showprotocol = false; + + // Check whether the protocol spec has more than one + morethanone = false; + for (p = sys->protocols; p != NULL; + p = p->next) + { + if (p != INTRUDER) + { + if (p != sys->runs[run].protocol) + { + morethanone = true; + break; + } + } + } + + // More than one? + if (morethanone) + { + if (run == 0) + { + // If this is run 0 we report the protocol anyway, even is there is only a single one in the attack + showprotocol = true; + } + else + { + int r; + // For other runs we only report when there are multiple protocols + showprotocol = false; + for (r = 0; r < sys->maxruns; r++) + { + if (sys->runs[r].protocol != + INTRUDER) + { + if (sys->runs[r].protocol != + sys->runs[run].protocol) + { + showprotocol = true; + break; + } + } + } + } + } + + // Use the result + if (showprotocol) + { + eprintf ("Protocol "); + termPrint (sys->runs[run].protocol-> + nameterm); + eprintf ("\\l"); + } + } + eprintf ("Run #%i\\l", run); + + + // print the other agents + eprintf ("|"); + if (termlistLength (sys->runs[run].agents) > 1) + { + if (sys->runs[run].role->initiator) + { + eprintf ("Chooses:\\l"); + } + else + { + eprintf ("Assumes:\\l"); + } + agentsOfRunPrintOthers (sys, run); + } + + // close up + eprintf ("}\", shape=record"); + eprintf (",style=filled,fillcolor=\"%s\"", + colorbuf + 8); + eprintf ("];\n"); + eprintf ("\t\ts%i -> ", run); + node (sys, run, index); + eprintf (" [style=bold, weight=\"10.0\"];\n"); + prevnode = index; + } + } + } + index++; + rd = rd->next; + } + //eprintf ("\t}\n"); + + } + } + } + free (colorbuf); +} + +//! Draw intruder runs +void +drawIntruderRuns (const System sys) +{ + int run; + + /* + eprintf ("\tsubgraph intruder {\n"); + eprintf ("\t\tlabel = \"Intruder\\nTesting the seconds.\";\n"); + eprintf ("\t\tcolor = red;\n"); + */ + for (run = 0; run < sys->maxruns; run++) + { + if (sys->runs[run].length > 0) + { + if (sys->runs[run].protocol == INTRUDER) + { + // Intruder run + if (sys->runs[run].role != I_M) + { + // Not an M_0 run, so we can draw it. + eprintf ("\t\t"); + node (sys, run, 0); + eprintf (" [style=filled,fillcolor=\""); + printColor (INTRUDERCOLORH, INTRUDERCOLORL, INTRUDERCOLORS); + eprintf ("\","); + if (sys->runs[run].role == I_RRSD) + { + eprintf ("label=\"decrypt\""); + } + if (sys->runs[run].role == I_RRS) + { + // Distinguish function application + if (isTermFunctionName + (sys->runs[run].start->next->message)) + { + eprintf ("label=\"apply\""); + } + else + { + eprintf ("label=\"encrypt\""); + } + } + eprintf ("];\n"); + } + } + } + } + //eprintf ("\t}\n\n"); } //! Show intruder choices @@ -606,6 +1128,64 @@ drawIntruderChoices (const System sys) termlistDelete (shown); } +//! Ranking info +void +showRanks (const System sys, int maxrank, int *ranks) +{ + // Fourth, all ranking info + int myrank; + +#ifdef DEBUG + { + int n; + + eprintf ("/* ranks: %i\n", maxrank); + n = 0; + while (n < nodes) + { + eprintf ("%i ", ranks[n]); + n++; + } + eprintf ("\n*/\n\n"); + } +#endif + myrank = 0; + while (myrank < maxrank) + { + int count; + int run; + int run1; + int ev1; + + count = 0; + run = 0; + while (run < sys->maxruns) + { + if (sys->runs[run].protocol != INTRUDER) + { + int ev; + + ev = 0; + while (ev < sys->runs[run].step) + { + if (myrank == ranks[eventNode (run, ev)]) + { + if (count == 0) + eprintf ("\t{ rank = same; "); + count++; + eprintf ("r%ii%i; ", run, ev); + } + ev++; + } + } + run++; + } + if (count > 0) + eprintf ("}\t\t// rank %i\n", myrank); + myrank++; + } +} + //! Display the current semistate using dot output format. /** @@ -634,6 +1214,11 @@ dotSemiState (const System sys) termPrint (sys->current_claim->type); eprintf ("\";\n"); + // Globals + eprintf ("\tfontname=Helvetica;\n"); + eprintf ("\tnode [fontname=Helvetica];\n"); + eprintf ("\tedge [fontname=Helvetica];\n"); + // Needed for the bindings later on: create graph nodes = nodeCount (); @@ -697,17 +1282,20 @@ dotSemiState (const System sys) } #endif - // First, simple runs - drawSimpleRuns (sys); - // Second, all bindings. - from_intruder_count = drawBindings (sys); + // First, runs + drawRegularRuns (sys); + drawIntruderRuns (sys); + from_intruder_count = drawAllBindings (sys); // Third, the intruder node (if needed) if (from_intruder_count > 0) { eprintf - ("\tintruder [label=\"Initial intruder knowledge\", color=red];\n"); + ("\tintruder [label=\"Initial intruder knowledge\", style=filled,fillcolor=\""); + printColor (INTRUDERCOLORH, INTRUDERCOLORL, INTRUDERCOLORS); + eprintf ("\"];\n"); } + // eprintf ("\t};\n"); // For debugging we might add more stuff: full dependencies #ifdef DEBUG @@ -746,63 +1334,11 @@ dotSemiState (const System sys) } #endif - // Fourth, all ranking info - { - int myrank; - -#ifdef DEBUG - { - int n; - - eprintf ("/* ranks: %i\n", maxrank); - n = 0; - while (n < nodes) - { - eprintf ("%i ", ranks[n]); - n++; - } - eprintf ("\n*/\n\n"); - } -#endif - myrank = 0; - while (myrank < maxrank) - { - int count; - int run; - int run1; - int ev1; - - count = 0; - run = 0; - while (run < sys->maxruns) - { - if (sys->runs[run].protocol != INTRUDER) - { - int ev; - - ev = 0; - while (ev < sys->runs[run].step) - { - if (myrank == ranks[eventNode (run, ev)]) - { - if (count == 0) - eprintf ("\t{ rank = same; "); - count++; - eprintf ("r%ii%i; ", run, ev); - } - ev++; - } - } - run++; - } - if (count > 0) - eprintf ("}\t\t// rank %i\n", myrank); - myrank++; - } - } - // Intruder choices - drawIntruderChoices (sys); + //drawIntruderChoices (sys); + + // Ranks + //showRanks (sys, maxrank, ranks); #ifdef DEBUG // Debug: print dependencies diff --git a/src/notes.txt b/src/notes.txt index 0c350f1..fbf97fa 100644 --- a/src/notes.txt +++ b/src/notes.txt @@ -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 constants. This should works also with a modifier of sorts (e.g. 'predictable') and such constants should be leaked to the intruder at 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 first claim + SOMECONST * runs'. SOMECONST relates to the partial-order induced trace prolonings. @@ -14,35 +13,6 @@ - Because the properties checked are related to the partial order reductions, it makes sense to check 'all secrecy claims' or 'all synchronisation claims' 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 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).