From 6afcfe1d1079ee0f17f0e3d69474b26cc7944973 Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Tue, 4 Jan 2011 15:17:52 +0100
Subject: [PATCH] NEW: Added SID & SKR dummy claims.

This allows for input file reuse among branches (i.e. compromise).
---
 src/arachne.c     | 17 ++++++++----
 src/claim.c       | 68 ++++++++++++++++++++++++++++++++++++++++++++++-
 src/claim.h       |  2 ++
 src/compiler.h    |  2 ++
 src/specialterm.c |  5 ++++
 src/specialterm.h |  2 ++
 6 files changed, 90 insertions(+), 6 deletions(-)

diff --git a/src/arachne.c b/src/arachne.c
index c8179d0..67cb737 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -2368,10 +2368,13 @@ arachneClaimTest (Claimlist cl)
 
 //! Arachne single claim inspection
 int
-arachneClaim (Claimlist cl)
+arachneClaim ()
 {
-  // Skip the dummy claims
-  if (!isTermEqual (cl->type, CLAIM_Empty))
+  Claimlist cl;
+
+  // Skip the dummy claims or SID markers
+  cl = sys->current_claim;
+  if (!isClaimSignal (cl))
     {
       // Some claims are always true!
       if (!cl->alwaystrue)
@@ -2472,9 +2475,13 @@ arachne ()
       /**
        * Check each claim
        */
-      if (arachneClaim (cl))
+      sys->current_claim = cl;
+      if (isClaimRelevant (cl))	// check for any filtered claims (switch)
 	{
-	  count++;
+	  if (arachneClaim ())
+	    {
+	      count++;
+	    }
 	}
 
       // next
diff --git a/src/claim.c b/src/claim.c
index be155b6..186ce97 100644
--- a/src/claim.c
+++ b/src/claim.c
@@ -39,6 +39,7 @@
 #include "color.h"
 #include "cost.h"
 #include "timer.h"
+#include "compiler.h"
 
 //! When none of the runs match
 #define MATCH_NONE 0
@@ -816,7 +817,7 @@ add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd,
   // per default, all agents are trusted
   sys->trustedRoles = NULL;
 
-  if (cl->type == CLAIM_Secret)
+  if (cl->type == CLAIM_Secret || cl->type == CLAIM_SKR)
     {
       int newgoals;
       int flag;
@@ -1153,3 +1154,68 @@ claimStatusReport (const System sys, Claimlist cl)
       return true;
     }
 }
+
+//! Check whether this claim needs to be verified according to filter settings
+int
+isClaimRelevant (const Claimlist cl)
+{
+  // Is there something to filter?
+  if (switches.filterProtocol == NULL)
+    {
+      // No: consider all claims
+      return true;
+    }
+  else
+    {
+      // only this protocol
+      if (!isStringEqual
+	  (switches.filterProtocol,
+	   TermSymb (((Protocol) cl->protocol)->nameterm)->text))
+	{
+	  // not this protocol; return
+	  return false;
+	}
+      // and maybe also a specific cl->label?
+      if (switches.filterLabel != NULL)
+	{
+	  if (cl->label == NULL)
+	    {
+	      return false;
+	    }
+	  else
+	    {
+	      Term t;
+
+	      t = cl->label;
+	      while (isTermTuple (t))
+		{
+		  t = TermOp2 (t);
+		}
+	      if (!isStringEqual (switches.filterLabel, TermSymb (t)->text))
+		{
+		  // not this label; return
+		  return false;
+		}
+	    }
+	}
+    }
+  return true;
+}
+
+//! Check whether a claim is really just a signal, and not a claim
+/**
+ * This piece of code effectively decides what is a signal and what not
+ */
+int
+isClaimSignal (const Claimlist cl)
+{
+  if (isTermEqual (cl->type, CLAIM_Empty))
+    {
+      return true;
+    }
+  if (isTermEqual (cl->type, CLAIM_SID))
+    {
+      return true;
+    }
+  return false;
+}
diff --git a/src/claim.h b/src/claim.h
index c66f335..ee22d9b 100644
--- a/src/claim.h
+++ b/src/claim.h
@@ -40,5 +40,7 @@ int add_claim_specifics (const System sys, const Claimlist cl, const
 void count_false_claim (const System sys);
 int property_check (const System sys);
 int claimStatusReport (const System sys, Claimlist cl);
+int isClaimRelevant (const Claimlist cl);
+int isClaimSignal (const Claimlist cl);
 
 #endif
diff --git a/src/compiler.h b/src/compiler.h
index a49ccdb..451c6bd 100644
--- a/src/compiler.h
+++ b/src/compiler.h
@@ -42,4 +42,6 @@ void levelTacDeclaration (Tac tc, int isVar);
 #define	levelVar(s)	symbolDeclare(s,1)
 #define	levelConst(s)	symbolDeclare(s,0)
 
+int isStringEqual (const char *s1, const char *s2);
+
 #endif
diff --git a/src/specialterm.c b/src/specialterm.c
index 54130f4..3d28fba 100644
--- a/src/specialterm.c
+++ b/src/specialterm.c
@@ -48,6 +48,8 @@ Term CLAIM_Nisynch;
 Term CLAIM_Niagree;
 Term CLAIM_Empty;
 Term CLAIM_Reachable;
+Term CLAIM_SID;
+Term CLAIM_SKR;
 
 Term AGENT_Alice;
 Term AGENT_Bob;
@@ -85,6 +87,9 @@ specialTermInit (const System sys)
   langcons (CLAIM_Empty, "Empty", TERM_Claim);
   langcons (CLAIM_Reachable, "Reachable", TERM_Claim);
 
+  langcons (CLAIM_SID, "SID", TERM_Claim);	// claim specifying session ID
+  langcons (CLAIM_SKR, "SKR", TERM_Claim);	// claim specifying session key : doubles as secrecy claim
+
   /* Define default PKI using PK/SK/K */
   langcons (TERM_PK, "pk", TERM_Function);
   langcons (TERM_SK, "sk", TERM_Function);
diff --git a/src/specialterm.h b/src/specialterm.h
index aa23f08..619c442 100644
--- a/src/specialterm.h
+++ b/src/specialterm.h
@@ -42,6 +42,8 @@ extern Term CLAIM_Nisynch;
 extern Term CLAIM_Niagree;
 extern Term CLAIM_Empty;
 extern Term CLAIM_Reachable;
+extern Term CLAIM_SID;
+extern Term CLAIM_SKR;
 
 extern Term AGENT_Alice;
 extern Term AGENT_Bob;