- Added well-formedness checks. This will only be enabled if a role uses

the 'knows' keyword.

src/compiler.c

@@ -876,6 +876,7 @@ roleCompile (Term nameterm, Tac tc)
 void
 roleKnows (Tac tc)
 {
+  sys->knowledgedefined = true;	// apparently someone uses this, so we enable the check
   thisRole->knows =
     termlistConcat (thisRole->knows, tacTermlist (tc->t1.tac));
 }
@@ -1801,6 +1802,63 @@ checkUnusedVariables (const System sys)
     }
 }
 
+//! Is a complete role well-formed
+int
+WellFormedRole (const System sys, Protocol p, Role r)
+{
+  Knowledge know;
+  int okay;
+  Roledef rd;
+
+  okay = true;
+  know = emptyKnowledge ();
+  // Transfer inverses
+  know->inverses = sys->know->inverses;
+  // Add role knowledge
+  knowledgeAddTermlist (know, r->knows);
+  // Add role names
+  //@TODO this is not in the semantics as such, often implicit
+  knowledgeAddTermlist (know, p->rolenames);
+  // Add local constants
+  //@TODO this is not in the semantics as such, often implicit
+  knowledgeAddTermlist (know, r->declaredconsts);
+
+  // Test
+  rd = r->roledef;
+  while (rd != NULL)
+    {
+      Knowledge knowres;
+
+      knowres = WellFormedEvent (r->nameterm, know, rd);
+      if (knowres == NULL)
+	{
+	  okay = false;
+	  break;
+	}
+      else
+	{
+	  know = knowres;
+	  rd = rd->next;
+	}
+    }
+
+  // clean up
+  knowledgeDelete (know);
+  return okay;
+}
+
+//! Well-formedness check
+void
+checkWellFormed (const System sys)
+{
+  int thisRole (Protocol p, Role r)
+  {
+    return WellFormedRole (sys, p, r);
+  }
+
+  iterateRoles (sys, thisRole);
+}
+
 //! Preprocess after system compilation
 void
 preprocess (const System sys)
@@ -1817,7 +1875,10 @@ preprocess (const System sys)
   /*
    * check for ununsed variables
    */
+  if (switches.check)
+    {
       checkUnusedVariables (sys);
+    }
   /*
    * compute hidelevels
    */
@@ -1825,5 +1886,15 @@ preprocess (const System sys)
   /*
    * Initial knowledge
    */
+  if (sys->knowledgedefined)
+    {
       initialIntruderKnowledge (sys);
+    }
+  /*
+   * Check well-formedness
+   */
+  if (sys->knowledgedefined)
+    {
+      checkWellFormed (sys);
+    }
 }

src/hidelevel.c

@@ -20,7 +20,7 @@ protocolHidelevel (const System sys, const Term t)
 
   minlevel = INT_MAX;
 
-  int itsends (const System sys, const Protocol p, const Role r)
+  int itsends (const Protocol p, const Role r)
   {
     int sends (Roledef rd)
     {
@@ -45,7 +45,7 @@ protocolHidelevel (const System sys, const Term t)
     return true;
   }
 
-  system_iterate_roles (sys, itsends);
+  iterateRoles (sys, itsends);
 
   return minlevel;
 }

src/intruderknowledge.c

@@ -11,9 +11,12 @@ addSTerm (const System sys, Term t, Termlist fromlist, Termlist tolist)
   Term t2;
 
   t2 = termLocal (t, fromlist, tolist);
+
+  /*
      eprintf ("[ Adding ");
      termPrint (t2);
      eprintf (" to the initial intruder knowledge]\n");
+   */
 }
 
 //! Unfold the term for all possible options
