- [[[ Broken commit ]]]

More intermediate work.

src/arachne.c

@@ -302,6 +302,18 @@ semiRunCreate (const Protocol p, const Role r)
     num_intruder_runs++;
   else
     num_regular_runs++;
+#ifdef DEBUG
+  if (DEBUGL (5))
+    {
+      globalError++;
+      eprintf ("Adding a run %i with semiRunCreate, ", sys->maxruns);
+      termPrint (p->nameterm);
+      eprintf (", ");
+      termPrint (r->nameterm);
+      eprintf ("\n");
+      globalError--;
+    }
+#endif
   roleInstance (sys, p, r, NULL, NULL);
   run = sys->maxruns - 1;
   sys->runs[run].height = 0;
@@ -688,6 +700,19 @@ create_decryptor (const Term term, const Term key)
       Term tempkey;
       int run;
 
+#ifdef DEBUG
+      if (DEBUGL (5))
+	{
+	  globalError++;
+	  eprintf ("Creating decryptor for term ");
+	  termPrint (term);
+	  eprintf (" and key ");
+	  termPrint (key);
+	  eprintf ("\n");
+	  globalError--;
+	}
+#endif
+
       run = semiRunCreate (INTRUDER, I_RRSD);
       rd = sys->runs[run].start;
       rd->message = termDuplicateUV (term);
@@ -731,6 +756,142 @@ getPriorityOfNeededKey (const System sys, const Term keyneeded)
   return prioritylevel;
 }
 
+//! Try to bind a specific existing run to a goal.
+/**
+ * The idea is that we try to bind it this specific run and index. If this
+ * requires keys, then we should add such goals as well with the required
+ * decryptor things.
+ *
+ * The key goals are bound to the goal. Iterates on success.
+ */
+int
+bind_existing_to_goal (const Binding b, const int run, const int index)
+{
+  int old_length;
+  int flag;
+  int newgoals;
+
+  int subterm_unification_needs (const Binding bt, Term tbig)
+  {
+    Term t;
+    int flag;
+
+    int bind_iterate (Termlist tl)
+    {
+      if (goal_bind (bt, run, index))
+	{
+	  int flag;
+
+	  flag = iterate ();
+	  goal_unbind (bt);
+	  return flag;
+	}
+      return false;
+    }
+
+    if (bt == NULL)
+      {
+	return false;
+      }
+    flag = false;
+    t = deVar (bt->term);
+    tbig = deVar (tbig);
+
+    // First check whether it unifies in a simple way
+    flag = flag || unify (t, tbig, NULL, bind_iterate);
+
+    // The other options are unification on subparts
+    if (realTermTuple (tbig))
+      {
+	// Either one will do
+	return (subterm_unification_needs (bt, TermOp1 (tbig)) ||
+		subterm_unification_needs (bt, TermOp1 (tbig)));
+      }
+    if (realTermEncrypt (tbig))
+      {
+	Term keyneeded;
+	Roledef rddecrypt;
+	int smallrun;
+	int prioritylevel;
+	int newgoals;
+	Binding bnew;
+
+	// Maybe we can bind to the inner thing. Try.
+	// Add decryptor run
+	keyneeded = inverseKey (sys->know->inverses, TermKey (tbig));
+	prioritylevel = getPriorityOfNeededKey (sys, keyneeded);
+	smallrun = create_decryptor (tbig, keyneeded);
+	rddecrypt = sys->runs[smallrun].start;
+
+	/*
+	 * 2. Add goal bindings
+	 */
+
+	newgoals = goal_add (rddecrypt->message, smallrun, 0, 0);
+	if (newgoals >= 0)
+	  {
+	    if (newgoals > 1)
+	      {
+		error
+		  ("Added more than one goal for decryptor goal 1, weird.");
+	      }
+	    else
+	      {
+		// This is the unique new goal then
+		bnew = (Binding) sys->bindings->data;
+	      }
+	  }
+	else
+	  {
+	    error ("No new binding added for inner message.");
+	    // No new binding? Weird, but fair enough
+	    bnew = NULL;
+	  }
+
+	newgoals += goal_add (rddecrypt->next->message, smallrun, 1,
+			      prioritylevel);
+	/*
+	 * 3. Bind open goal to decryptor
+	 */
+	if (goal_bind (bt, smallrun, 2))
+	  {
+	    // Allright, good binding, proceed with next
+	    flag = flag || subterm_unification_needs (bnew, TermOp (tbig));
+	    goal_unbind (bt);
+	  }
+	/*
+	 * clean up
+	 */
+	termDelete (keyneeded);
+	goal_remove_last (newgoals);
+	semiRunDestroy ();
+
+	return flag;
+      }
+    return false;
+  }
+
+  old_length = sys->runs[run].height;
+  if ((index + 1) > old_length)
+    {
+      newgoals = add_read_goals (run, old_length, index + 1);
+    }
+  else
+    {
+      newgoals = 0;
+    }
+  flag =
+    subterm_unification_needs (b,
+			       roledef_shift (sys->runs[run].start,
+					      index)->message);
+  if (newgoals > 0)
+    {
+      goal_remove_last (newgoals);
+    }
+  sys->runs[run].height = old_length;
+  return flag;
+}
+
 //! Try to bind a specific existing run to a goal.
 /**
  * The key goals are bound to the goal.
@@ -746,7 +907,7 @@ getPriorityOfNeededKey (const System sys, const Term keyneeded)
  *@param index	index in run of binding start
  */
 int
