From 92a98a85cc3007e27d00d93d49f53630fbe17171 Mon Sep 17 00:00:00 2001 From: ccremers Date: Tue, 1 Aug 2006 06:04:01 +0000 Subject: [PATCH] - Single claim check branched. --- src/arachne.c | 276 +++++++++++++++++++++++++++----------------------- 1 file changed, 147 insertions(+), 129 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 9eed29c..65cf1ca 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -2231,6 +2231,147 @@ iterate_buffer_attacks (void) } } +//! Arachne single claim +int +arachneClaim (Claimlist cl) +{ + // Skip the dummy claims + if (!isTermEqual (cl->type, CLAIM_Empty)) + { + // Any other claims might be filterered + if (switches.filterClaim == NULL || switches.filterClaim == cl->type) + { + // Some claims are always true! + if (!cl->alwaystrue) + { + // others we simply test... + int run; + int newruns; + Protocol p; + Role r; + + newruns = 0; + sys->current_claim = cl; + attack_length = INT_MAX; + attack_leastcost = INT_MAX; + cl->complete = 1; + p = (Protocol) cl->protocol; + r = (Role) cl->role; + + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Testing Claim "); + termPrint (cl->type); + eprintf (" from "); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf (" at index %i.\n", cl->ev); + } + indentDepth++; + + run = semiRunCreate (p, r); + newruns++; + { + int newgoals; + + int realStart (void) + { +#ifdef DEBUG + if (DEBUGL (5)) + { + printSemiState (); + } +#endif + return iterate_buffer_attacks (); + } + + proof_suppose_run (run, 0, cl->ev + 1); + newgoals = add_read_goals (run, 0, cl->ev + 1); + + /** + * Add initial knowledge node + */ + { + Termlist m0tl; + Term m0t; + int m0run; + + m0tl = knowledgeSet (sys->know); + m0t = termlist_to_tuple (m0tl); + // eprintf("Initial intruder knowledge node for "); + // termPrint(m0t); + // eprintf("\n"); + I_M->roledef->message = m0t; + m0run = semiRunCreate (INTRUDER, I_M); + newruns++; + proof_suppose_run (m0run, 0, 1); + sys->runs[m0run].height = 1; + + { + /** + * Add specific goal info and iterate algorithm + */ + add_claim_specifics (sys, cl, + roledef_shift (sys->runs[run]. + start, cl->ev), + realStart); + } + + + // remove initial knowledge node + termDelete (m0t); + termlistDelete (m0tl); + semiRunDestroy (); + newruns--; + } + // remove claiming run goals + goal_remove_last (newgoals); + semiRunDestroy (); + newruns--; + } + //! Destroy + while (sys->maxruns > 0 && newruns > 0) + { + semiRunDestroy (); + newruns--; + } +#ifdef DEBUG + if (sys->bindings != NULL) + { + error ("sys->bindings NOT empty after claim test."); + } + if (sys->maxruns != 0) + { + error ("%i undestroyed runs left after claim test.", + sys->maxruns); + } + if (newruns != 0) + { + error ("Lost %i runs after claim test.", newruns); + } +#endif + + //! Indent back + indentDepth--; + + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Proof complete for this claim.\n"); + } + } + } + return true; + } + else + { + return false; + } +} + + //! Main code for Arachne /** * For this test, we manually set up some stuff. @@ -2241,6 +2382,7 @@ int arachne () { Claimlist cl; + int count; int print_send (Protocol p, Role r, Roledef rd, int index) { @@ -2304,145 +2446,21 @@ arachne () indentDepth = 0; proofDepth = 0; cl = sys->claimlist; + count = 0; while (cl != NULL) { /** * Check each claim */ - - // Skip the dummy claims - if (!isTermEqual (cl->type, CLAIM_Empty)) + if (arachneClaim (cl)) { - // Any other claims might be filterered - if (switches.filterClaim == NULL - || switches.filterClaim == cl->type) - { - // Some claims are always true! - if (!cl->alwaystrue) - { - // others we simply test... - int run; - int newruns; - Protocol p; - Role r; - - newruns = 0; - sys->current_claim = cl; - attack_length = INT_MAX; - attack_leastcost = INT_MAX; - cl->complete = 1; - p = (Protocol) cl->protocol; - r = (Role) cl->role; - - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Testing Claim "); - termPrint (cl->type); - eprintf (" from "); - termPrint (p->nameterm); - eprintf (", "); - termPrint (r->nameterm); - eprintf (" at index %i.\n", cl->ev); - } - indentDepth++; - - run = semiRunCreate (p, r); - newruns++; - { - int newgoals; - - int realStart (void) - { -#ifdef DEBUG - if (DEBUGL (5)) - { - printSemiState (); - } -#endif - return iterate_buffer_attacks (); - } - - proof_suppose_run (run, 0, cl->ev + 1); - newgoals = add_read_goals (run, 0, cl->ev + 1); - - /** - * Add initial knowledge node - */ - { - Termlist m0tl; - Term m0t; - int m0run; - - m0tl = knowledgeSet (sys->know); - m0t = termlist_to_tuple (m0tl); - // eprintf("Initial intruder knowledge node for "); - // termPrint(m0t); - // eprintf("\n"); - I_M->roledef->message = m0t; - m0run = semiRunCreate (INTRUDER, I_M); - newruns++; - proof_suppose_run (m0run, 0, 1); - sys->runs[m0run].height = 1; - - { - /** - * Add specific goal info and iterate algorithm - */ - add_claim_specifics (sys, cl, - roledef_shift (sys->runs[run]. - start, cl->ev), - realStart); - } - - - // remove initial knowledge node - termDelete (m0t); - termlistDelete (m0tl); - semiRunDestroy (); - newruns--; - } - // remove claiming run goals - goal_remove_last (newgoals); - semiRunDestroy (); - newruns--; - } - //! Destroy - while (sys->maxruns > 0 && newruns > 0) - { - semiRunDestroy (); - newruns--; - } -#ifdef DEBUG - if (sys->bindings != NULL) - { - error ("sys->bindings NOT empty after claim test."); - } - if (sys->maxruns != 0) - { - error ("%i undestroyed runs left after claim test.", - sys->maxruns); - } - if (newruns != 0) - { - error ("Lost %i runs after claim test.", newruns); - } -#endif - - //! Indent back - indentDepth--; - - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Proof complete for this claim.\n"); - } - } - } + count++; } + // next cl = cl->next; } + return count; } //! Construct knowledge set at some event, based on a semitrace.