- Much work for the skeleton of the Hidelevel lemma.

src/compiler.c

@@ -1,5 +1,6 @@
 #include <stdlib.h>
 #include <stdio.h>
+#include <limits.h>
 #include "tac.h"
 #include "term.h"
 #include "termlist.h"
@@ -12,6 +13,7 @@
 #include "compiler.h"
 #include "switches.h"
 #include "specialterm.h"
+#include "hidelevel.h"
 
 /*
    Simple sys pointer as a global. Yields cleaner code although it's against programming standards.
@@ -372,6 +374,10 @@ levelTacDeclaration (Tac tc, int isVar)
 		termlistAdd (thisRole->declaredconsts, t);
 	    }
 	}
+      else if (level == 0)
+	{
+	  sys->globalconstants = termlistAdd (sys->globalconstants, t);
+	}
       tscan = tscan->next;
     }
 }
@@ -1790,4 +1796,8 @@ preprocess (const System sys)
    * check for ununsed variables
    */
   checkUnusedVariables (sys);
+  /*
+   * compute hidelevels
+   */
+  hidelevelCompute (sys);
 }

src/hidelevel.c

@@ -0,0 +1,180 @@
+/** @file hidelevel.c \brief Hidelevel lemma base functions.
+ *
+ * The Hidelevel lemma is fairly complex and so it requires some buffering,
+ * instead of fully recomputing the required data each time again.
+ */
+
+#include <limits.h>
+#include "hidelevel.h"
+#include "system.h"
+#include "memory.h"
+
+//! hide level within protocol
+unsigned int
+protocolHidelevel (const System sys, const Term t)
+{
+	unsigned int minlevel;
+
+	minlevel = INT_MAX;
+
+	int itsends (const System sys, const Protocol p, const Role r)
+	{
+		int sends(Roledef rd)
+		{
+			if (rd->type == SEND)
+			{
+				unsigned int l;
+
+				l = termHidelevel (t, rd->from);
+				if (l < minlevel) minlevel = l;
+				l = termHidelevel (t, rd->to);
+				if (l < minlevel) minlevel = l;
+				l = termHidelevel (t, rd->message);
+				if (l < minlevel) minlevel = l;
+			}
+			return true;
+		}
+
+		roledef_iterate_events (r->roledef, sends);
+		return true;
+	}
+
+	system_iterate_roles (sys, itsends);
+
+	return minlevel;
+}
+
+//! hide level within initial knowledge
+unsigned int
+knowledgeHidelevel (const System sys, const Term t)
+{
+	unsigned int minlevel;
+	Termlist tl;
+
+	minlevel = INT_MAX;
+	tl = knowledgeSet (sys->know);
+	while (tl != NULL)
+	{
+		unsigned int l;
+
+		l = termHidelevel (t, tl->term);
+		if (l < minlevel)
+		{
+			minlevel = l;
+		}
+		tl = tl->next;
+	}
+	termlistDelete (tl);
+
+	return minlevel;
+}
+
+//! Check hide levels
+void
+hidelevelCompute (const System sys)
+{
+	Termlist tl;
+
+	sys->hidden = NULL;
+	tl = sys->globalconstants;
+	eprintf ("Global constants: ");
+	termlistPrint (tl);
+	eprintf ("\n");
+
+	while (tl != NULL)
+	{
+		unsigned int l1,l2,l;
+
+		l1 = knowledgeHidelevel (sys, tl->term);
+		l2 = protocolHidelevel (sys, tl->term);
+		if (l1 < l2)
+		{
+			l = l1;
+		}
+		else
+		{
+			l = l2;
+		}
+
+		// Interesting only if higher than zero
+		if (l > 0)
+		{
+			Hiddenterm ht;
+
+			ht = (Hiddenterm) memAlloc (sizeof (struct hiddenterm));
+			ht->term = tl->term;
+			ht->hideminimum = l;
+			ht->hideprotocol = l2;
+			ht->hideknowledge = l1;
+			ht->next = sys->hidden;
+			sys->hidden = ht;
+
+#ifdef DEBUG
+			eprintf ("Added possibly interesting term: ");
+			termPrint (tl->term);
+			eprintf ("; know %i, prot %i\n", l1,l2);
+#endif
+		}
+
+		tl = tl->next;
+	}
+}
+
+
+//! Given a term, iterate over all factors
+int iterate_interesting (const System sys, const Term goalterm, int (*func) ())
+{
+	Hiddenterm ht;
+
+	ht = sys->hidden;
+	while (ht != NULL)
+	{
+		unsigned int l;
+		// Test the goalterm for occurrences of this
+
+		l = termHidelevel (ht->term, goalterm);
+		if (l < INT_MAX)
+		{
+			if (!func (l, ht->hideminimum, ht->hideprotocol, ht->hideknowledge))
+			{
+				return false;
+			}
+		}
+
+		ht = ht->next;
+	}
+	return true;
+}
+
+//! Determine whether a goal might be interesting from the viewpoint of hide levels (the highest minimum is best)
+int hidelevelInteresting (const System sys, const Term goalterm)
+{
+	int uninteresting (unsigned int l, unsigned int lmin, unsigned int lprot, unsigned int lknow)
+	{
+		if (lmin > 0)
+		{
+			// anything higher than usual is interesting :)
+			return false;
+		}
+		return true;
+	}
+
+	return !iterate_interesting (sys, goalterm, uninteresting);
+}
+
+//! Determine whether a goal is impossible to satisfy because of the hidelevel lemma.
+int hidelevelImpossible (const System sys, const Term goalterm)
+{
+	int possible (unsigned int l, unsigned int lmin, unsigned int lprot, unsigned int lknow)
+	{
+		if (l < lmin)
+		{
+			// impossible, abort!
+			return false;
+		}
+		return true;
+	}
+
+	return !iterate_interesting (sys, goalterm, possible);
+}
+

