- Big change in the Arachne algorithm: decryptor sequences now get

expanded explicitly. This solves a long-standing issue with {k}k
  decryption to yield k. Needs some testing to ensure that it did not
  introduce any new errors.

src/arachne.c

@@ -7,6 +7,7 @@
  *
  */
 
+#include <stdlib.h>
 #include <limits.h>
 #include <float.h>
 #ifdef DEBUG
@@ -48,6 +49,7 @@ static int attack_length;
 Protocol INTRUDER;		// Pointers, to be set by the Init
 Role I_M;			// Same here.
 Role I_RRS;
+Role I_RRSD;
 
 static int indentDepth;
 static int proofDepth;
@@ -125,6 +127,15 @@ arachneInit (const System mysys)
   add_event (SEND, NULL);
   I_RRS = add_role ("I_E: Encrypt");
 
+  add_event (READ, NULL);
+  add_event (READ, NULL);
+  add_event (SEND, NULL);
+  I_RRSD = add_role ("I_D: Decrypt");
+
+  num_regular_runs = 0;
+  num_intruder_runs = 0;
+  max_encryption_level = 0;
+
   return;
 }
 
@@ -621,9 +632,76 @@ iterate_role_sends (int (*func) ())
   return iterate_role_events (send_wrapper);
 }
 
+//! Create decryption role instance
+/**
+ * Note that this does not add any bindings for the reads.
+ *
+ *@param term	The term to be decrypted (implies decryption key)
+ *
+ *@returns The run id of the decryptor instance
+ */
+int
+create_decryptor (const Term term, const Term key)
+{
+  if (term != NULL && isTermEncrypt (term))
+    {
+      Roledef rd;
+      Term tempkey;
+      int run;
+
+      run = semiRunCreate (INTRUDER, I_RRSD);
+      rd = sys->runs[run].start;
+      rd->message = termDuplicateUV (term);
+      rd->next->message = termDuplicateUV (key);
+      rd->next->next->message = termDuplicateUV (TermOp (term));
+      sys->runs[run].step = 3;
+      proof_suppose_run (run, 0, 3);
+
+      return run;
+    }
+  else
+    {
+      globalError++;
+      printf ("Term for which a decryptor instance is requested: ");
+      termPrint (term);
+      printf ("\n");
+      error
+	("Trying to build a decryptor instance for a non-encrypted term.");
+    }
+}
+
+//! Get the priority level of a key that is needed for a term (typical pk/sk distinction)
+int
+getPriorityOfNeededKey (const System sys, const Term keyneeded)
+{
+  int prioritylevel;
+
+  /* Normally, a key gets higher priority, but unfortunately this is not propagated at the moment. Maybe later.
+   */
+  prioritylevel = 1;
+  if (realTermEncrypt (keyneeded))
+    {
+      /* the key is a construction itself */
+      if (inKnowledge (sys->know, TermKey (keyneeded)))
+	{
+	  /* the key is constructed by a public thing */
+	  /* typically, this is a public key, so we postpone it  */
+	  prioritylevel = -1;
+	}
+    }
+  return prioritylevel;
+}
+
 //! Try to bind a specific existing run to a goal.
 /**
  * The key goals are bound to the goal.
+ *
+ *@todo This is currently NOT correct. The point is that the key chain
+ * cannot uniquely define a path through a term in general, and
+ * a rewrite of termMguSubterm is needed. It should not yield the
+ * needed keys, but simply the path throught the term. This would enable
+ * reconstruction of the keys anyway. TODO
+ *      
  *@param subterm determines whether it is a subterm unification or not.
  */
 int
@@ -635,7 +713,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
   int newgoals;
   int found;
 
