- Added '--concrete' switch to fill in to pick readable names for

variables.

src/arachne.c

@@ -3260,6 +3260,210 @@ count_false ()
   sys->current_claim->failed = statesIncrease (sys->current_claim->failed);
 }
 
+//! Create a generic new term of the same type, with a new run identifier.
+/**
+ * Output: the first element of the returned list.
+ */
+Termlist
+createNewTermGeneric (Termlist tl, Term t)
+{
+  int freenumber;
+  Termlist tlscan;
+  Term newterm;
+
+  /* Determine first free number */
+  freenumber = 0;
+  tlscan = tl;
+  while (tlscan != NULL)
+    {
+      Term ts;
+
+      ts = tlscan->term;
+      if (isLeafNameEqual (t, ts))
+	{
+	  if (TermRunid (ts) >= freenumber)
+	    {
+	      freenumber = TermRunid (ts) + 1;
+	    }
+	}
+      tlscan = tlscan->next;
+    }
+
+  /* Make a new term with the free number */
+  newterm = (Term) memAlloc (sizeof (struct term));
+  memcpy (newterm, t, sizeof (struct term));
+  TermRunid (newterm) = freenumber;
+
+  /* return */
+  return termlistPrepend (tl, newterm);
+}
+
+//! Create a new term with incremented run rumber, starting at sys->maxruns.
+/**
+ * Output: the first element of the returned list.
+ */
+Termlist
+createNewTerm (Termlist tl, Term t, int isagent)
+{
+  /* Does if have an explicit type?
+   * If so, we try to find a fresh name from the intruder knowledge first.
+   */
+  if (isagent)
+    {
+      Termlist knowlist;
+      Termlist kl;
+
+      knowlist = knowledgeSet (sys->know);
+      kl = knowlist;
+      while (kl != NULL)
+	{
+	  Term k;
+
+	  k = kl->term;
+	  if (isAgentType (k->stype))
+	    {
+	      /* agent */
+	      /* We don't want to instantiate untrusted agents. */
+	      if (!inTermlist (sys->untrusted, k))
+		{
+		  /* trusted agent */
+		  if (!inTermlist (tl, k))
+		    {
+		      /* This agent name is not in the list yet. */
+		      return termlistPrepend (tl, k);
+		    }
+		}
+	    }
+	  kl = kl->next;
+	}
+      termlistDelete (knowlist);
+    }
+
+  /* Not an agent or no free one found */
+  return createNewTermGeneric (tl, t);
+}
+
+//! Delete a term made in the previous constructions
+void
+deleteNewTerm (Term t)
+{
+  if (TermRunid (t) >= 0)
+    {
+      /* if it has a positive runid, it did not come from the intruder
+       * knowledge, so it must have been constructed.
+       */
+      memFree (t, sizeof (struct term));
+    }
+}
+
+//! Make a trace concrete
+Termlist
+makeTraceConcrete (const System sys)
+{
+  Termlist changedvars;
+  Termlist tlnew;
+  int run;
+
+  changedvars = NULL;
+  tlnew = NULL;
+  run = 0;
+
+  while (run < sys->maxruns)
+    {
+      Termlist tl;
+
+      tl = sys->runs[run].locals;
+      while (tl != NULL)
+	{
+	  /* variable, and of some run? */
+	  if (isTermVariable (tl->term) && TermRunid (tl->term) >= 0)
+	    {
+	      Term var;
+	      Term name;
+	      Termlist vartype;
+
+	      var = deVar (tl->term);
+	      vartype = var->stype;
+	      // Determine class name
+	      if (vartype != NULL)
+		{
+		  // Take first type name
+		  name = vartype->term;
+		}
+	      else
+		{
+		  // Just a generic name
+		  name = TERM_Data;
+		}
+	      // We should turn this into an actual term
+	      tlnew = createNewTerm (tlnew, name, isAgentType (var->stype));
+	      var->subst = tlnew->term;
+
+	      // Store for undo later
+	      changedvars = termlistAdd (changedvars, var);
+	    }
+	  tl = tl->next;
+	}
+      run++;
+    }
+  termlistDelete (tlnew);
+  return changedvars;
+}
+
+//! Make a trace a class again
+void
+makeTraceClass (const System sys, Termlist varlist)
+{
+  Termlist tl;
+
+  tl = varlist;
+  while (tl != NULL)
+    {
+      Term var;
+
+      var = tl->term;
+      deleteNewTerm (var->subst);
+      var->subst = NULL;
+
+      tl = tl->next;
+    }
+  termlistDelete (varlist);
+}
+
+//! Output an attack in the desired way
+void
+arachneOutputAttack ()
+{
+  Termlist varlist;
+
+  if (switches.concrete)
+    {
+      varlist = makeTraceConcrete (sys);
+    }
+  else
+    {
+      varlist = NULL;
+    }
+
+  if (switches.xml)
+    {
+      xmlOutSemitrace (sys);
+    }
+  else
+    {
+      if (switches.latex == 1)
+	{
+	  latexSemiState ();
+	}
+      else
+	{
+	  dotSemiState ();
+	}
+    }
+
+  makeTraceClass (sys, varlist);
+}
+
 //------------------------------------------------------------------------
 // Main logic core
 //------------------------------------------------------------------------
