- After some trouble, nonce binding is working nicely.

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)
+      flag = 1;
-	      && bind_new_run (goal, p, r, index));
+      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)
+      flag = 1;
-	      && bind_new_run (goal, p, r, index));
+      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

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;
+}

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