-  int subterm_iterate (Termlist substlist, Termlist keylist)
+  int subterm_iterate (Termlist substlist, Termlist cryptlist)
   {
     int flag;
 
@@ -644,56 +722,149 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
     /**
      * Now create the new bindings
      */
-    if (goal_bind (b, run, index))
-      {
     int newgoals;
-	Termlist tl;
+    int newruns;
+    int stillvalid;
 
-	proof_suppose_binding (b);
+    Binding smalltermbinding;
-	if (keylist != NULL && sys->output == PROOF)
+
+    stillvalid = true;		// New stuff is valid (no cycles)
+    newgoals = 0;		// No new goals introduced (yet)
+    newruns = 0;		// New runs introduced
+    smalltermbinding = b;	// Start off with destination binding
+
+#ifdef DEBUG
+    if (DEBUGL (4))
+      {
+	printf ("Trying to bind the small term ");
+	termPrint (b->term);
+	printf (" as coming from the big send ");
+	termPrint (rd->message);
+	printf (" , binding ");
+	termPrint (b->term);
+	printf ("\nCrypted list needed: ");
+	termlistPrint (cryptlist);
+	printf ("\n");
+      }
+#endif
+    if (cryptlist != NULL && sys->output == PROOF)
       {
 	indentPrint ();
 	eprintf
-	      ("This introduces the obligation to produce the following keys: ");
+	  ("This introduces the obligation to decrypted the following encrypted subterms: ");
-	    termlistPrint (keylist);
+	termlistPrint (cryptlist);
 	eprintf ("\n");
       }
-	newgoals = 0;
+
-	tl = keylist;
+    /* The order of the cryptlist is inner -> outer */
-	while (tl != NULL)
+    while (stillvalid && cryptlist != NULL && smalltermbinding != NULL)
       {
-	    int keyrun;
+	/*
+	 * Invariants:
+	 *
+	 * smalltermbinding     binding to be satisfied next (and for which a decryptor is needed)
+	 */
+	Term keyneeded;
 	int prioritylevel;
+	int smallrun;
+	int count;
+	Roledef rddecrypt;
+	Binding bnew;
+	int res;
 
-	    /* normally, a key gets higher priority */
+	/*
-	    prioritylevel = 1;
+	 * 1. Add decryptor
-	    if (realTermEncrypt (tl->term))
+	 */
+
+	keyneeded =
+	  inverseKey (sys->know->inverses, TermKey (cryptlist->term));
+	prioritylevel = getPriorityOfNeededKey (sys, keyneeded);
+	smallrun = create_decryptor (cryptlist->term, keyneeded);
+	rddecrypt = sys->runs[smallrun].start;
+	termDelete (keyneeded);
+	newruns++;
+
+	/*
+	 * 2. Add goal bindings
+	 */
+
+	count = goal_add (rddecrypt->message, smallrun, 0, 0);
+	newgoals = newgoals + count;
+	if (count >= 0)
 	  {
-		/* the key is a construction itself */
+	    if (count > 1)
-		if (inKnowledge (sys->know, TermKey (tl->term)))
 	      {
-		    /* the key is constructed by a public thing */
+		error
-		    /* typically, this is a public key, so we postpone it  */
+		  ("Added more than one goal for decryptor goal 1, weird.");
-		    prioritylevel = -1;
+	      }
+	    else
+	      {
+		// This is the unique new goal then
+		bnew = (Binding) sys->bindings->data;
 	      }
 	  }
-	    /* add the key as a goal */
+	else
+	  {
+	    // No new binding? Weird, but fair enough
+	    bnew = NULL;
+	  }
 	newgoals =
-	      newgoals + goal_add (tl->term, b->run_to, b->ev_to,
+	  newgoals + goal_add (rddecrypt->next->message, smallrun, 1,
 			       prioritylevel);
-	    tl = tl->next;
+
+	/*
+	 * 3. Bind open goal to decryptor
+	 */
+
+	res = goal_bind (smalltermbinding, smallrun, 2);	// returns 0 iff invalid
+	if (res != 0)
+	  {
+	    // Allright, good binding, proceed with next
+	    smalltermbinding = bnew;
+	  }
+	else
+	  {
+	    stillvalid = false;
 	  }
 
+	/* progression */
+	cryptlist = cryptlist->next;
+      }
+
+    /*
+     * Decryptors for any nested keys have been added. Now we can fill the
+     * final binding.
+     */
+
+    if (stillvalid)
+      {
+	if (goal_bind (smalltermbinding, run, index))
+	  {
+	    proof_suppose_binding (b);
+#ifdef DEBUG
+	    if (DEBUGL (4))
+	      {
+		indentPrint ();
+		eprintf ("Added %i new goals, iterating.\n", newgoals);
+	      }
+#endif
+	    /* Iterate process */
 	    indentDepth++;
 	    flag = flag && iterate ();
 	    indentDepth--;
-
-	goal_remove_last (newgoals);
 	  }
 	else
 	  {
 	    proof_cannot_bind (b, run, index);
 	  }
+      }
+
+    goal_remove_last (newgoals);
+    while (newruns > 0)
+      {
+	semiRunDestroy ();
+	newruns--;
+      }
     goal_unbind (b);
     return flag;
   }
@@ -2754,7 +2925,8 @@ prune_claim_specifics ()
     {
       if (arachne_claim_niagree (sys, 0, sys->current_claim->ev))
 	{
-	  sys->current_claim->count = statesIncrease (sys->current_claim->count);
+	  sys->current_claim->count =
+	    statesIncrease (sys->current_claim->count);
 	  if (sys->output == PROOF)
 	    {
 	      indentPrint ();
@@ -2768,7 +2940,8 @@ prune_claim_specifics ()
     {
       if (arachne_claim_nisynch (sys, 0, sys->current_claim->ev))
 	{
-	  sys->current_claim->count = statesIncrease (sys->current_claim->count);
+	  sys->current_claim->count =
+	    statesIncrease (sys->current_claim->count);
 	  if (sys->output == PROOF)
 	    {
 	      indentPrint ();

src/binding.c

@@ -47,7 +47,7 @@ binding_create (Term term, int run_to, int ev_to)
   b->ev_from = -1;
   b->run_to = run_to;
   b->ev_to = ev_to;
-  goal_graph_destroy();
+  goal_graph_destroy ();
   b->term = term;
   b->level = 0;
   return b;
@@ -104,13 +104,13 @@ goal_graph_destroy ()
       struct mallinfo mi_free;
       int mem_free;
 
-      mi_free = mallinfo();
+      mi_free = mallinfo ();
       mem_free = mi_free.uordblks;
 #endif
       memFree (graph, (nodes * nodes) * sizeof (int));
       graph = NULL;
 #ifdef DEBUG
-      mi_free = mallinfo();
+      mi_free = mallinfo ();
       if (mem_free - mi_free.uordblks != graph_uordblks)
 	error ("Freeing gave a weird result.");
 #endif
@@ -137,11 +137,13 @@ goal_graph_create ()
     int create_mem_before;
 
     if (graph_uordblks != 0)
-	  error ("Trying to create graph stuff without 0 uordblks for it first, but it is %i.", graph_uordblks);
+      error
-      create_mi = mallinfo();
+	("Trying to create graph stuff without 0 uordblks for it first, but it is %i.",
+	 graph_uordblks);
+    create_mi = mallinfo ();
     create_mem_before = create_mi.uordblks;
     graph = memAlloc ((nodes * nodes) * sizeof (int));
-      create_mi = mallinfo();
+    create_mi = mallinfo ();
     graph_uordblks = create_mi.uordblks - create_mem_before;
   }
 
@@ -270,15 +272,17 @@ goal_graph_create ()
 							    // It's read here first.
 							    // Order and be done with it.
 							    graph[graph_nodes
-								    (nodes, run2,
+								  (nodes,
-								     ev2, run,
+								   run2, ev2,
-								     ev)] = 1;
+								   run, ev)] =
+							      1;
 #ifdef DEBUG
 							    if (DEBUGL (5))
 							      {
 								eprintf
 								  ("* [local originator] term ");
-								  termPrint (t2);
+								termPrint
+								  (t2);
 								eprintf
 								  (" is bound using %i, %i before %i,%i\n",
 								   run2, ev2,
@@ -295,7 +299,8 @@ goal_graph_create ()
 							      {
 								eprintf
 								  ("Term ");
-								  termPrint (t2);
+								termPrint
+								  (t2);
 								eprintf
 								  (" from run %i occurs in run %i, term ",
 								   run2, run);
@@ -310,8 +315,9 @@ goal_graph_create ()
 								// This forces a loop, and thus prunes
 								graph
 								  [graph_nodes
-								     (nodes, 0, 1,
+								   (nodes, 0,
-								      0, 0)] = 1;
+								    1, 0,
+								    0)] = 1;
 							      }
 							  }
 						      }
@@ -432,9 +438,6 @@ binding_print (const Binding b)
 int
 goal_add (Term term, const int run, const int ev, const int level)
 {
-  int sum;
-
-  sum = 0;
   term = deVar (term);
 #ifdef DEBUG
   if (term == NULL)
@@ -447,8 +450,7 @@ goal_add (Term term, const int run, const int ev, const int level)
 #endif
   if (realTermTuple (term))
     {
-      sum = sum + 
+      return goal_add (TermOp1 (term), run, ev, level) +
-	  goal_add (TermOp1 (term), run, ev, level) + 
 	goal_add (TermOp2 (term), run, ev, level);
     }
   else
@@ -479,17 +481,67 @@ goal_add (Term term, const int run, const int ev, const int level)
 	  b = binding_create (term, run, ev);
 	  b->level = level;
 	  sys->bindings = list_insert (sys->bindings, b);
-	  sum = sum + 1;
+#ifdef DEBUG
+	  if (DEBUGL (3))
+	    {
+	      eprintf ("Adding new binding for ");
+	      termPrint (term);
+	      eprintf (" to run %i, ev %i.\n", run, ev);
+	    }
+#endif
+	  return 1;
 	}
     }
-  return sum;
+  return 0;
+}
+
+//! Add a goal, and bind it immediately.
+// If the result is negative, no goals will have been added, as the resulting state must be pruned (cycle) */
+int
+goal_add_fixed (Term term, const int run, const int ev, const int fromrun,
+		const int fromev)
+{
+  int newgoals, n;
+  List l;
+  int res;
+
+  newgoals = goal_add (term, run, ev, 0);
+  l = sys->bindings;
+  n = newgoals;
+  res = 1;
+  while (res != 0 && n > 0 && l != NULL)
+    {
+      Binding b;
+
+      b = (Binding) l->data;
+      if (b->done)
+	{
+	  globalError++;
+	  binding_print (b);
+	  error (" problem with new fixed binding!");
+	}
+      res = goal_bind (b, fromrun, fromev);	// returns 0 if it must be pruned
+      l = l->next;
+      n--;
+    }
+  if (res != 0)
+    {
+      return newgoals;
+    }
+  else
+    {
+      goal_remove_last (newgoals);
+      return -1;
+    }
 }
 
 //! Remove a goal
 void
 goal_remove_last (int n)
 {
-  while (n > 0 && (sys->bindings != NULL))
+  while (n > 0)
+    {
+      if (sys->bindings != NULL)
 	{
 	  Binding b;
 
@@ -498,6 +550,13 @@ goal_remove_last (int n)
 	  sys->bindings = list_delete (sys->bindings);
 	  n--;
 	}
+      else
+	{
+	  error
+	    ("goal_remove_last error: trying to remove %i too many bindings.",
+	     n);
+	}
+    }
 }
 
 //! Bind a goal (0 if it must be pruned)
@@ -522,6 +581,8 @@ goal_bind (const Binding b, const int run, const int ev)
     }
   else
     {
+      globalError++;
+      binding_print (b);
       error ("Trying to bind a bound goal again.");
     }
 }
@@ -545,7 +606,8 @@ goal_unbind (const Binding b)
 /**
  * Especially made for tuple expansion
  */
-int binding_block (Binding b)
+int
+binding_block (Binding b)
 {
   if (!b->blocked)
     {
@@ -559,7 +621,8 @@ int binding_block (Binding b)
 }
 
 //! Unblock a binding
-int binding_unblock (Binding b)
+int
+binding_unblock (Binding b)
 {
   if (b->blocked)
     {
@@ -630,7 +693,8 @@ labels_ordered (Termmap runs, Termlist labels)
 }
 
 //! Check whether the binding denotes a sensible thing such that we can use run_from and ev_from
-int valid_binding (Binding b)
+int
+valid_binding (Binding b)
 {
   if (b->done && !b->blocked)
     return 1;
@@ -656,7 +720,19 @@ bindings_c_minimal ()
       // Recompute closure; does that work?
       if (!warshall (graph, nodes))
 	{
-	  // Hmm, cycle
+	  List l;
+
+	  globalError++;
+	  l = sys->bindings;
+	  while (l != NULL)
+	    {
+	      Binding b;
+
+	      b = (Binding) l->data;
+	      binding_print (b);
+	      eprintf ("\n");
+	      l = l->next;
+	    }
 	  error ("Detected a cycle when testing for c-minimality");
 	}
     }
@@ -669,7 +745,7 @@ bindings_c_minimal ()
 
       b = (Binding) bl->data;
       // Check for a valid binding; it has to be 'done' and sensibly bound (not as in tuple expanded stuff)
-      if (valid_binding(b))
+      if (valid_binding (b))
 	{
 	  int run;
 	  int node_from;

src/binding.h

@@ -43,6 +43,8 @@ int binding_print (Binding b);
 int valid_binding (Binding b);
 
 int goal_add (Term term, const int run, const int ev, const int level);
+int goal_add_fixed (Term term, const int run, const int ev, const int fromrun,
+		    const int fromev);
 void goal_remove_last (int n);
 int goal_bind (const Binding b, const int run, const int ev);
 void goal_unbind (const Binding b);

src/compiler.c

@@ -1018,9 +1018,13 @@ order_label_roles (const Claimlist cl)
       int scan_label (void *data)
       {
 	Labelinfo linfo;
+	Termlist tl;
 
 	linfo = (Labelinfo) data;
-	if (inTermlist (cl->prec, linfo->label))
+	if (linfo == NULL)
+	  return 1;
+	tl = cl->prec;
+	if (inTermlist (tl, linfo->label))
 	  {
 	    if (linfo->protocol == cl->protocol)
 	      {

src/mgu.c

@@ -104,8 +104,7 @@ goodsubst (Term tvar, Term tsubst)
       else
 	{
 	  // It's a leaf, but what type?
-	  if (mgu_match == 1
+	  if (mgu_match == 1 || compatibleTypes ())
-	      || compatibleTypes ())
 	    {
 	      return 1;
 	    }
@@ -305,68 +304,69 @@ termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist))
   return flag;
 }
 
-//! Most general subterm unifiers of t1 subterm t2
+//! Most general subterm unifiers of smallterm subterm bigterm
 /**
  * Try to determine the most general subterm unifiers of two terms.
- *@returns Nothing. Iteration gets termlist of subst, and list of keys needed to decrypt.
+ *@returns Nothing. Iteration gets termlist of subst, and list of keys needed
+ *  to decrypt. This termlist does not need to be deleted, because it is handled
+ *  by the mguSubTerm itself.
  */
 int
-termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
+termMguSubTerm (Term smallterm, Term bigterm,
-		Termlist inverses, Termlist keylist)
+		int (*iterator) (Termlist, Termlist), Termlist inverses,
+		Termlist cryptlist)
 {
   int flag;
 
   flag = 1;
-  t1 = deVar (t1);
+  smallterm = deVar (smallterm);
-  t2 = deVar (t2);
+  bigterm = deVar (bigterm);
-  if (t2 != NULL)
+  if (bigterm != NULL)
     {
       Termlist tl;
 
-      if (!realTermLeaf (t2))
+      if (!realTermLeaf (bigterm))
 	{
-	  if (realTermTuple (t2))
+	  if (realTermTuple (bigterm))
 	    {
 	      // 'simple' tuple
 	      flag =
-		flag && termMguSubTerm (t1, TermOp1 (t2), iterator, inverses,
+		flag
-					keylist);
+		&& termMguSubTerm (smallterm, TermOp1 (bigterm), iterator,
-	      flag =
+				   inverses, cryptlist);
-		flag && termMguSubTerm (t1, TermOp2 (t2), iterator, inverses,
+	      flag = flag
-					keylist);
+		&& termMguSubTerm (smallterm, TermOp2 (bigterm), iterator,
+				   inverses, cryptlist);
 	    }
 	  else
 	    {
 	      // Must be encryption
-	      // So, we need the key, and try to get the rest
+	      Term keyneeded;
-	      Term newkey;
 
-	      newkey = inverseKey (inverses, TermKey (t2));
+	      keyneeded = inverseKey (inverses, TermKey (bigterm));
 	      // We can never produce the TERM_Hidden key, thus, this is not a valid iteration.
-	      if (!isTermEqual (newkey, TERM_Hidden))
+	      if (!isTermEqual (keyneeded, TERM_Hidden))
 		{
-		  Termlist keylist_new;
+		  cryptlist = termlistAdd (cryptlist, bigterm);	// Append, so the last encrypted term in the list is the most 'inner' one, and the first is the outer one.
-
-		  keylist_new = termlistShallow (keylist);
-		  keylist_new = termlistAdd (keylist_new, newkey);
 
 		  // Recurse
 		  flag =
 		    flag
-		    && termMguSubTerm (t1, TermOp (t2), iterator, inverses,
+		    && termMguSubTerm (smallterm, TermOp (bigterm), iterator,
-				       keylist_new);
+				       inverses, cryptlist);
 
-		  termlistDelete (keylist_new);
+
+		  cryptlist = termlistDelTerm (cryptlist);
 		}
-	      termDelete (newkey);
+	      termDelete (keyneeded);
 	    }
 	}
       // simple clause or combined
-      tl = termMguTerm (t1, t2);
+      tl = termMguTerm (smallterm, bigterm);
       if (tl != MGUFAIL)
 	{
 	  // Iterate
-	  flag = flag && iterator (tl, keylist);
+	  flag = flag && iterator (tl, cryptlist);
 	  // Reset variables
 	  termlistSubstReset (tl);
 	  // Remove list
@@ -375,7 +375,7 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
     }
   else
     {
-      if (t1 != NULL)
+      if (smallterm != NULL)
 	{
 	  flag = 0;
 	}

src/system.c

@@ -101,6 +101,7 @@ systemInit ()
   sys->roleeventmax = 0;
   sys->claimlist = NULL;
   sys->labellist = NULL;
+  sys->match = 0;		// default matching
 
   /* matching CLP */
   sys->constraints = NULL;	// no initial constraints

src/term.c

@@ -683,7 +683,7 @@ tupleCount (Term tt)
 //! Yield the projection Pi(n) of a term.
 /**
  *@param tt Term
- *@param n The index in the tuple.
+ *@param n The index in the tuple [0..tupleCount-1]
  *@return Returns either a pointer to a term, or NULL if the index is out of range.
  *\sa tupleCount()
  */
@@ -1085,7 +1085,7 @@ term_encryption_level (const Term term)
     if (t == NULL)
       {
 #ifdef DEBUG
-	if (DEBUGL(2))
+	if (DEBUGL (2))
 	  {
 	    eprintf ("Warning: Term encryption level finds a NULL for term ");
 	    termPrint (term);

src/termlist.c

@@ -272,7 +272,8 @@ termlistConcat (Termlist tl1, Termlist tl2)
 
 //! Remove the pointed at element from the termlist.
 /**
- * Easier because of the double linked list.
+ * Easier because of the double linked list. Note: does not do termDelete on the term.
+ *
  *@param tl The pointer to the termlist node to be deleted from the list.
  *@return The possibly new head pointer to the termlist.
  */
@@ -667,8 +668,7 @@ termlistLocal (Termlist tl, const Termlist fromlist, const Termlist tolist)
 
   while (tl != NULL)
     {
-      newtl =
+      newtl = termlistAdd (newtl, termLocal (tl->term, fromlist, tolist));
-	termlistAdd (newtl, termLocal (tl->term, fromlist, tolist));
       tl = tl->next;
     }
   return newtl;