- Added Ticket basic term type. Note that this only has consequences for

the Arachne type checking. The net result is that a variable of type
  'Ticket' can always contain any term, even with -m0 or -m1 matching.

src/arachne.c

@@ -30,6 +30,7 @@
 #include "binding.h"
 #include "warshall.h"
 #include "timer.h"
+#include "type.h"
 
 extern Term CLAIM_Secret;
 extern Term CLAIM_Nisynch;
@@ -2650,6 +2651,18 @@ prune_theorems ()
   List bl;
   int run;
 
+  // Check all types of the local agents according to the matching type
+  if (!checkTypeLocals (sys))
+    {
+      if (sys->output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf
+	    ("Pruned because some local variable was incorrectly subsituted.\n");
+	}
+      return 1;
+    }
+
   // Check if all agents are agents (!)
   run = 0;
   while (run < sys->maxruns)

src/compiler.c

@@ -57,6 +57,7 @@ Term TERM_Function;
 Term TERM_Hidden;
 Term TERM_Type;
 Term TERM_Nonce;
+Term TERM_Ticket;
 
 Term TERM_Claim;
 Term CLAIM_Secret;
@@ -101,6 +102,7 @@ compilerInit (const System mysys)
   langcons (TERM_Agent, "Agent", TERM_Type);
   langcons (TERM_Function, "Function", TERM_Type);
   langcons (TERM_Nonce, "Nonce", TERM_Type);
+  langcons (TERM_Ticket, "Ticket", TERM_Type);
 
   langcons (CLAIM_Secret, "Secret", TERM_Claim);
   langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim);

src/mgu.c

@@ -5,6 +5,7 @@
 #include "substitution.h"
 #include "mgu.h"
 #include "memory.h"
+#include "type.h"
 
 /*
    Most General Unifier
@@ -14,17 +15,24 @@
    New version yields a termlist with substituted variables, which can later be reset to NULL.
 */
 
-//! Global constant. If true, typed checking
+//! Internal constant. If true, typed checking
 /**
  * Analoguous to sys->match
  * 0	typed
  * 1	basic typeflaws
  * 2	all typeflaws
  */
-int mgu_match = 0;
+static int mgu_match = 0;
 
 extern Term TERM_Hidden;
 
+//! Set mgu mode (basically sys->match)
+void
+setMguMode (const int match)
+{
+  mgu_match = match;
+}
+
 void
 showSubst (Term t)
 {
@@ -58,76 +66,16 @@ showSubst (Term t)
 __inline__ int
 goodsubst (Term tvar, Term tsubst)
 {
-  // function to test compatibility
-  __inline__ int compatibleTypes ()
-  {
-    if (tvar->stype == NULL)
-      {
-	// If the variable type is unspecified, anything goes
-	return 1;
-      }
-    else
-      {
-	// There are variable types.
-	// At least one of them should match a type of the constant.
-	Termlist tl;
+  Term tbuf;
+  int res;
 
-	tl = tvar->stype;
-	while (tl != NULL)
-	  {
-	    if (inTermlist (tsubst->stype, tl->term))
-	      {
-		// One type matches
-		return 1;
-	      }
-	    tl = tl->next;
-	  }
-	// No matches
-	return 0;
-      }
-  }
+  tbuf = tvar->subst;
+  tvar->subst = tsubst;
 
-  if (mgu_match == 2)
-    {
-      return 1;
-    }
-  else
-    {
-      /**
-       * Check if each type of the substitution is allowed in the variable
-       */
-      if (!realTermLeaf (tsubst))
-	{
-	  // Typed var cannot match with non-leaf
-	  return 0;
-	}
-      else
-	{
-	  // It's a leaf, but what type?
-	  if (mgu_match == 1 || compatibleTypes ())
-	    {
-	      return 1;
-	    }
-	  else
-	    {
-#ifdef DEBUG
-	      if (DEBUGL (5))
-		{
-		  eprintf ("Substitution fails on ");
-		  termPrint (tvar);
-		  eprintf (" -/-> ");
-		  termPrint (tsubst);
-		  eprintf (", because type: \n");
-		  termlistPrint (tvar->stype);
-		  eprintf (" does not contain ");
-		  termlistPrint (tsubst->stype);
-		  eprintf ("\n");
-		}
-#endif
-	      return 0;
-	    }
-	}
-    }
+  res = checkTypeTerm (mgu_match, tvar);
+
+  tvar->subst = tbuf;
+  return res;
 }
 
 //! Undo all substitutions in a list of variables.

src/mgu.h

@@ -14,6 +14,7 @@
  */
 #define MGUFAIL (Termlist) -1
 
+void setMguMode (const int mgu);
 Termlist termMguTerm (Term t1, Term t2);
 int termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist));
 int termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),

src/switches.c

@@ -12,7 +12,6 @@
 #include "timer.h"
 
 extern System sys;
-extern int mgu_match;
 
 extern struct tacnode *spdltac;
 extern Term TERM_Claim;