@@ -89,6 +92,8 @@ anySubTerm (Term t, Termlist sublist)
 void
 initialIntruderKnowledge (const System sys)
 {
+  if (switches.check)
+    {
       eprintf ("Computing initial intruder knowledge.\n\n");
       eprintf ("Agent names      : ");
       termlistPrint (sys->agentnames);
@@ -96,6 +101,7 @@ initialIntruderKnowledge (const System sys)
       eprintf ("Untrusted agents : ");
       termlistPrint (sys->untrusted);
       eprintf ("\n");
+    }
 
   /*
    * display initial role knowledge
@@ -169,11 +175,14 @@ initialIntruderKnowledge (const System sys)
 	}
     }
 
+    if (switches.check)
+      {
 	eprintf ("Role ");
 	termPrint (r->nameterm);
 	eprintf (" knows ");
 	termlistPrint (r->knows);
 	eprintf ("\n");
+      }
 
     addListKnowledge (r->knows, r->nameterm);
     return true;

src/intruderknowledge.h

@@ -2,6 +2,7 @@
 #define INTRUDERKNOWLEDGE
 
 #include "system.h"
+#include "switches.h"
 
 void initialIntruderKnowledge (const System sys);
 

src/role.c

@@ -321,7 +321,7 @@ roledef_shift (Roledef rd, int i)
   return rd;
 }
 
-// Check whether a term is a subterm of a roledef
+//! Check whether a term is a subterm of a roledef
 int
 roledefSubTerm (Roledef rd, Term tsub)
 {
@@ -335,3 +335,172 @@ roledefSubTerm (Roledef rd, Term tsub)
 	      termSubTerm (rd->to, tsub) || termSubTerm (rd->message, tsub));
     }
 }
+
+/*
+ * Some stuff directly from the semantics
+ */
+
+//! Is a term readable (from some knowledge set)
+/**
+ * Returns value of predicate
+ */
+int
+Readable (Knowledge know, Term t)
+{
+  if (isTermVariable (t))
+    {
+      // Variable pattern
+      return true;
+    }
+  if (!isTermLeaf (t))
+    {
+      if (isTermTuple (t))
+	{
+	  // Tuple pattern
+	  Knowledge knowalt;
+	  int both;
+
+	  both = false;
+	  knowalt = knowledgeDuplicate (know);
+	  knowledgeAddTerm (knowalt, TermOp2 (t));
+	  if (Readable (knowalt, TermOp1 (t)))
+	    {
+	      // Yes, left half works
+	      knowledgeDelete (knowalt);
+	      knowalt = knowledgeDuplicate (know);
+	      knowledgeAddTerm (knowalt, TermOp1 (t));
+	      if (Readable (knowalt, TermOp2 (t)))
+		{
+		  both = true;
+		}
+	    }
+	  knowledgeDelete (knowalt);
+	  return both;
+	}
+      else
+	{
+	  // Encryption pattern
+	  // But we exclude functions
+	  if (getTermFunction (t) == NULL)
+	    {
+	      // Real encryption pattern
+	      Term inv;
+	      int either;
+
+	      // Left disjunct
+	      if (inKnowledge (know, t))
+		{
+		  return true;
+		}
+	      // Right disjunct
+	      inv = inverseKey (know->inverses, TermKey (t));
+	      either = false;
+	      if (inKnowledge (know, inv))
+		{
+		  if (Readable (know, TermOp (t)))
+		    {
+		      either = true;
+		    }
+		}
+	      termDelete (inv);
+	      return either;
+	    }
+	}
+    }
+  return inKnowledge (know, t);
+}
+
+//! Well-formed error reporting.
+void
+wfeError (Knowledge know, Roledef rd, char *errorstring, Term was,
+	  Term shouldbe)
+{
+  globalError++;
+  eprintf ("Well-formedness error.\n");
+  roledefPrint (rd);
+  eprintf ("\nKnowing ");
+  knowledgePrintShort (know);
+  eprintf ("\n");
+  if (was != NULL || shouldbe != NULL)
+    {
+      eprintf ("while parsing ");
+      termPrint (was);
+      if (shouldbe != NULL)
+	{
+	  eprintf (" which should have been ");
+	  termPrint (shouldbe);
+	}
+      eprintf ("\n");
+    }
+  globalError--;
+  error (errorstring);
+}
+
+
+//! Is an event well-formed
+/**
+ * Returns the new knowledge or NULL if it was not well-formed.
+ */
+Knowledge
+WellFormedEvent (Term role, Knowledge know, Roledef rd)
+{
+  if (rd == NULL)
+    {
+      return know;
+    }
+  if (rd->type == READ)
+    {
+      // Read
+      if (!isTermEqual (role, rd->to))
+	{
+	  wfeError (know, rd, "Reading role incorrect.", rd->to, role);
+	  return NULL;
+	}
+      if (!inKnowledge (know, rd->from))
+	{
+	  wfeError (know, rd, "Unknown sender role.", rd->from, NULL);
+	  return NULL;
+
+	}
+      if (!Readable (know, rd->message))
+	{
+	  wfeError (know, rd, "Cannot read message pattern.", rd->message,
+		    NULL);
+	  return NULL;
+	}
+      knowledgeAddTerm (know, rd->message);
+      return know;
+    }
+  if (rd->type == SEND)
+    {
+      // Send
+      if (!isTermEqual (role, rd->from))
+	{
+	  wfeError (know, rd, "Sending role incorrect.", rd->from, role);
+	  return NULL;
+	}
+      if (!inKnowledge (know, rd->to))
+	{
+	  wfeError (know, rd, "Unknown reading role.", rd->to, NULL);
+	  return NULL;
+
+	}
+      if (!inKnowledge (know, rd->message))
+	{
+	  wfeError (know, rd, "Unable to construct message.", rd->message,
+		    NULL);
+	  return NULL;
+	}
+    }
+  if (rd->type == CLAIM)
+    {
+      // Claim
+      if (!isTermEqual (role, rd->from))
+	{
+	  wfeError (know, rd, "Claiming role incorrect.", rd->from, role);
+	  return NULL;
+	}
+    }
+  // Unknown, false
+  return NULL;
+}

src/role.h

@@ -164,5 +164,6 @@ int roledef_iterate_events (Roledef rd, int (*func) ());
 int roledef_length (const Roledef rd);
 Roledef roledef_shift (Roledef rd, int i);
 int roledefSubTerm (Roledef rd, Term tsub);
+Knowledge WellFormedEvent (Term role, Knowledge know, Roledef rd);
 
 #endif

src/system.c

@@ -70,6 +70,7 @@ systemInit ()
   sys->roleeventmax = 0;
   sys->claimlist = NULL;
   sys->labellist = NULL;
+  sys->knowledgedefined = false;	// currently, we have backwards compatibility for empty role knowledge defs (disabling well-formedness rules)
   sys->attackid = 0;		// First attack will have id 1, because the counter is increased before any attacks are displayed.
 
   bindingInit (sys);
@@ -1194,33 +1195,6 @@ scenarioPrint (const System sys)
     }
 }
 
