From c993e175976da45105268810599be63f805bb332 Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 19 Aug 2004 11:37:41 +0000 Subject: [PATCH] - Improving proof output. --- src/arachne.c | 147 +++++++++++++++++++++++++++++++++++--------------- 1 file changed, 105 insertions(+), 42 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index ffa76dc..d8df418 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -145,8 +145,8 @@ indentPrint () if (i % 3 == 0) eprintf ("|"); else - eprintf (" "); - eprintf (" "); + eprintf (" "); + eprintf (" "); } } @@ -186,7 +186,7 @@ add_read_goals (const int run, const int old, const int new) { if (count == 0) { - indentPrint(); + indentPrint (); eprintf ("* Thus, we must also produce "); } else @@ -194,7 +194,7 @@ add_read_goals (const int run, const int old, const int new) eprintf (", "); } termPrint (rd->message); - } + } goal_add (rd->message, run, i); count++; } @@ -321,12 +321,29 @@ proof_select_goal (Binding b) Roledef rd; rd = roledef_shift (sys->runs[b->run_to].start, b->ev_to); + indentDepth--; indentPrint (); - eprintf ("Where does term "); + eprintf ("Selected goal: Where does term "); termPrint (b->term); - eprintf (" , needed for "); + eprintf (" originate first?\n"); + indentPrint (); + eprintf ("* It is required for "); roledefPrint (rd); - eprintf (" at index %i in run %i, originate first?\n", b->ev_to, b->run_to); + eprintf (" at index %i in run %i\n", b->ev_to, b->run_to); + indentDepth++; + } +} + +//! Cannot bind because of cycle +void +proof_cannot_bind (const Binding b, const int run, const int index) +{ + if (sys->output == PROOF) + { + indentPrint (); + eprintf + ("Cannot bind this to run %i, index %i because that introduces a cycle.\n", + run, index); } } @@ -340,11 +357,16 @@ proof_suppose_binding (Binding b) indentPrint (); rd = roledef_shift (sys->runs[b->run_from].start, b->ev_from); - eprintf ("Suppose it originates in run %i, at ", b->run_from); + eprintf ("Suppose it originates in run %i, at index %i\n", b->run_from, + b->ev_from); + indentPrint (); + eprintf ("* I.e. event "); roledefPrint (rd); - eprintf (" from "); + eprintf ("\n"); + indentPrint (); + eprintf ("* from "); role_name_print (b->run_from); - eprintf (" at index %i\n", b->ev_from); + eprintf ("\n"); } } @@ -419,7 +441,8 @@ bind_existing_to_goal (const Binding b, const int run, const int index) if (keylist != NULL && sys->output == PROOF) { indentPrint (); - eprintf ("* This introduces the obligation to produce the following keys: "); + eprintf + ("* This introduces the obligation to produce the following keys: "); termlistPrint (keylist); eprintf ("\n"); } @@ -444,12 +467,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index) } else { - if (sys->output == PROOF) - { - indentPrint (); - eprintf ("Aborted binding existing run because of cycle.\n"); - } - flag = 1; + proof_cannot_bind (b, run, index); } goal_unbind (b); return flag; @@ -481,22 +499,43 @@ bind_existing_run (const Binding b, const Protocol p, const Role r, const int index) { int run, flag; + int found; - if (sys->output == PROOF) - { - indentPrint (); - eprintf ("Can we bind it to an existing regular run?\n"); - } - indentDepth++; flag = 1; + found = 0; for (run = 0; run < sys->maxruns; run++) { if (sys->runs[run].protocol == p && sys->runs[run].role == r) { + found++; + if (sys->output == PROOF) + { + if (found == 1) + { + indentPrint (); + eprintf ("Can we bind it to an existing regular run of "); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf ("?\n"); + } + indentPrint (); + eprintf ("%i. Can we bind it to run %i?\n", found, run); + } + indentDepth++; flag = flag && bind_existing_to_goal (b, run, index); + indentDepth--; } } - indentDepth--; + if (sys->output == PROOF && found == 0) + { + indentPrint (); + eprintf ("There is no existing run for "); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf ("\n"); + } return flag; } @@ -511,10 +550,11 @@ bind_new_run (const Binding b, const Protocol p, const Role r, roleInstance (sys, p, r, NULL, NULL); run = sys->maxruns - 1; - proof_suppose_run (run, 0, index+1); - + proof_suppose_run (run, 0, index + 1); newgoals = add_read_goals (run, 0, index + 1); + indentDepth++; flag = bind_existing_to_goal (b, run, index); + indentDepth--; remove_read_goals (newgoals); roleInstanceDestroy (sys); return flag; @@ -655,9 +695,10 @@ bind_goal_new_m0 (const Binding b) roleInstance (sys, INTRUDER, I_M, NULL, NULL); run = sys->maxruns - 1; - proof_suppose_run (run, 0,1); + proof_suppose_run (run, 0, 1); sys->runs[run].start->message = termDuplicate (b->term); sys->runs[run].length = 1; + indentDepth++; if (goal_bind (b, run, 0)) { proof_suppose_binding (b); @@ -670,7 +711,12 @@ bind_goal_new_m0 (const Binding b) } flag = flag && iterate (); } + else + { + proof_cannot_bind (b, run, 0); + } goal_unbind (b); + indentDepth--; roleInstanceDestroy (sys); termlistSubstReset (subst); termlistDelete (subst); @@ -721,12 +767,11 @@ bind_goal_new_encrypt (const Binding b) rd->next->message = termDuplicate (t2); rd->next->next->message = termDuplicate (term); index = 2; - proof_suppose_run (run, 0, index+1); - newgoals = add_read_goals (run, 0, index + 1); + proof_suppose_run (run, 0, index + 1); if (sys->output == PROOF) { indentPrint (); - eprintf ("Encrypting "); + eprintf ("* Encrypting "); termPrint (term); eprintf (" using term "); termPrint (t1); @@ -734,12 +779,19 @@ bind_goal_new_encrypt (const Binding b) termPrint (t2); eprintf ("\n"); } + newgoals = add_read_goals (run, 0, index + 1); + indentDepth++; if (goal_bind (b, run, index)) { proof_suppose_binding (b); flag = flag && iterate (); } + else + { + proof_cannot_bind (b, run, index); + } goal_unbind (b); + indentDepth--; remove_read_goals (newgoals); roleInstanceDestroy (sys); } @@ -761,6 +813,7 @@ int bind_goal_regular_run (const Binding b) { int flag; + int found; /* * This is a local function so we have access to goal @@ -799,17 +852,20 @@ bind_goal_regular_run (const Binding b) int flag; // A good candidate -#ifdef DEBUG - if (DEBUGL (5)) + found++; + if (sys->output == PROOF) { indentPrint (); - eprintf ("Term "); + eprintf ("* "); termPrint (b->term); - eprintf (" can possibly be bound by role "); + eprintf (" matches the pattern "); + termPrint (rd->message); + eprintf (" from "); + termPrint (p->nameterm); + eprintf (", "); termPrint (r->nameterm); - eprintf (", index %i\n", index); + eprintf (", at %i\n", index); } -#endif // Bind to existing run flag = bind_existing_run (b, p, r, index); // bind to new run @@ -818,7 +874,6 @@ bind_goal_regular_run (const Binding b) } else { - // Cannot unify: no attacks return 1; } } @@ -831,7 +886,16 @@ bind_goal_regular_run (const Binding b) eprintf ("Try regular role send.\n"); } #endif - return iterate_role_sends (bind_this_role_send); + found = 0; + flag = iterate_role_sends (bind_this_role_send); + if (sys->output == PROOF && found == 0) + { + indentPrint (); + eprintf ("The term "); + termPrint (b->term); + eprintf (" does not match any pattern from the role definitions.\n"); + } + return flag; } @@ -1035,7 +1099,8 @@ add_claim_specifics (const Claimlist cl, const Roledef rd) termPrint (rd->message); eprintf (" as a goal.\n"); indentPrint (); - eprintf ("* If all goals can be bound, this constitutes an attack.\n"); + eprintf + ("* If all goals can be bound, this constitutes an attack.\n"); } goal_add (rd->message, 0, cl->ev); // Assumption that all claims are in run 0 } @@ -1079,7 +1144,6 @@ iterate () int flag; flag = 1; - indentDepth++; if (!prune ()) { Binding b; @@ -1117,7 +1181,6 @@ iterate () flag = bind_goal (b); } } - indentDepth--; #ifdef DEBUG if (DEBUGL (5) && !flag) @@ -1207,7 +1270,7 @@ arachne () role_name_print (0); eprintf (" at index %i.\n", cl->ev); } - proof_suppose_run (0,0, cl->ev+1); + proof_suppose_run (0, 0, cl->ev + 1); add_read_goals (sys->maxruns - 1, 0, cl->ev + 1);