- Added feature for multi-party protocols (weaker precondition on Reachable)

gui/Changelog.txt

@@ -6,6 +6,11 @@ Scyther 1.0-beta6
 	
 	* Added Mac support (added universal binary)
 	* Fixed bug in scripting backend (e.g. with mpa.py)
+	* Added claim parameter for Reachable claim; Reachable,R means
+	  that role R should be trusted (as well as the actor), but not
+	  any other claim. This can be useful for showing stronger
+	  authentication properties of protocols with more than two
+	  parties.
 
 Scyther 1.0-beta5 
 

src/claim.c

@@ -707,6 +707,29 @@ arachne_claim_nisynch (const System sys, const int claim_run,
   return arachne_claim_authentications (sys, claim_run, claim_index, 1);
 }
 
+//! Are all agents trusted of the claim run (as required by the property?)
+int
+pruneClaimRunTrusted (const System sys)
+{
+  if (sys->trustedRoles == NULL)
+    {
+      // all agents need to be trusted
+      if (!isRunTrusted (sys, 0))
+	{
+	  return true;
+	}
+    }
+  else
+    {
+      // a subset is trusted
+      if (!isAgentlistTrusted (sys, sys->trustedRoles))
+	{
+	  return true;
+	}
+    }
+  return false;
+}
+
 //! Prune determination for specific properties
 /**
  * Sometimes, a property holds in part of the tree. Thus, we don't need to explore that part further if we want to find an attack.
@@ -716,6 +739,19 @@ arachne_claim_nisynch (const System sys, const int claim_run,
 int
 prune_claim_specifics (const System sys)
 {
+  // generic status of (all) roles trusted or not
+  if (pruneClaimRunTrusted (sys))
+    {
+      if (switches.output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf
+	    ("Pruned because all agents of the claim run must be trusted.\n");
+	}
+      return true;
+    }
+
+  // specific claims
   if (sys->current_claim->type == CLAIM_Niagree)
     {
       if (arachne_claim_niagree (sys, 0, sys->current_claim->ev))
@@ -757,6 +793,10 @@ add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd,
   /*
    * different cases
    */
+
+  // per default, all agents are trusted
+  sys->trustedRoles = NULL;
+
   if (cl->type == CLAIM_Secret)
     {
       int newgoals;
@@ -791,6 +831,8 @@ add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd,
 
   if (cl->type == CLAIM_Reachable)
     {
+      int flag;
+
       if (switches.check)
 	{
 	  // For reachability claims in check mode, we restrict the number of runs to the number of roles of this protocol
@@ -801,7 +843,28 @@ add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd,
 	  rolecount = termlistLength (protocol->rolenames);
 	  switches.runs = rolecount;
 	}
-      return callback ();
+      if (rd->message != NULL)
+	{
+	  sys->trustedRoles = tuple_to_termlist (rd->message);
+
+#ifdef DEBUG
+	  if (DEBUGL (2))
+	    {
+	      eprintf ("Trusted roles : ");
+	      termlistPrint (sys->trustedRoles);
+	      eprintf ("\n");
+	    }
+#endif
+	}
+
+      flag = callback ();
+
+      if (rd->message != NULL)
+	{
+	  termlistDelete (sys->trustedRoles);
+	  sys->trustedRoles = NULL;
+	}
+      return flag;
     }
 
   return callback ();

src/compiler.c

@@ -998,22 +998,7 @@ runInstanceCreate (Tac tc)
   roleInstance (sys, p, r, instParams, NULL);	// technically, we don't need to do this for Arachne [fix later]
 
   /* after creation analysis */
-  /* AC1: untrusted agents */
+  /* originator assumption for CLP ? */
-  /*      first: determine whether the run is untrusted,
-   *      by checking whether one of the untrusted agents occurs
-   *      in the run instance  */
-  if (!isAgentlistTrusted (sys, instParams))
-    {
-      /* nothing yet */
-      /* claims handle this themselves */
-
-      /* some reduction might be possible, by cutting of the last few actions
-       * of such an untrusted run */
-
-      /* but most of it might be handled dynamically */
-    }
-
-  /* AC2: originator assumption for CLP ? */
   /* TODO */
 }
 

src/dotout.c