-//! Iterate over all roles (AND)
-/**
- * Function called gets (sys,protocol,role)
- * If it returns 0, iteration aborts.
- */
-int
-system_iterate_roles (const System sys, int (*func) ())
-{
-  Protocol p;
-
-  p = sys->protocols;
-  while (p != NULL)
-    {
-      Role r;
-
-      r = p->roles;
-      while (r != NULL)
-	{
-	  if (!func (sys, p, r))
-	    return 0;
-	  r = r->next;
-	}
-      p = p->next;
-    }
-  return 1;
-}
-
 //! Determine whether we don't need any more attacks
 /**
  * Returns 1 (true) iff no more attacks are needed.

src/system.h

@@ -139,6 +139,7 @@ struct system
   int lastChooseRun;		//!< Last run with a choose event
   Claimlist claimlist;		//!< List of claims in the system, with occurrence counts
   List labellist;		//!< List of labelinfo stuff
+  int knowledgedefined;		//!< True if knowledge is defined for some role (which triggers well-formedness check etc.)
 
   /* constructed trace pointers, static */
   Roledef *traceEvent;		//!< Trace roledefs: MaxRuns * maxRoledef
@@ -189,7 +190,6 @@ int compute_rolecount (const System sys);
 int compute_roleeventmax (const System sys);
 
 void scenarioPrint (const System sys);
-int system_iterate_roles (const System sys, int (*func) ());
 int isAgentTrusted (const System sys, Term agent);
 int isAgentlistTrusted (const System sys, Termlist agents);
 int isRunTrusted (const System sys, const int run);