- Added --unique responder/initiator switches, which are both implied by

--extravert.

src/cost.c

@@ -34,6 +34,7 @@ attackCost (const System sys)
 
   cost += get_semitrace_length ();
   cost += 8 * selfInitiators (sys);
+  cost += 4 * selfResponders (sys);
 
   return cost;
 }

src/prune_theorems.c

@@ -208,7 +208,7 @@ prune_theorems (const System sys)
    * initiators. We still allow it for responder runs, because we assume the
    * responder is not checking this.
    */
-  if (switches.extravert)
+  if (switches.initUnique)
     {
       if (selfInitiators (sys) > 0)
 	{
@@ -220,6 +220,18 @@ prune_theorems (const System sys)
 	}
     }
 
+  if (switches.respUnique)
+    {
+      if (selfResponders (sys) > 0)
+	{
+	  // XXX TODO
+	  // Still need to fix proof output for this
+	  //
+	  // Pruning because some agents are equal for this role.
+	  return true;
+	}
+    }
+
   // Prune wrong agents type for initators
   if (!initiatorAgentsType (sys))
     {

src/switches.c

@@ -51,7 +51,8 @@ switchesInit (int argc, char **argv)
   switches.maxIntruderActions = INT_MAX;	// max number of encrypt/decrypt events
   switches.agentTypecheck = 1;	// default do check agent types
   switches.concrete = true;	// default removes symbols, and makes traces concrete
-  switches.extravert = false;	// default allows also initiator Alice to talk to Alice
+  switches.initUnique = false;	// default allows initiator rho to contain duplicate terms
+  switches.respUnique = false;	// default allows responder rho to contain duplicate terms
   switches.intruder = true;	// default allows an intruder
 
   // Misc
@@ -812,7 +813,40 @@ switcher (const int process, int index, int commandline)
 	}
       else
 	{
-	  switches.extravert = true;
+	  switches.initUnique = true;
+	  switches.respUnique = true;
+	  return index;
+	}
+    }
+
+  if (detect (' ', "init-unique", 0))
+    {
+      if (!process)
+	{
+	  /* discourage: hide
+	   *
+	   * Finds only attacks which exclude initiator Alice talking to Alice
+	   */
+	}
+      else
+	{
+	  switches.initUnique = true;
+	  return index;
+	}
+    }
+
+  if (detect (' ', "resp-unique", 0))
+    {
+      if (!process)
+	{
+	  /* discourage: hide
+	   *
+	   * Finds only attacks which exclude initiator Alice talking to Alice
+	   */
+	}
+      else
+	{
+	  switches.respUnique = true;
 	  return index;
 	}
     }

src/switches.h

@@ -31,7 +31,8 @@ struct switchdata
   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.
-  int extravert;		//!< Disallow Alice talking to Alice
+  int initUnique;		//!< Default allows duplicate terms in rho (init) 
+  int respUnique;		//!< Default allows duplicate terms in rho (resp)
   int intruder;			//!< Enable intruder actions (default)
 
   // Misc

src/system.c

@@ -1399,6 +1399,82 @@ eventRoledef (const System sys, const int run, const int ev)
   return roledef_shift (sys->runs[run].start, ev);
 }
 
+//! determine whether a run talks to itself
+int
+selfSession (const System sys, const int run)
+{
+  int self_session;
+  Termlist agents;
+  Termlist seen;
+
+  if (sys->runs[run].protocol == INTRUDER)
+    {
+      // Intruder has no self sessions
+      return false;
+    }
+
+  self_session = false;
+
+  agents = sys->runs[run].rho;
+  seen = NULL;
+  while (agents != NULL)
+    {
+      Term agent;
+
+      agent = deVar (agents->term);
+      if (inTermlist (seen, agent))
+	{
+	  // This agent was already in the seen list
+	  self_session = true;
+	}
+      else
+	{
+	  seen = termlistAdd (seen, agent);
+	}
+      agents = agents->next;
+    }
+  termlistDelete (seen);
+
+  return self_session;
+}
+
+//! determine whether a run is a so-called self-responder
+/**
+ * Alice starting a run with Bob, Charlie, Bob is also counted as self-response.
+ */
+int
+selfResponder (const System sys, const int run)
+{
+  if (sys->runs[run].role->initiator)
+    {
+      return false;
+    }
+  else
+    {
+      return selfSession (sys, run);
+    }
+}
+
+//! Count the number of any self-responders
+int
+selfResponders (const System sys)
+{
+  int count;
+  int run;
+
+  count = 0;
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      if (selfInitiator (sys, run))
+	{
+	  count++;
+	}
+      run++;
+    }
+  return count;
+}
+
 //! determine whether a run is a so-called self-initiator
 /**
  * Alice starting a run with Bob, Charlie, Bob is also counted as self-initiation.
@@ -1406,36 +1482,14 @@ eventRoledef (const System sys, const int run, const int ev)
 int
 selfInitiator (const System sys, const int run)
 {
-  int self_initiator;
-
-  self_initiator = false;
   if (sys->runs[run].role->initiator)
     {
-      // An initiator
+      return selfSession (sys, run);
-      Termlist agents;
+    }
-      Termlist seen;
+  else
-
+    {
-      agents = sys->runs[run].rho;
+      return false;
-      seen = NULL;
-      while (agents != NULL)
-	{
-	  Term agent;
-
-	  agent = agents->term;
-	  if (inTermlist (seen, agent))
-	    {
-	      // This agent was already in the seen list
-	      self_initiator = true;
-	    }
-	  else
-	    {
-	      seen = termlistAdd (seen, agent);
-	    }
-	  agents = agents->next;
-	}
-      termlistDelete (seen);
     }
-  return self_initiator;
 }
 
 //! Count the number of any self-initiators

src/system.h

@@ -201,6 +201,8 @@ int iterateLocalToOther (const System sys, const int myrun,
 			 int (*callback) (Term t));
 int firstOccurrence (const System sys, const int r, Term t, int evtype);
 Roledef eventRoledef (const System sys, const int run, const int ev);
+int selfResponder (const System sys, const int run);
+int selfResponders (const System sys);
 int selfInitiator (const System sys, const int run);
 int selfInitiators (const System sys);