From 6543a8f6593288e81fae47e1cd3194fc6b3446cc Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Tue, 29 Nov 2005 09:15:16 +0000
Subject: [PATCH] - Added '--extravert' switch, which avoids initiator Alice to
 talk to   Alice.

---
 src/arachne.c  | 44 ++++++++++++++++++++++++++++++++++++++++++++
 src/switches.c | 17 +++++++++++++++++
 src/switches.h |  1 +
 3 files changed, 62 insertions(+)

diff --git a/src/arachne.c b/src/arachne.c
index f571062..bd6f713 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -2888,6 +2888,50 @@ prune_theorems ()
       run++;
     }
 
+  // Prune if any initiator run talks to itself
+  /**
+   * This effectively disallows Alice from talking to Alice, for all
+   * initiators. We still allow it for responder runs, because we assume the
+   * responder is not checking this.
+   */
+  if (switches.extravert)
+    {
+      int run;
+
+      run = 0;
+      while (run < sys->maxruns)
+	{
+	  // Check this run only if it is an initiator role
+	  if (sys->runs[run].role->initiator)
+	    {
+	      // Check this initiator run
+	      Termlist tl;
+
+	      tl = sys->runs[run].agents;
+	      while (tl != NULL)
+		{
+		  Termlist tlscan;
+
+		  tlscan = tl->next;
+		  while (tlscan != NULL)
+		    {
+		      if (isTermEqual (tl->term, tlscan->term))
+			{
+			  // XXX TODO
+			  // Still need to fix proof output for this
+			  //
+			  // Pruning because some agents are equal for this role.
+			  return 1;
+			}
+		      tlscan = tlscan->next;
+		    }
+		  tl = tl->next;
+		}
+	      run++;
+	    }
+	}
+    }
+
   // Prune wrong agents type for initators
   if (!initiatorAgentsType ())
     {
diff --git a/src/switches.c b/src/switches.c
index 7e64a2b..770bfde 100644
--- a/src/switches.c
+++ b/src/switches.c
@@ -68,6 +68,7 @@ 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
 
   // Misc
   switches.switchP = 0;		// multi-purpose parameter
@@ -560,6 +561,22 @@ switcher (const int process, int index)
 	}
     }
 
+  if (detect (' ', "extravert", 0))
+    {
+      if (!process)
+	{
+	  /* discourage: hide
+	   *
+	   * Finds only attacks which exclude initiator Alice talking to Alice
+	   */
+	}
+      else
+	{
+	  switches.extravert = true;
+	  return index;
+	}
+    }
+
   if (detect (' ', "extend-trivial", 0))
     {
       if (!process)
diff --git a/src/switches.h b/src/switches.h
index b1bebb2..be39cc3 100644
--- a/src/switches.h
+++ b/src/switches.h
@@ -47,6 +47,7 @@ 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
 
   // Misc
   int switchP;			//!< A multi-purpose integer parameter, passed to the partial order reduction method selected.