@@ -232,7 +231,6 @@ switcher (const int process, const System sys, int index)
       else
 	{
 	  sys->match = integer_argument ();
-	  mgu_match = sys->match;
 	  return index;
 	}
     }

src/system.c

@@ -15,6 +15,7 @@
 #include "output.h"
 #include "tracebuf.h"
 #include "role.h"
+#include "mgu.h"
 
 /* from compiler.o */
 extern Term TERM_Type;
@@ -160,6 +161,9 @@ systemReset (const System sys)
 
   globalLatex = sys->latex;
 
+  /* propagate mgu_mode */
+
+  setMguMode (sys->match);
 }
 
 //! Initialize runtime system (according to cut traces, limited runs)

src/type.c

@@ -0,0 +1,151 @@
+/*
+ * type.c
+ *
+ * Code to check the consistency of types, in the presence of type flaw stuff etc.
+ */
+
+#include <stdlib.h>
+#include <stdio.h>
+#include "term.h"
+#include "termlist.h"
+#include "system.h"
+#include "debug.h"
+
+/*
+ * Special term definitions from compiler.c
+ */
+extern Term TERM_Agent;
+extern Term TERM_Function;
+extern Term TERM_Hidden;
+extern Term TERM_Type;
+extern Term TERM_Nonce;
+extern Term TERM_Ticket;
+
+extern Protocol INTRUDER;
+
+//! Report a bad substitution, if needed
+void
+reportBadSubst (const Term tvar, const Term tsubst)
+{
+#ifdef DEBUG
+  if (DEBUGL (5))
+    {
+      Term tbuf;
+
+      tbuf = tvar->subst;
+      tvar->subst = NULL;
+
+      eprintf ("Substitution fails on ");
+      termPrint (tvar);
+      eprintf (" -/-> ");
+      termPrint (tsubst);
+      eprintf (", maybe because type: \n");
+      termlistPrint (tvar->stype);
+      eprintf (" does not contain ");
+      termlistPrint (tsubst->stype);
+      eprintf ("\n");
+
+      tvar->subst = tbuf;
+    }
+#endif
+}
+
+//! Check whether a single variable term is instantiated correctly.
+/**
+ * Check whether a single variable term is instantiated correctly in this
+ * system. This takes the matching parameter into account, and is aware of the
+ * 'ticket' type.
+ *
+ * Non-variables etc. imply true.
+ */
+int
+checkTypeTerm (const int mgumode, const Term tvar)
+{
+  // Checks are only needed for mgumode < 2 etc.
+  if (mgumode < 2 && tvar != NULL && realTermVariable (tvar))
+    {
+      // Non-instantiated terms are fine.
+      if (tvar->subst != NULL)
+	{
+	  // NULL type is always fine
+	  if (tvar->stype != NULL)
+	    {
+	      // Tickets are always fine too
+	      if (!inTermlist (tvar->stype, TERM_Ticket))
+		{
+		  // So there is a specific (non-ticket) type, and the var is instantiated, match mode 0 or 1
+		  // Is it really a leaf?
+		  Term tsubst;
+
+		  tsubst = deVar (tvar);
+		  if (!realTermLeaf (tsubst))
+		    {
+		      // Then it's definitively false
+		      reportBadSubst (tvar, tsubst);
+		      return false;
+		    }
+		  else
+		    {
+		      // It is a leaf
+		      if (mgumode == 0)
+			{
+			  /* Types must match exactly. Thus, one of the variable type should match a type of the constant.
+			   */
+			  Termlist tl;
+
+			  tl = tvar->stype;
+			  while (tl != NULL)
+			    {
+			      if (inTermlist (tsubst->stype, tl->term))
+				{
+				  // One type matches
+				  return true;
+				}
+			      tl = tl->next;
+			    }
+			  // No type matches.
+			  reportBadSubst (tvar, tsubst);
+			  return false;
+			}
+		    }
+		}
+	    }
+	}
+    }
+  return true;
+}
+
+//! Check types of a list
+/**
+ * Empty list implies true.
+ */
+int
+checkTypeTermlist (const int mgumode, Termlist tl)
+{
+  while (tl != NULL)
+    {
+      if (!checkTypeTerm (mgumode, tl->term))
+	return false;
+      tl = tl->next;
+    }
+  return true;
+}
+
+//! Check whether all local variables are instantiated correctly.
+int
+checkTypeLocals (const System sys)
+{
+  int run;
+
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      if (sys->runs[run].protocol != INTRUDER)
+	{
+	  if (!checkTypeTermlist (sys->match, sys->runs[run].locals))
+	    return false;
+	}
+      run++;
+    }
+  return true;
+}

src/type.h

@@ -0,0 +1,11 @@
+#ifndef TYPE
+#define TYPE
+
+#include "term.h"
+#include "system.h"
+
+int checkTypeTerm (const int mgumode, const Term t);
+int checkTypeTermlist (const int mgumode, Termlist tl);
+int checkTypeLocals (const System sys);
+
+#endif