- Removed some too interesting pruning methods that really need theorems

first. Revealed by the certified e-mail protocol by Abadi and
  Blanchet.

src/arachne.c

@@ -1452,8 +1452,6 @@ bind_goal (const Binding b)
   if (!b->done)
     {
       int flag;
-      int know_only;
-      Term function;
 
       flag = 1;
       proof_select_goal (b);
@@ -1481,26 +1479,35 @@ bind_goal (const Binding b)
 	}
       else
 	{
-	  // Prune: if it is an SK type construct, ready
-	  // No regular run will apply SK for you.
-	  //!@todo This still needs a lemma, and a more generic (correct) algorithm!!
+	  int know_only;
 
 	  know_only = 0;
-	  function = getTermFunction (b->term);
-	  if (function != NULL)
+
+	  if (1 == 0)		// blocked for now
 	    {
-	      if (!inKnowledge (sys->know, function))
+	      // Prune: if it is an SK type construct, ready
+	      // No regular run will apply SK for you.
+	      //!@todo This still needs a lemma, and a more generic (correct) algorithm!! It is currently
+	      // actually false, e.g. for signing protocols, and password-like functions.
+	      //
+	      Term function;
+
+	      function = getTermFunction (b->term);
+	      if (function != NULL)
 		{
-		  // Prune because we didn't know it before, and it is never subterm-sent
-		  if (switches.output == PROOF)
+		  if (!inKnowledge (sys->know, function))
 		    {
-		      indentPrint ();
-		      eprintf ("* Because ");
-		      termPrint (b->term);
-		      eprintf
-			(" is never sent from a regular run, so we only intruder construct it.\n");
+		      // Prune because we didn't know it before, and it is never subterm-sent
+		      if (switches.output == PROOF)
+			{
+			  indentPrint ();
+			  eprintf ("* Because ");
+			  termPrint (b->term);
+			  eprintf
+			    (" is never sent from a regular run, so we only intruder construct it.\n");
+			}
+		      know_only = 1;
 		    }
-		  know_only = 1;
 		}
 	    }
 

src/prune_theorems.c

@@ -259,18 +259,25 @@ prune_theorems (const System sys)
       // Check for encryption levels
       /*
        * if (switches.match < 2
+       *!@todo Doesn't work yet as desired for Tickets. Prove lemma first.
        */
-      if (term_encryption_level (b->term) > max_encryption_level)
+      if (switches.experimental)
 	{
-	  // Prune: we do not need to construct such terms
-	  if (switches.output == PROOF)
+	  if (!hasTicketSubterm (b->term))
 	    {
-	      indentPrint ();
-	      eprintf ("Pruned because the encryption level of ");
-	      termPrint (b->term);
-	      eprintf (" is too high.\n");
+	      if (term_encryption_level (b->term) > max_encryption_level)
+		{
+		  // Prune: we do not need to construct such terms
+		  if (switches.output == PROOF)
+		    {
+		      indentPrint ();
+		      eprintf ("Pruned because the encryption level of ");
+		      termPrint (b->term);
+		      eprintf (" is too high.\n");
+		    }
+		  return 1;
+		}
 	    }
-	  return 1;
 	}
 
       // Check for SK-type function occurrences

src/specialterm.c

@@ -62,3 +62,35 @@ specialTermInit (const System sys)
   CLAIMS_dep_prec = termlistAdd (CLAIMS_dep_prec, CLAIM_Nisynch);
 
 }
+
+//! Determine whether this is a leaf construct with a ticket in it
+int
+isTicketTerm (Term t)
+{
+  if (t != NULL)
+    {
+      if (realTermLeaf (t))
+	{
+	  if (inTermlist (t->stype, TERM_Ticket))
+	    {
+	      return true;
+	    }
+	  else
+	    {
+	      if (realTermVariable (t))
+		{
+		  return isTicketTerm (t->subst);
+		}
+	    }
+	}
+    }
+  return false;
+}
+
+//! Determine whether this is a term with a Ticket in it
+int
+hasTicketSubterm (Term t)
+{
+  // Doesn't work yet
+  return true;
+}

src/specialterm.h

@@ -25,4 +25,7 @@ extern Term CLAIM_Reachable;
 
 extern Termlist CLAIMS_dep_prec;
 
+int isTicketTerm (Term t);
+int hasTicketSubterm (Term t);
+
 #endif

src/term.c

@@ -1094,11 +1094,18 @@ term_rolelocals_are_variables ()
 }
 
 //! Count the encryption level of a term
+/**
+ * Note that this stops at any variable that is of ticket type.
+ */
 int
 term_encryption_level (const Term term)
 {
   int iter_maxencrypt (Term t)
   {
+    if (isTicketTerm (t))
+      {
+	return 0;
+      }
     t = deVar (t);
     if (t == NULL)
       {