@@ -3283,21 +3487,7 @@ property_check ()
   count_false ();
   if (switches.output == ATTACK)
     {
-      if (switches.xml)
-	{
-	  xmlOutSemitrace (sys);
-	}
-      else
-	{
-	  if (switches.latex == 1)
-	    {
-	      latexSemiState ();
-	    }
-	  else
-	    {
-	      dotSemiState ();
-	    }
-	}
+      arachneOutputAttack ();
     }
   // Store attack length if shorter
   attack_this = get_semitrace_length ();

src/specialterm.c

@@ -19,6 +19,7 @@ Term TERM_Hidden;
 Term TERM_Type;
 Term TERM_Nonce;
 Term TERM_Ticket;
+Term TERM_Data;
 
 Term TERM_Claim;
 Term CLAIM_Secret;
@@ -43,6 +44,7 @@ specialTermInit (const System sys)
   langcons (TERM_Function, "Function", TERM_Type);
   langcons (TERM_Nonce, "Nonce", TERM_Type);
   langcons (TERM_Ticket, "Ticket", TERM_Type);
+  langcons (TERM_Data, "Data", TERM_Type);
 
   langcons (CLAIM_Secret, "Secret", TERM_Claim);
   langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim);

src/specialterm.h

@@ -11,6 +11,7 @@ extern Term TERM_Hidden;
 extern Term TERM_Type;
 extern Term TERM_Nonce;
 extern Term TERM_Ticket;
+extern Term TERM_Data;
 
 extern Term TERM_Claim;
 extern Term CLAIM_Secret;

src/switches.c

@@ -67,6 +67,7 @@ switchesInit (int argc, char **argv)
   switches.arachneSelector = 3;	// default goal selection method
   switches.maxIntruderActions = INT_MAX;	// max number of encrypt/decrypt events
   switches.agentTypecheck = 1;	// default do check agent types
+  switches.concrete = false;	// default leaves variables in output to yield class
 
   // Misc
   switches.switchP = 0;		// multi-purpose parameter
@@ -291,7 +292,8 @@ switcher (const int process, int index)
     {
       if (!process)
 	{
-	  helptext ("-M,--modelchecker", "select Model checking engine [Arachne]");
+	  helptext ("-M,--modelchecker",
+		    "select Model checking engine [Arachne]");
 	}
       else
 	{
@@ -318,7 +320,8 @@ switcher (const int process, int index)
     {
       if (!process)
 	{
-	  helptext ("-m,--match=<int>", "matching method [0] (0:Typed,1:Basic,2:Typeless)");
+	  helptext ("-m,--match=<int>",
+		    "matching method [0] (0:Typed,1:Basic,2:Typeless)");
 	}
       else
 	{
@@ -405,11 +408,12 @@ switcher (const int process, int index)
       if (!process)
 	{
 	  helptext ("-H,--human-readable",
-		    "try to make the output human-friendly (e.g. in XML)");
+		    "try to make the output human-friendly (e.g. in XML). Implies --concrete.");
 	}
       else
 	{
 	  switches.human = true;
+	  switches.concrete = true;
 	  return index;
 	}
     }
@@ -588,6 +592,19 @@ switcher (const int process, int index)
 	}
     }
 
