From f219461c8d109d6c6f9d86a500bc5222a8090903 Mon Sep 17 00:00:00 2001 From: ccremers Date: Sat, 14 Aug 2004 14:23:21 +0000 Subject: [PATCH] - After some trouble, nonce binding is working nicely. --- src/arachne.c | 86 ++++++++++++++++++++++++++++++++++++++++++++++++--- src/term.c | 11 +++++++ src/term.h | 10 ++++-- 3 files changed, 99 insertions(+), 8 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 3a5338b..1922771 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -79,6 +79,12 @@ arachneInit (const System mysys) } sys = mysys; // make sys available for this module as a global + + /** + * Very important: turn role terms that are local to a run, into variables. + */ + term_rolelocals_are_variables (); + /* * Add intruder protocol roles */ @@ -132,6 +138,54 @@ mgu_iterate (const Termlist tl) return iterate (); } +//! Determine the run that follows from a substitution. +/** + * After an Arachne unification, stuff might go wrong w.r.t. nonce instantiation. + * This function determines the run that is implied by a substitution list. + * @returns >= 0: a run, -1 for invalid, -2 for any run. + */ +int +determine_unification_run (Termlist tl) +{ + int run; + + run = -2; + while (tl != NULL) + { + //! Again, hardcoded reference to compiler.c. Level -3 means a local constant for a role. + if (tl->term->type != VARIABLE && tl->term->right.runid == -3) + { + Term t; + + t = tl->term->subst; + + // It is required that it is actually a leaf, because we construct it. + if (!realTermLeaf (t)) + { + return -1; + } + else + { + if (run == -2) + { + // Any run + run = t->right.runid; + } + else + { + // Specific run: compare + if (run != t->right.runid) + { + return -1; + } + } + } + } + tl = tl->next; + } + return run; +} + //------------------------------------------------------------------------ // Sub //------------------------------------------------------------------------ @@ -238,6 +292,7 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r, eprintf ("\n"); #endif flag = 1; + goal.rd->bind_index = index; for (run = 0; run < sys->maxruns; run++) { if (sys->runs[run].protocol == p && sys->runs[run].role == r) @@ -257,12 +312,15 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r, e_run = run; e_term1 = goal.rd->message; #endif + goal.rd->bind_run = run; + flag = (flag && termMguInTerm (goal.rd->message, rd->message, mgu_iterate)); sys->runs[run].length = old_length; } } + goal.rd->bind_run = -1; return flag; } @@ -383,20 +441,29 @@ bind_goal_regular (const Goal goal) { int bind_this_unification (Termlist substlist) { + int run, flag; + + run = determine_unification_run (substlist); + if (run == -1) + return 1; #ifdef DEBUG indentPrint (); eprintf ("Term "); termPrint (goal.rd->message); eprintf (" can possibly be bound by role "); termPrint (r->nameterm); - eprintf (", index %i.\n", index); + eprintf (", index %i, forced_run %i\n", index, run); #endif /** * Two options; as this, it is from an existing run, * or from a new one. */ - return (bind_existing_run (goal, p, r, index) - && bind_new_run (goal, p, r, index)); + flag = 1; + if (run == -2) + { + flag = flag && bind_new_run (goal, p, r, index); + } + return (flag && bind_existing_run (goal, p, r, index)); } if (p == INTRUDER) @@ -446,6 +513,11 @@ bind_intruder_to_regular (Goal goal) int flag; int keygoals; Termlist tl; + int run; + + run = determine_unification_run (substlist); + if (run == -1) + return 1; /** * the list of keys is added as a new goal. @@ -465,8 +537,12 @@ bind_intruder_to_regular (Goal goal) * or from a new one. */ - flag = (bind_existing_run (goal, p, r, index) - && bind_new_run (goal, p, r, index)); + flag = 1; + if (run == -2) + { + flag = flag && bind_new_run (goal, p, r, index); + } + flag = flag && bind_existing_run (goal, p, r, index); /** * deconstruct key list goals diff --git a/src/term.c b/src/term.c index 89d6333..2520220 100644 --- a/src/term.c +++ b/src/term.c @@ -19,6 +19,9 @@ #include "memory.h" #include "ctype.h" +/* public flag */ +int rolelocal_variable; + /* external definitions */ extern Term TERM_Function; @@ -41,6 +44,7 @@ void indent (void); void termsInit (void) { + rolelocal_variable = 0; return; } @@ -931,3 +935,10 @@ term_iterate_open_leaves (const Term term, int (*func) ()) return term_iterate_leaves (term, testleaf); } + +//! Turn all rolelocals into variables +void +term_rolelocals_are_variables () +{ + rolelocal_variable = 1; +} diff --git a/src/term.h b/src/term.h index 8d80f37..b3ea1de 100644 --- a/src/term.h +++ b/src/term.h @@ -53,6 +53,9 @@ struct term } right; }; +//! Flag for term status +extern int rolelocal_variable; + //! Pointer shorthand. typedef struct term *Term; @@ -62,12 +65,12 @@ Term makeTermEncrypt (Term t1, Term t2); Term makeTermTuple (Term t1, Term t2); Term makeTermType (const int type, const Symbol symb, const int runid); __inline__ Term deVarScan (Term t); -#define substVar(t) ((t != NULL && t->type == VARIABLE && t->subst != NULL) ? 1 : 0) -#define deVar(t) ( substVar(t) ? deVarScan(t->subst) : t) #define realTermLeaf(t) (t != NULL && t->type <= LEAF) #define realTermTuple(t) (t != NULL && t->type == TUPLE) #define realTermEncrypt(t) (t != NULL && t->type == ENCRYPT) -#define realTermVariable(t) (t != NULL && t->type == VARIABLE) +#define realTermVariable(t) (t != NULL && (t->type == VARIABLE || (rolelocal_variable && t->right.runid == -3))) +#define substVar(t) ((realTermVariable (t) && t->subst != NULL) ? 1 : 0) +#define deVar(t) ( substVar(t) ? deVarScan(t->subst) : t) #define isTermLeaf(t) realTermLeaf(deVar(t)) #define isTermTuple(t) realTermTuple(deVar(t)) #define isTermEncrypt(t) realTermEncrypt(deVar(t)) @@ -166,5 +169,6 @@ float termDistance (Term t1, Term t2); int termOrder (Term t1, Term t2); int term_iterate_leaves (const Term t, int (*func) ()); int term_iterate_open_leaves (const Term term, int (*func) ()); +void term_rolelocals_are_variables (); #endif