From fe16785982edeb8a2c0b63f51533bb29d0acce79 Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 13 Aug 2004 20:09:12 +0000 Subject: [PATCH] - Fixed error in error reporting :-\ - Added intruder construction nodes. - Several cleanups. --- src/arachne.c | 153 +++++++++++++++++++++++++++++-------------------- src/mgu.c | 12 ++-- src/system.c | 3 +- src/termlist.c | 2 +- 4 files changed, 99 insertions(+), 71 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index f4ff122..0fb9fbb 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -374,18 +374,12 @@ bind_goal_regular (const Goal goal) * * Note that we only bind to regular runs here */ - int flag; - if (p == INTRUDER) { return 1; // don't abort scans } - flag = bind_existing_run (goal, p, r, index); - if (flag) - { - flag = bind_new_run (goal, p, r, index); - } - return flag; + return (bind_existing_run (goal, p, r, index) + && bind_new_run (goal, p, r, index)); } // Test for interm unification @@ -397,78 +391,109 @@ bind_goal_regular (const Goal goal) } //! Bind an intruder goal to a regular run +/** + * A bit of a problem child, this one. + */ int -bind_intruder_to_regular (const Goal goal) +bind_intruder_to_regular (Goal goal) { - int bind_this_f2 (Protocol p, Role r, Roledef rd, int index) + int bind_this_roleevent (Protocol p, Role r, Roledef rd, int index) { - int element_f2 (Termlist substlist, Termlist keylist) + int bind_this_unification (Termlist substlist, Termlist keylist) { int flag; + int keygoals; + Termlist tl; /** - * Note that we only bind to regular runs here + * the list of keys is added as a new goal. */ - if (p == INTRUDER) + keygoals = 0; + tl = keylist; + while (tl != NULL) { - return 1; // don't abort scans + keygoals++; + create_intruder_goal (tl->term); + //!@todo This needs a mapping Pi relation as well. + + tl = tl->next; } - else + /** + * Two options; as this, it is from an existing run, + * or from a new one. + */ + + flag = (bind_existing_run (goal, p, r, index) + && bind_new_run (goal, p, r, index)); + + /** + * deconstruct key list goals + */ + while (keygoals > 0) { - int keygoals; - - /** - * In any case, the list of keys is added as a new goal. - */ - int add_key_goal (Term t) - { - keygoals++; - create_intruder_goal (t); - //!@todo This needs a mapping Pi relation as well. - return 1; - } - - keygoals = 0; - termlist_iterate (keylist, add_key_goal); - /** - * Two options; as this, it is from an existing run, - * or from a new one. - */ - - /** - * This code has a major bug (memory destruction) - * in both branches - *@todo FIX!! - */ - flag = (bind_existing_run (goal, p, r, index) - && bind_new_run (goal, p, r, index)); - - /** - * deconstruct key list goals - */ - while (keygoals > 0) - { - roleInstanceDestroy (sys); - keygoals--; - } - - return flag; + roleInstanceDestroy (sys); + keygoals--; } + + return flag; } - // Test for subterm unification - return termMguSubTerm (goal.rd->message, rd->message, element_f2, - sys->traceKnow[0]->inverses, NULL); + /** + * Note that we only bind to regular runs here + */ + if (p == INTRUDER) + { + return 1; // don't abort scans + } + else + { // Test for subterm unification + return termMguSubTerm (goal.rd->message, rd->message, + bind_this_unification, sys->know->inverses, + NULL); + } } // Bind to all possible sends? - return iterate_role_sends (bind_this_f2); + return iterate_role_sends (bind_this_roleevent); } //! Bind an intruder goal by intruder construction int bind_intruder_to_construct (const Goal goal) { + Term term; + + term = goal.rd->message; + if (!realTermLeaf (term)) + { + Term t1, t2; + int flag; + + if (realTermTuple (term)) + { + // tuple construction + t1 = term->left.op1; + t2 = term->right.op2; + } + else + { + // must be encryption + t1 = term->left.op; + t2 = term->right.key; + } + create_intruder_goal (t1); + create_intruder_goal (t2); + + flag = iterate (); + + roleInstanceDestroy (sys); + roleInstanceDestroy (sys); + return flag; + } + else + { + return 1; + } } @@ -504,7 +529,7 @@ bind_goal (const Goal goal) int prune () { - if (indentDepth > 2) + if (indentDepth > 10) { // Hardcoded limit on iterations #ifdef DEBUG @@ -569,11 +594,6 @@ iterate () eprintf (" "); } eprintf ("\n"); - explanation = NULL; - e_run = INVALID; - e_term1 = NULL; - e_term2 = NULL; - e_term3 = NULL; } #endif @@ -605,6 +625,13 @@ iterate () flag = bind_goal (goal); } } +#ifdef DEBUG + explanation = NULL; + e_run = INVALID; + e_term1 = NULL; + e_term2 = NULL; + e_term3 = NULL; +#endif indentDepth--; return flag; } diff --git a/src/mgu.c b/src/mgu.c index e46e900..a4ad886 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -73,7 +73,7 @@ termMguTerm (Term t1, Term t2) } /* symmetrical tests for single variable */ - if (isTermVariable (t1)) + if (realTermVariable (t1)) { if (termOccurs (t2, t1)) return MGUFAIL; @@ -86,7 +86,7 @@ termMguTerm (Term t1, Term t2) return termlistAdd (NULL, t1); } } - if (isTermVariable (t2)) + if (realTermVariable (t2)) { if (termOccurs (t1, t2)) return MGUFAIL; @@ -106,7 +106,7 @@ termMguTerm (Term t1, Term t2) /* identical compounds */ /* encryption first */ - if (isTermEncrypt (t1)) + if (realTermEncrypt (t1)) { Termlist tl1, tl2; @@ -175,7 +175,7 @@ termMguInTerm (Term t1, Term t2, int (*iterator) ()) t2 = deVar (t2); if (t2 != NULL) { - if (isTermTuple (t2)) + if (realTermTuple (t2)) { // t2 is a tuple, consider interm options as well. flag = flag && termMguInTerm (t1, t2->left.op1, iterator); @@ -210,9 +210,9 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (), t2 = deVar (t2); if (t2 != NULL) { - if (!isTermLeaf (t2)) + if (!realTermLeaf (t2)) { - if (isTermTuple (t2)) + if (realTermTuple (t2)) { // 'simple' tuple flag = diff --git a/src/system.c b/src/system.c index 9708ba9..23b0d86 100644 --- a/src/system.c +++ b/src/system.c @@ -596,8 +596,9 @@ roleInstance (const System sys, const Protocol protocol, const Role role, { // Make new var for this run newt = makeTermType (VARIABLE, newt->left.symb, rid); - newt->subst = oldt->subst; artefacts = termlistAdd (artefacts, newt); + // Copy substitution + newt->subst = oldt->subst; } // Add to agent list, possibly if (inTermlist (protocol->rolenames, oldt)) diff --git a/src/termlist.c b/src/termlist.c index bbbb360..ae4f4e9 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -601,7 +601,7 @@ termLocal (Term t, Termlist fromlist, Termlist tolist, const int runid) if (t == NULL) return NULL; - deVar (t); // remove any instantiated variables from the term. + // deVar (t); // remove any instantiated variables from the term. if (realTermLeaf (t)) { while (fromlist != NULL && tolist != NULL)