+  if (detect (' ', "concrete", 0))
+    {
+      if (!process)
+	{
+	  /* maybe add after testing */
+	}
+      else
+	{
+	  switches.concrete = true;
+	  return index;
+	}
+    }
+
 #ifdef DEBUG
   /* ==================
    *  Experimental options

src/switches.h

@@ -46,6 +46,7 @@ struct switchdata
   int arachneSelector;		//!< Goal selection method for Arachne engine
   int maxIntruderActions;	//!< Maximum number of intruder actions in the semitrace (encrypt/decrypt)
   int agentTypecheck;		//!< Check type of agent variables in all matching modes
+  int concrete;			//!< Swap out variables at the end.
 
   // Misc
   int switchP;			//!< A multi-purpose integer parameter, passed to the partial order reduction method selected.

src/term.c

@@ -470,7 +470,7 @@ termNodeDuplicate (const Term term)
 
 //! Make a true deep copy of a term.
 /**
- * Currently, it this function is not to be used, so we can be sure leaf nodes occur only once in the system.
+ * Currently, this function is not to be used, so we can be sure leaf nodes occur only once in the system.
  *@return New memory is allocated and the node is copied recursively.
  *\sa termDuplicate()
  */
@@ -1329,3 +1329,10 @@ termPrintDiff (Term t1, Term t2)
 	}
     }
 }
+
+//! Test two leaf terms for abstract equality (abstracting from the run identifiers)
+int
+isLeafNameEqual (Term t1, Term t2)
+{
+  return (TermSymb (t1) == TermSymb (t2));
+}

src/term.h

@@ -195,5 +195,6 @@ int term_encryption_level (const Term term);
 float term_constrain_level (const Term term);
 void term_set_keylevels (const Term term);
 void termPrintDiff (Term t1, Term t2);
+int isLeafNameEqual (Term t1, Term t2);
 
 #endif

src/termlist.h

@@ -32,6 +32,7 @@ __inline__ int inTermlist (Termlist tl, const Term term);
 __inline__ Termlist termlistFind (Termlist tl, const Term term);
 int isTermlistEqual (Termlist tl1, Termlist tl2);
 Termlist termlistAdd (Termlist tl, Term term);
+#define termlistPrepend(tl,t) termlistAdd(tl,t)
 Termlist termlistAppend (const Termlist tl, const Term term);
 Termlist termlistAddNew (const Termlist tl, const Term t);
 Termlist termlistConcat (Termlist tl1, Termlist tl2);

src/xmlout.c

@@ -26,6 +26,7 @@
  * Externally defined
  */
 extern Protocol INTRUDER;	// from arachne.c
+extern Term TERM_Data;		// from specialterm.c
 
 /*
  * Global/static stuff.
@@ -328,19 +329,19 @@ xmlTermType (const Term t)
     }
 
   xmlindent++;
-  xmlPrint("<term>");
+  xmlPrint ("<term>");
   xmlindent++;
   xmlIndentPrint ();
   xmlTermPrint (t);
   printf ("\n");
   xmlindent--;
-  xmlPrint("</term>");
+  xmlPrint ("</term>");
 
-  xmlPrint("<type>");
+  xmlPrint ("<type>");
   xmlindent++;
   xmlTermlistPrint (t->stype);
   xmlindent--;
-  xmlPrint("</type>");
+  xmlPrint ("</type>");
   xmlindent--;
 
   if (realTermVariable (t))
@@ -373,9 +374,9 @@ xmlVariable (const System sys, const Term variable, const int run)
       xmlPrint ("</name>");
       if (variable->subst != NULL)
 	{
-          xmlPrint ("<substitution>");
+	  xmlPrint ("<substitution>");
 	  xmlTermType (deVar (variable));
-          xmlPrint ("</substitution>");
+	  xmlPrint ("</substitution>");
 	}
       xmlindent--;
       xmlPrint ("</variable>");
@@ -902,7 +903,6 @@ xmlOutRuns (const System sys)
     }
 }
 
-
 /*
  * -----------------------------------------------------------------------------------
  * Publicly available functions