NEW: Added --role-unique switch to enforce that an agent can perform only one role.

src/prune_theorems.c

@@ -226,6 +226,20 @@ prune_theorems (const System sys)
 	}
     }
 
+  if (switches.roleUnique)
+    {
+      if (!agentsUniqueRoles (sys))
+	{
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf
+		("Pruned because agents are not performing unique roles.\n");
+	    }
+	  return true;
+	}
+    }
+
 /*
 The semantics imply that create event chose agent names, i.e., the range of rho is a subset of Agent.
 

src/switches.c

@@ -78,6 +78,7 @@ switchesInit (int argc, char **argv)
   switches.concrete = true;	// default removes symbols, and makes traces concrete
   switches.initUnique = false;	// default allows initiator rho to contain duplicate terms
   switches.respUnique = false;	// default allows responder rho to contain duplicate terms
+  switches.roleUnique = false;	// default allows agents to perform multiple roles
   switches.intruder = true;	// default allows an intruder
   switches.chosenName = false;	// default no chosen name attacks
   switches.agentUnfold = 0;	// default not to unfold agents
@@ -1065,6 +1066,22 @@ switcher (const int process, int index, int commandline)
 	}
     }
 
+  if (detect (' ', "role-unique", 0))
+    {
+      if (!process)
+	{
+	  /* discourage: hide
+	   *
+	   * Finds only attacks in which agents perform at most one role
+	   */
+	}
+      else
+	{
+	  switches.roleUnique = true;
+	  return index;
+	}
+    }
+
   if (detect (' ', "chosen-name", 0))
     {
       if (!process)

src/switches.h

@@ -54,6 +54,7 @@ struct switchdata
   int concrete;			//!< Swap out variables at the end.
   int initUnique;		//!< Default allows duplicate terms in rho (init) 
   int respUnique;		//!< Default allows duplicate terms in rho (resp)
+  int roleUnique;		//!< Default allows agents to perform multiple roles
   int intruder;			//!< Enable intruder actions (default)
   int chosenName;		//!< Check for chosen name attacks
   int agentUnfold;		//!< Explicitly unfold for N honest agents and 1 compromised iff > 0

src/system.c

@@ -1384,3 +1384,57 @@ isHelperProtocol (Protocol p)
     }
   return false;
 }
+
+//! Check whether agents are performing unique roles
+int
+agentsUniqueRoles (const System sys)
+{
+  Termlist roles;
+  Termlist agents;
+  int run;
+  int res;
+
+  roles = NULL;
+  agents = NULL;
+  res = true;
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      if (!isHelperProtocol (sys->runs[run].protocol))
+	{
+	  Term agentname;
+	  Term rolename;
+	  Termlist tla, tlr;
+
+	  rolename = sys->runs[run].role->nameterm;
+	  agentname = agentOfRunRole (sys, run, rolename);
+
+	  // Find out whether agent name was already mapped to a role
+	  tlr = roles;
+	  tla = agents;
+	  while ((tlr != NULL) && (tla != NULL))
+	    {
+	      if (isTermEqual (tla->term, agentname))
+		{
+		  // okay so this matches. Then so should the second.
+		  if (!isTermEqual (tlr->term, rolename))
+		    {
+		      res = false;
+		      // full abort
+		      tlr = NULL;
+		      run = sys->maxruns;
+		    }
+		  // stop anyway, because the agent is fine, should not occur twice
+		  break;
+		}
+	      tlr = tlr->next;
+	      tla = tla->next;
+	    }
+	  // Not in there yet, add. 
+	  agents = termlistAdd (agents, agentname);
+	  roles = termlistAdd (roles, rolename);
+	}
+    }
+  termlistDelete (agents);
+  termlistDelete (roles);
+  return res;
+}

src/system.h

@@ -209,6 +209,7 @@ int selfInitiator (const System sys, const int run);
 int selfInitiators (const System sys);
 int enoughAttacks (const System sys);
 int isHelperProtocol (Protocol p);
+int agentsUniqueRoles (const System sys);
 
 
 //! Equality for run structure naming