From 5f7138c300805592198359a34139fdc396dbc84c Mon Sep 17 00:00:00 2001
From: Cas Cremers <cremersc@brutus3.ethz.ch>
Date: Tue, 18 Jan 2011 17:03:20 +0100
Subject: [PATCH] BUGFIX: Partial implementation of chosen name attacks could
 yield false type flaw attacks.

For the typed model, this was not an issue.
---
 src/prune_theorems.c | 113 +++++++++++++++++++++++++++++++------------
 src/switches.c       |  17 +++++++
 src/switches.h       |   1 +
 3 files changed, 100 insertions(+), 31 deletions(-)

diff --git a/src/prune_theorems.c b/src/prune_theorems.c
index 165ce15..9c41c89 100644
--- a/src/prune_theorems.c
+++ b/src/prune_theorems.c
@@ -113,6 +113,32 @@ correctLocalOrder (const System sys)
   return flag;
 }
 
+//! Check all runs
+/**
+ * Returns false iff an agent type is wrong
+ */
+int
+allAgentsType (const System sys)
+{
+  int run;
+
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      Termlist agents;
+
+      agents = sys->runs[run].rho;
+      while (agents != NULL)
+	{
+	  if (!goodAgentType (agents->term))
+	    {
+	      return false;
+	    }
+	  agents = agents->next;
+	}
+    }
+  return true;			// seems to be okay
+}
+
 //! Check initiator roles
 /**
  * Returns false iff an agent type is wrong
@@ -170,30 +196,6 @@ prune_theorems (const System sys)
       return true;
     }
 
-  // Check if all actors are agents for responders (initiators come next)
-  run = 0;
-  while (run < sys->maxruns)
-    {
-      if (!sys->runs[run].role->initiator)
-	{
-	  Term actor;
-
-	  actor = agentOfRun (sys, run);
-	  if (!goodAgentType (actor))
-	    {
-	      if (switches.output == PROOF)
-		{
-		  indentPrint ();
-		  eprintf ("Pruned because the actor ");
-		  termPrint (actor);
-		  eprintf (" of run %i is not of a compatible type.\n", run);
-		}
-	      return true;
-	    }
-	}
-      run++;
-    }
-
   // Prune if any initiator run talks to itself
   /**
    * This effectively disallows Alice from talking to Alice, for all
@@ -224,16 +226,65 @@ prune_theorems (const System sys)
 	}
     }
 
-  // Prune wrong agents type for initators
-  if (!initiatorAgentsType (sys))
+/*
+The semantics imply that create event chose agent names, i.e., the range of rho is a subset of Agent.
+
+For chosen name attacks we may want to loosen that. However, this requires inserting receive events for the non-actor role variables of responders, and we don't have that yet,
+so technically this is a bug. Don't use.
+*/
+  if (switches.chosenName)
     {
-      if (switches.output == PROOF)
+      // Check if all actors are agents for responders (initiators come next)
+      run = 0;
+      while (run < sys->maxruns)
 	{
-	  indentPrint ();
-	  eprintf
-	    ("Pruned: an initiator role does not have the correct type for one of its agents.\n");
+	  if (!sys->runs[run].role->initiator)
+	    {
+	      Term actor;
+
+	      actor = agentOfRun (sys, run);
+	      if (!goodAgentType (actor))
+		{
+		  if (switches.output == PROOF)
+		    {
+		      indentPrint ();
+		      eprintf ("Pruned because the actor ");
+		      termPrint (actor);
+		      eprintf (" of run %i is not of a compatible type.\n",
+			       run);
+		    }
+		  return true;
+		}
+	    }
+	  run++;
+	}
+
+      // Prune wrong agents type for initators
+      if (!initiatorAgentsType (sys))
+	{
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf
+		("Pruned: an initiator role does not have the correct type for one of its agents.\n");
+	    }
+	  return true;
+	}
+
+    }
+  else
+    {
+      // Prune wrong agents type for runs
+      if (!allAgentsType (sys))
+	{
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf
+		("Pruned: some run does not have the correct type for one of its agents.\n");
+	    }
+	  return true;
 	}
-      return true;
     }
 
   // Check if the actors of all other runs are not untrusted
diff --git a/src/switches.c b/src/switches.c
index ca9c82a..ad6aa13 100644
--- a/src/switches.c
+++ b/src/switches.c
@@ -79,6 +79,7 @@ switchesInit (int argc, char **argv)
   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
+  switches.chosenName = false;	// default no chosen name attacks
   switches.agentUnfold = 0;	// default not to unfold agents
   switches.abstractionMethod = 0;	// default no abstraction used
   switches.useAttackBuffer = false;	// don't use by default as it does not work properly under windows vista yet
@@ -1064,6 +1065,22 @@ switcher (const int process, int index, int commandline)
 	}
     }
 
+  if (detect (' ', "chosen-name", 0))
+    {
+      if (!process)
+	{
+	  /* discourage: hide
+	   *
+	   * Check for chosen-name attacks. Currently buggy: see prune_theorems.c for more details.
+	   */
+	}
+      else
+	{
+	  switches.chosenName = true;
+	  return index;
+	}
+    }
+
   if (detect (' ', "extend-trivial", 0))
     {
       if (!process)
diff --git a/src/switches.h b/src/switches.h
index c2d8a65..20a866f 100644
--- a/src/switches.h
+++ b/src/switches.h
@@ -55,6 +55,7 @@ struct switchdata
   int initUnique;		//!< Default allows duplicate terms in rho (init) 
   int respUnique;		//!< Default allows duplicate terms in rho (resp)
   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
   int abstractionMethod;	//!< 0 means none, others are specific modes
   int useAttackBuffer;		//!< Use temporary file for attack storage