src/hidelevel.h

@@ -0,0 +1,16 @@
+#ifndef HIDELEVELS
+#define HIDELEVELS
+
+#include "term.h"
+#include "system.h"
+
+/*
+ * The structure hiddenterm/Hiddenterm is defined in system.h
+ */
+
+void hidelevelCompute (const System sys);
+int hidelevelInteresting (const System sys, const Term goalterm);
+int hidelevelImpossible (const System sys, const Term goalterm);
+
+#endif
+

src/hidelevel.txt

@@ -0,0 +1,31 @@
+Implemented: 
+
+- scans
+- test functions (in hidelevel.c)
+
+TODO:
+
+- use test functions (impossible for pruning, interesting for goal selection heuristic)
+- state count display switch for comparisons
+- consider adding info for goal stuff (only from M_0, not by create)
+
+*******************************************************************
+
+roivas:~scyther% ./scyther ccitt509-1c.spdl
+Global constants: [te, ne, Eve, Bob, Alice, unhash, sk, hash, pk]
+
+Possibly interesting term: unhash; know 2147483647, prot 2147483647
+Possibly interesting term: sk; know 1, prot 2
+
+
+roivas:~scyther% ./scyther yahalom.spdl
+warning: variable T was declared in role yahalom,R but never used in a read event.
+Global constants: [Simon, Bob, Alice, Compromised, Fresh, k]
+
+Possibly interesting term: k; know 2147483647, prot 2
+
+
+roivas:~scyther% ./scyther ns3.spdl
+Global constants: [Eve, sk, pk]
+
+Possibly interesting term: sk; know 1, prot 2147483647

src/system.c

@@ -67,6 +67,8 @@ systemInit ()
   sys->locals = NULL;
   sys->variables = NULL;
   sys->untrusted = NULL;
+  sys->globalconstants = NULL;
+  sys->hidden = NULL;
   sys->secrets = NULL;		// list of claimed secrets
   sys->synchronising_labels = NULL;
   sys->attack = NULL;		// clash with prev. attack declaration TODO

src/system.h

@@ -100,6 +100,19 @@ struct tracebuf
   Varbuf variables;
 };
 
+//! Structure for information on special terms (cacheing)
+struct hiddenterm
+{
+  Term term;
+  unsigned int hideminimum;
+  unsigned int hideprotocol;
+  unsigned int hideknowledge;
+  struct hiddenterm *next;
+};
+
+//! Pointer shorthand
+typedef struct hiddenterm *Hiddenterm;
+
 //! The main state structure.
 struct system
 {
@@ -136,6 +149,8 @@ struct system
   Termlist locals;		//!< List of local terms
   Termlist variables;		//!< List of all variables
   Termlist untrusted;		//!< List of untrusted agent names
+  Termlist globalconstants;	//!< List of global constants
+  Hiddenterm hidden;		//!< List of hiddenterm constructs for Hidelevel lemma
 
   /* protocol preprocessing */
   int rolecount;		//!< Number of roles in the system
@@ -166,6 +181,7 @@ struct system
 
 typedef struct system *System;
 
+
 System systemInit ();
 void systemReset (const System sys);
 void systemRuns (const System sys);

src/term.c

@@ -1378,3 +1378,52 @@ getTermFunction (Term t)
     }
   return NULL;
 }
+
+//! Return hidelevel for a single term within another
+unsigned int
+termHidelevel (const Term tsmall, Term tbig)
+{
+  tbig = deVar (tbig);
+  if (isTermEqual (tsmall, tbig))
+    {
+      // It's simply here: not hidden at any level
+      return 0;
+    }
+  else
+    {
+      if (realTermLeaf (tbig))
+	{
+	  // Not here: infinitely hidden
+	  return INT_MAX;
+	}
+      else
+	{
+	  // Nested term
+	  unsigned int t1, t2;
+
+	  if (realTermTuple (tbig))
+	    {
+	      // Tupling
+	      t1 = termHidelevel (tsmall, TermOp1 (tbig));
+	      t2 = termHidelevel (tsmall, TermOp2 (tbig));
+	    }
+	  else
+	    {
+	      // Encryption
+	      t1 = termHidelevel (tsmall, TermOp (tbig));
+	      t2 = termHidelevel (tsmall, TermKey (tbig));
+	      if (t2 < INT_MAX)
+		t2++;
+	    }
+	  // Return minimum
+	  if (t1 < t2)
+	    {
+	      return t1;
+	    }
+	  else
+	    {
+	      return t2;
+	    }
+	}
+    }
+}

src/term.h

@@ -201,6 +201,7 @@ int isLeafNameEqual (Term t1, Term t2);
 Term freshTermPrefix (Term prefixterm);
 int isTermFunctionName (Term t);
 Term getTermFunction (Term t);
+unsigned int termHidelevel (const Term tsmall, Term tbig);
 
 
 #endif