From 341f519bbb8302b3efc9c2d869354d778fd37daa Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 18 Aug 2004 15:46:33 +0000 Subject: [PATCH] BROKEN - Works better all the time. Huge shift of main logic. Much better. --- src/arachne.c | 130 +++++++++++++++++++++++++++++++++---------------- src/binding.c | 20 ++++++-- src/term.c | 2 + src/warshall.c | 6 +-- 4 files changed, 107 insertions(+), 51 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 1e75cf9..8f316a5 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -1,4 +1,5 @@ /** + * *@file arachne.c * * Introduces a method for proofs akin to the Athena modelchecker @@ -34,6 +35,7 @@ Role I_V; Role I_R; Role I_E; Role I_D; +Role I_RRS; static int indentDepth; static int max_encryption_level; @@ -112,7 +114,7 @@ arachneInit (const System mysys) add_event (READ, NULL); add_event (READ, NULL); add_event (SEND, NULL); - I_D = add_role ("I_D: Decrypt"); + I_RRS = add_role ("I_D: Encrypt"); return; } @@ -354,7 +356,6 @@ bind_existing_to_goal (const Binding b, const int index, const int run, goal_remove_last (); keycount--; } - termlistDestroy (keylist); } else { @@ -553,13 +554,17 @@ select_goal () b = (Binding) bl->data; if (!b->done) { - float cons; - - cons = term_constrain_level (b->term); - if (cons < min_constrain) + // We don't care about singular variables, so... + if (!isTermVariable (b->term)) { - min_constrain = cons; - best = b; + float cons; + + cons = term_constrain_level (b->term); + if (cons < min_constrain) + { + min_constrain = cons; + best = b; + } } } bl = bl->next; @@ -572,7 +577,7 @@ select_goal () * Handles the case where the intruder constructs a composed term himself. */ int -bind_intruder_to_construct (const Binding b) +bind_goal_new_intruder_run (const Binding b) { Term term; Termlist m0tl; @@ -588,40 +593,50 @@ bind_intruder_to_construct (const Binding b) */ if (!realTermLeaf (term)) { + int run; + int index; + int newgoals; + Roledef rd; Term t1, t2; if (realTermTuple (term)) { - warning ("Goal that is a tuple should not occur!"); // tuple construction - t1 = term->left.op1; - t2 = term->right.op2; - } - else - { - // must be encryption - t1 = term->left.op; - t2 = term->right.key; + error ("Goal that is a tuple should not occur!"); } - goal_add (t1, b->run_to, b->ev_to); - goal_add (t2, b->run_to, b->ev_to); + // must be encryption + t1 = term->left.op; + t2 = term->right.key; + + roleInstance (sys, INTRUDER, I_RRS, NULL, NULL); + run = sys->maxruns - 1; + rd = sys->runs[run].start; + rd->message = termDuplicate (t1); + rd->next->message = termDuplicate (t2); + rd->next->next->message = termDuplicate (term); + index = 2; + newgoals = add_read_goals (run, 0, index+1); #ifdef DEBUG if (DEBUGL (3)) { indentPrint (); - eprintf ("Constructing "); + eprintf ("Encrypting "); termPrint (term); - eprintf (" from smaller terms "); + eprintf (" using term "); termPrint (t1); - eprintf (" and "); + eprintf (" and key "); termPrint (t2); eprintf ("\n"); } #endif - flag = flag && iterate (); - goal_remove_last (); - goal_remove_last (); + if (goal_bind (b, run, index)) + { + flag = flag && iterate (); + } + goal_unbind (b); + remove_read_goals (newgoals); + roleInstanceDestroy (sys); } /** * 2. Constructed from bigger term and decryption key @@ -713,7 +728,7 @@ bind_intruder_to_construct (const Binding b) //! Bind a regular goal int -bind_goal_regular (const Binding b) +bind_goal_regular_run (const Binding b) { int flag; @@ -728,6 +743,12 @@ bind_goal_regular (const Binding b) return 0; } + if (p == INTRUDER) + { + // No intruder roles here + return 1; + } + // Test for interm unification #ifdef DEBUG if (DEBUGL (5)) @@ -761,11 +782,8 @@ bind_goal_regular (const Binding b) #endif // Bind to existing run flag = bind_existing_run (b, p, r, index, 1); - if (p != INTRUDER) - { - // No intruder: bind to new run - flag = flag && bind_new_run (b, p, r, index, 1); - } + // bind to new run + flag = flag && bind_new_run (b, p, r, index, 1); return flag; } else @@ -775,7 +793,7 @@ bind_goal_regular (const Binding b) } } - // Bind to all possible sends or intruder node; + // Bind to all possible sends of regular runs #ifdef DEBUG if (DEBUGL (5)) { @@ -783,32 +801,60 @@ bind_goal_regular (const Binding b) eprintf ("Try regular role send.\n"); } #endif - flag = iterate_role_sends (bind_this_role_send); + return iterate_role_sends (bind_this_role_send); +} + + +// Bind to all possible sends of intruder runs +int bind_goal_old_intruder_run (Binding b) +{ + int run; + int flag; + #ifdef DEBUG if (DEBUGL (5)) { indentPrint (); - eprintf ("Try intruder send.\n"); + eprintf ("Try regular intruder send.\n"); } #endif - // Other option: bind to term construction + flag = 1; + for (run = 0; run < sys->maxruns; run++) + { + if (sys->runs[run].protocol == INTRUDER) + { + int ev; + Roledef rd; - flag = flag && bind_intruder_to_construct (b); - - // Return result + rd = sys->runs[run].start; + ev = 0; + while (ev < sys->runs[run].length) + { + if (rd->type == SEND) + { + flag = flag && bind_existing_to_goal (b, ev, run, 1); + } + rd = rd->next; + ev++; + } + } + } return flag; } - - //! Bind a goal in all possible ways int bind_goal (const Binding b) { if (!b->done) { - return bind_goal_regular (b); + int flag; + + flag = bind_goal_regular_run (b); + flag = flag && bind_goal_old_intruder_run (b); + flag = flag && bind_goal_new_intruder_run (b); + return flag; } else { diff --git a/src/binding.c b/src/binding.c index 79aeddd..92ff099 100644 --- a/src/binding.c +++ b/src/binding.c @@ -226,6 +226,14 @@ void goal_add (Term term, const int run, const int ev) { term = deVar (term); +#ifdef DEBUG + if (term == NULL) + error ("Trying to add an emtpy goal term"); + if (run >= sys->maxruns) + error ("Trying to add a goal for a run that does not exist."); + if (ev >= sys->runs[run].step) + error ("Trying to add a goal for an event that is not in the semistate yet."); +#endif if (realTermTuple (term)) { int width; @@ -280,6 +288,10 @@ goal_bind (const Binding b, const int run, const int ev) { if (!b->done) { +#ifdef DEBUG + if (run >= sys->maxruns || sys->runs[run].step <= ev) + error ("Trying to bind to something not yet in the semistate."); +#endif b->done = 1; b->run_from = run; b->ev_from = ev; @@ -326,7 +338,7 @@ bindings_c_minimal () if (!warshall (graph, nodes)) { // Hmm, cycle - return 0; + error ("Detected a cycle when testing for c-minimality"); } } @@ -344,12 +356,12 @@ bindings_c_minimal () node_from = node_number (b->run_from, b->ev_from); // Find all preceding events - for (run = 0; run <= sys->maxruns; run++) + for (run = 0; run < sys->maxruns; run++) { int ev; //!@todo hardcoded reference to step, should be length - for (ev = 0; run < sys->runs[run].step; ev++) + for (ev = 0; ev < sys->runs[run].step; ev++) { int node_comp; @@ -360,7 +372,7 @@ bindings_c_minimal () Roledef rd; rd = roledef_shift (sys->runs[run].start, ev); - if (termInTerm (rd->message, b->term)) + if (termInTerm (b->term, rd->message)) { // This term already occurs as interm in a previous node! return 0; diff --git a/src/term.c b/src/term.c index 24e8a1c..15d0fc8 100644 --- a/src/term.c +++ b/src/term.c @@ -1092,6 +1092,8 @@ term_constrain_level (const Term term) int nodel (const Term t) { structure++; + if (realTermTuple (t)) + structure++; return 1; } diff --git a/src/warshall.c b/src/warshall.c index 75caed1..0a6eb60 100644 --- a/src/warshall.c +++ b/src/warshall.c @@ -81,11 +81,7 @@ warshall (int *graph, int nodes) { if (graph[index (k, j)] == 1) { - /** - * Previously, we tested k == i (self-loop). - * Now we test 2-node loops, i.e. wether there is also a path from i to k. - */ - if (graph[index (i, k)] > 0) + if (k == i) { // Oh no! A cycle. graph[index (k, i)] = 2;