-bind_existing_to_goal (const Binding b, const int run, const int index)
+bind_existing_to_goal_old (const Binding b, const int run, const int index)
 {
   Roledef rd;
   int flag;
@@ -1370,8 +1531,14 @@ bind_goal_regular_run (const Binding b)
 	indentDepth++;
 
 	// Bind to existing run
+#ifdef DEBUG
+	debug (5, "Trying to bind to existing run.");
+#endif
 	sflag = bind_existing_run (b, p, r, index);
 	// bind to new run
+#ifdef DEBUG
+	debug (5, "Trying to bind to new run.");
+#endif
 	sflag = sflag && bind_new_run (b, p, r, index);
 
 	indentDepth--;

src/binding.c

@@ -123,7 +123,18 @@ goal_bind (const Binding b, const int run, const int ev)
     {
 #ifdef DEBUG
       if (run >= sys->maxruns || sys->runs[run].step <= ev)
-	error ("Trying to bind to something not yet in the semistate.");
+	{
+	  globalError++;
+	  eprintf ("For term: ");
+	  termPrint (b->term);
+	  eprintf (" needed for r%ii%i.\n", b->run_to, b->ev_to);
+	  eprintf ("Current limits: %i runs, %i events for this run.\n",
+		   sys->maxruns, sys->runs[run].step);
+	  globalError--;
+	  error
+	    ("trying to bind to something not yet in the semistate: r%ii%i.",
+	     run, ev);
+	}
 #endif
       b->run_from = run;
       b->ev_from = ev;

src/mgu.c

@@ -110,6 +110,134 @@ termlistSubstReset (Termlist tl)
     }
 }
 
