From d7e49028c15efe85c764b8ec1ad0a5652897cdd2 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Fri, 20 Aug 2004 14:55:34 +0000
Subject: [PATCH] - Added pruning of functions the intruder does not know (e.g.
 SK)

---
 src/arachne.c | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/src/arachne.c b/src/arachne.c
index 09a22df..50c5bcc 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -1253,6 +1253,25 @@ prune_theorems ()
 	  return 1;
 	}
 
+      // Check for SK-type function occurrences
+      //!@todo Needs a LEMMA, although this seems to be quite straightforward to prove.
+      // The idea is that functions are never sent as a whole, but only used in applications.
+      if (isTermFunctionName (b->term))
+	{
+	  if (!inKnowledge (sys->know, b->term))
+	    {
+	      // Not in initial knowledge of the intruder
+	      if (sys->output == PROOF)
+		{
+		  indentPrint ();
+		  eprintf ("Pruned because the function ");
+		  termPrint (b->term);
+		  eprintf (" is not known initially to the intruder.\n");
+		}
+	      return 1;
+	    }
+	}
+
       bl = bl->next;
     }