@@ -1673,61 +1673,61 @@ dotSemiState (const System mysys)
   maxrank = graph_ranks (ranks, nodes);	// determine ranks
 
 #ifdef DEBUG
-  if (DEBUGL(1))
+  if (DEBUGL (1))
-  {
+    {
-    // For debugging purposes, we also display an ASCII version of some stuff in the comments
+      // For debugging purposes, we also display an ASCII version of some stuff in the comments
-    printSemiState ();
+      printSemiState ();
-    // Even draw all dependencies for non-intruder runs
+      // Even draw all dependencies for non-intruder runs
-    // Real nice debugging :(
+      // Real nice debugging :(
-    int run;
+      int run;
 
-    run = 0;
+      run = 0;
-    while (run < sys->maxruns)
+      while (run < sys->maxruns)
-      {
+	{
-	int ev;
+	  int ev;
 
-	ev = 0;
+	  ev = 0;
-	while (ev < sys->runs[run].length)
+	  while (ev < sys->runs[run].length)
-	  {
+	    {
-	    int run2;
+	      int run2;
-	    int notfirstrun;
+	      int notfirstrun;
 
-	    eprintf ("// precedence: r%ii%i <- ", run, ev);
+	      eprintf ("// precedence: r%ii%i <- ", run, ev);
-	    run2 = 0;
+	      run2 = 0;
-	    notfirstrun = 0;
+	      notfirstrun = 0;
-	    while (run2 < sys->maxruns)
+	      while (run2 < sys->maxruns)
-	      {
+		{
-		int notfirstev;
+		  int notfirstev;
-		int ev2;
+		  int ev2;
 
-		notfirstev = 0;
+		  notfirstev = 0;
-		ev2 = 0;
+		  ev2 = 0;
-		while (ev2 < sys->runs[run2].length)
+		  while (ev2 < sys->runs[run2].length)
-		  {
+		    {
-		    if (isDependEvent (run2, ev2, run, ev))
+		      if (isDependEvent (run2, ev2, run, ev))
-		      {
+			{
-			if (notfirstev)
+			  if (notfirstev)
-			  eprintf (",");
+			    eprintf (",");
-			else
+			  else
-			  {
+			    {
-			    if (notfirstrun)
+			      if (notfirstrun)
-			      eprintf (" ");
+				eprintf (" ");
-			    eprintf ("r%i:", run2);
+			      eprintf ("r%i:", run2);
-			  }
+			    }
-			eprintf ("%i", ev2);
+			  eprintf ("%i", ev2);
-			notfirstrun = 1;
+			  notfirstrun = 1;
-			notfirstev = 1;
+			  notfirstev = 1;
-		      }
+			}
-		    ev2++;
+		      ev2++;
-		  }
+		    }
-		run2++;
+		  run2++;
-	      }
+		}
-	    eprintf ("\n");
+	      eprintf ("\n");
-	    ev++;
+	      ev++;
-	  }
+	    }
-	run++;
+	  run++;
-      }
+	}
-  }
+    }
 #endif
 
   // First, runs

src/prune_theorems.c

@@ -246,18 +246,6 @@ prune_theorems (const System sys)
       return true;
     }
 
-  // Check if all agents of the main run are valid
-  if (!isRunTrusted (sys, 0))
-    {
-      if (switches.output == PROOF)
-	{
-	  indentPrint ();
-	  eprintf
-	    ("Pruned because all agents of the claim run must be trusted.\n");
-	}
-      return true;
-    }
-
   // Check if the actors of all other runs are not untrusted
   if (sys->untrusted != NULL)
     {

src/system.c

@@ -74,9 +74,11 @@ systemInit ()
   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.
 
+  /* arachne assist */
   bindingInit (sys);
   sys->bindings = NULL;
   sys->current_claim = NULL;
+  sys->trustedRoles = NULL;
 
   /* reset global counters */
   systemReset (sys);

src/system.h

@@ -150,6 +150,7 @@ struct system
   /* Arachne assistance */
   List bindings;		//!< List of bindings
   Claimlist current_claim;	//!< The claim under current investigation
+  Termlist trustedRoles;	//!< Roles that should be trusted for this claim (the default, NULL, means all)
 };
 
 typedef struct system *System;