From f384042bfedc68bf51e80055fc3df5661535e5fd Mon Sep 17 00:00:00 2001 From: ccremers Date: Mon, 16 Aug 2004 14:49:41 +0000 Subject: [PATCH] - Switched -r n behaviour for Arachne, effectively turning it into the upper bound on runs. --- src/arachne.c | 101 ++++++++++++++++++++++++++++++++++++++------------ src/main.c | 14 ++++++- src/system.c | 1 + src/system.h | 1 + 4 files changed, 91 insertions(+), 26 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 672b386..250d3c4 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -106,15 +106,9 @@ arachneInit (const System mysys) add_event (READ, NULL); I_GOAL = add_role (" I_GOAL "); - know0 = knowledgeSet (sys->know); - tl = know0; - while (tl != NULL) - { - add_event (SEND, tl->term); - I_M0 = add_role (" I_M0 "); - tl = tl->next; - } - termlistDelete (know0); + add_event (SEND, NULL); + I_M0 = add_role (" I_M0 "); + return; } @@ -268,6 +262,7 @@ create_intruder_goal (Term t) { explanation = "Adding intruder goal for message "; e_term1 = t; + e_run = run; } #endif return run; @@ -441,6 +436,8 @@ bind_new_run (const Goal goal, const Protocol p, const Role r, int run; int flag; + roleInstance (sys, p, r, NULL, NULL); + run = sys->maxruns - 1; #ifdef DEBUG if (DEBUGL (4)) { @@ -451,11 +448,9 @@ bind_new_run (const Goal goal, const Protocol p, const Role r, termPrint (p->nameterm); eprintf (", "); termPrint (r->nameterm); - eprintf (" (%i)\n", subterm); + eprintf (", run %i (subterm:%i)\n", run, subterm); } #endif - roleInstance (sys, p, r, NULL, NULL); - run = sys->maxruns - 1; flag = bind_existing_to_goal (goal, index, run, subterm); roleInstanceDestroy (sys); return flag; @@ -705,12 +700,20 @@ int bind_intruder_to_construct (const Goal goal) { Term term; + Termlist m0tl; + int flag; + int run; + flag = 1; term = goal.rd->message; + /** + * Two options. + * + * 1. Constructed from composite terms + */ if (!realTermLeaf (term)) { Term t1, t2; - int flag; if (realTermTuple (term)) { @@ -724,19 +727,66 @@ bind_intruder_to_construct (const Goal goal) t1 = term->left.op; t2 = term->right.key; } - create_intruder_goal (t1); - create_intruder_goal (t2); - - flag = iterate (); + run = create_intruder_goal (t1); + if (binding_add (run, 0, goal.run, goal.index)) + { + run = create_intruder_goal (t2); + if (binding_add (run, 0, goal.run, goal.index)) + { + flag = flag && iterate (); + } + binding_remove_last (); + roleInstanceDestroy (sys); + } + binding_remove_last (); roleInstanceDestroy (sys); - roleInstanceDestroy (sys); - return flag; } - else + /** + * 2. Retrieved from M_0 + */ + m0tl = knowledgeSet (sys->know); + while (flag && m0tl != NULL) { - return 1; + Term m0t; + Termlist subst; + + m0t = m0tl->term; + subst = termMguTerm (term, m0t); + if (subst != MGUFAIL) + { + int run; + + roleInstance (sys, INTRUDER, I_M0, NULL, NULL); + run = sys->maxruns - 1; + sys->runs[run].start->message = termDuplicate(term); + sys->runs[run].length = 1; + if (binding_add (run, 0, goal.run, goal.index)) + { +#ifdef DEBUG + if (DEBUGL (3)) + { + indentPrint (); + eprintf ("Retrieving "); + termPrint (term); + eprintf (" from the initial knowledge.\n"); + } +#endif + iterate (); + } + binding_remove_last (); + roleInstanceDestroy (sys); + termlistSubstReset (subst); + termlistDelete (subst); + } + + m0tl = m0tl->next; } + termlistDelete (m0tl); + /** + * return result + */ + return flag; } @@ -766,6 +816,7 @@ bind_goal_intruder (const Goal goal) // This seems to work flag = flag && iterate (); termlistSubstReset (substlist); + termlistDelete (substlist); } tl = tl->next; } @@ -820,7 +871,7 @@ prune () #endif return 1; } - if (sys->maxruns > 4) + if (sys->maxruns > sys->switchRuns) { // Hardcoded limit on runs #ifdef DEBUG @@ -862,13 +913,13 @@ prune () #endif return 1; } - if (inTermlist (sys->untrusted, agent)) + if (!realTermVariable (agent) && inTermlist (sys->untrusted, agent)) { #ifdef DEBUG if (DEBUGL (3)) { indentPrint (); - eprintf ("Pruned because agents must be untrusted.\n"); + eprintf ("Pruned because all agents of the claim run must be trusted.\n"); } #endif return 1; @@ -914,7 +965,9 @@ iterate () #ifdef DEBUG if (DEBUGL (3) && explanation != NULL) { + indentDepth--; indentPrint (); + indentDepth++; eprintf ("ITERATE: %s", explanation); if (e_run != INVALID) diff --git a/src/main.c b/src/main.c index 4e183e9..1b8df98 100644 --- a/src/main.c +++ b/src/main.c @@ -360,7 +360,8 @@ main (int argc, char **argv) } /* handle switches */ - + + sys->switchRuns = switch_maximum_runs->ival[0]; /* maximum number of runs */ if (switch_implicit_choose->count > 0) /* allow implicit chooses */ sys->switchForceChoose = 0; @@ -453,7 +454,16 @@ main (int argc, char **argv) /* compile */ - compile (spdltac, switch_maximum_runs->ival[0]); + if (sys->engine != ARACHNE_ENGINE) + { + // Compile as many runs as possible + compile (spdltac, switch_maximum_runs->ival[0]); + } + else + { + // Compile no runs for Arachne + compile (spdltac, 0); + } scanner_cleanup (); /* preprocess */ diff --git a/src/system.c b/src/system.c index ce3186f..d394e63 100644 --- a/src/system.c +++ b/src/system.c @@ -58,6 +58,7 @@ systemInit () sys->output = ATTACK; // default is to show the attacks sys->porparam = 0; // multi-purpose parameter sys->latex = 0; // latex output? + sys->switchRuns = INT_MAX; sys->switchScenario = 0; sys->switchScenarioSize = 0; sys->switchForceChoose = 1; // force explicit chooses by default diff --git a/src/system.h b/src/system.h index 49a728b..62f741e 100644 --- a/src/system.h +++ b/src/system.h @@ -128,6 +128,7 @@ struct system int switchT; //!< Time display switch. int switchS; //!< Progress display switch. (traversed states) int porparam; //!< A multi-purpose integer parameter, passed to the partial order reduction method selected. + int switchRuns; //!< The number of runs as in the switch int switchScenario; //!< -1 to count, 0 for disable, 1-n to select the choose scenario int switchScenarioSize; //!< Scenario size, also called fixed trace prefix length int switchForceChoose; //!< Force chooses for each run, even if involved in first read