+//! Most general unifier iteration
+/**
+ * Try to determine the most general unifier of two terms, if so calls function.
+ *
+ * The callback receives a list of variables, that were previously open, but are now closed
+ * in such a way that the two terms unify. Returns result of iteration, or false if not.
+ */
+int
+unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
+{
+  /* added for speed */
+  t1 = deVar (t1);
+  t2 = deVar (t2);
+  if (t1 == t2)
+    return callback (tl);
+
+  int callsubst (Termlist tl, Term t, Term tsubst)
+  {
+    int flag;
+
+    t->subst = tsubst;
+#ifdef DEBUG
+    showSubst (t);
+#endif
+    tl = termlistAdd (tl, t);
+    flag = callback (tl);
+    tl = termlistDelTerm (tl);
+    t->subst = NULL;
+    return flag;
+  }
+
+  if (!(hasTermVariable (t1) || hasTermVariable (t2)))
+    {
+      if (isTermEqual (t1, t2))
+	{
+	  return callback (tl);
+	}
+      else
+	{
+	  return false;
+	}
+    }
+
+  /*
+   * Distinguish a special case where both are unbound variables that will be
+   * connected, and I want to give one priority over the other for readability.
+   *
+   * Because t1 and t2 have been deVar'd means that if they are variables, they
+   * are also unbound.
+   */
+
+  if (realTermVariable (t1) && realTermVariable (t2) && goodsubst (t1, t2))
+    {
+      /* Both are unbound variables. Decide.
+       *
+       * The plan: t1->subst will point to t2. But maybe we prefer the other
+       * way around?
+       */
+      if (preferSubstitutionOrder (t2, t1))
+	{
+	  Term t3;
+
+	  // Swappy.
+	  t3 = t1;
+	  t1 = t2;
+	  t2 = t3;
+	}
+      return callsubst (tl, t1, t2);
+    }
+
+  /* symmetrical tests for single variable.
+   */
+
+  if (realTermVariable (t2))
+    {
+      if (termSubTerm (t1, t2) || !goodsubst (t2, t1))
+	return false;
+      else
+	{
+	  return callsubst (tl, t2, t1);
+	}
+    }
+  if (realTermVariable (t1))
+    {
+      if (termSubTerm (t2, t1) || !goodsubst (t1, t2))
+	return false;
+      else
+	{
+	  return callsubst (tl, t1, t2);
+	}
+    }
+
+  /* left & right are compounds with variables */
+  if (t1->type != t2->type)
+    return false;
+
+  /* identical compound types */
+
+  /* encryption first */
+  if (realTermEncrypt (t1))
+    {
+      int unify_combined_enc (Termlist tl)
+      {
+	// now the keys are unified (subst in this tl)
+	// and we try the inner terms
+	return unify (TermOp (t1), TermOp (t2), tl, callback);
+      }
+
+      return unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc);
+    }
+
+  /* tupling second
+     non-associative version ! TODO other version */
+  if (isTermTuple (t1))
+    {
+      int unify_combined_tup (Termlist tl)
+      {
+	// now the keys are unified (subst in this tl)
+	// and we try the inner terms
+	return unify (TermOp2 (t1), TermOp2 (t2), tl, callback);
+      }
+
+      return unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup);
+    }
+  return false;
+}
+
+
 //! Most general unifier.
 /**
  * Try to determine the most general unifier of two terms.

src/mgu.h

@@ -20,5 +20,6 @@ int termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist));
 int termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
 		    Termlist inverses, Termlist keylist);
 void termlistSubstReset (Termlist tl);
+int unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist));
 
 #endif

src/system.c

@@ -823,6 +823,11 @@ roleInstanceArachne (const System sys, const Protocol protocol,
 
   /* length */
   runs[rid].rolelength = roledef_length (runs[rid].start);
+  /* [[[ Hack ]]] this length is minimally 3 (to help the construction of the encryptors/decryptors from bare roledefs */
+  if (runs[rid].rolelength < 3)
+    {
+      runs[rid].rolelength = 3;
+    }
 
   /* new graph to create */
   dependPushRun (sys);

src/termlist.c

@@ -295,6 +295,29 @@ termlistConcat (Termlist tl1, Termlist tl2)
   return tl1;
 }
 
+//! Concatenates two termlists.
+/**
+ * Creates a completely new list that can be deleted.
+ *
+ * Note that the order is not preserved currently.
+ */
+Termlist
+termlistConcatStatic (Termlist tl1, Termlist tl2)
+{
+  Termlist tl, tls;
+
+  tl = NULL;
+  for (tls = tl1; tls != NULL; tls = tls->next)
+    {
+      tl = termlistAdd (tl, tls->term);
+    }
+  for (tls = tl2; tls != NULL; tls = tls->next)
+    {
+      tl = termlistAdd (tl, tls->term);
+    }
+  return tl;
+}
+
 //! Remove the pointed at element from the termlist.
 /**
  * Easier because of the double linked list. Note: does not do termDelete on the term.

src/termlist.h

@@ -36,6 +36,7 @@ Termlist termlistAdd (Termlist tl, Term term);
 Termlist termlistAppend (const Termlist tl, const Term term);
 Termlist termlistAddNew (const Termlist tl, const Term t);
 Termlist termlistConcat (Termlist tl1, Termlist tl2);
+Termlist termlistConcatStatic (Termlist tl1, Termlist tl2);
 Termlist termlistDelTerm (Termlist tl);
 Termlist termlistConjunct (Termlist tl1, Termlist tl2);
 Termlist termlistConjunctType (Termlist tl1, Termlist tl2, int termtype);