diff --git a/src/arachne.c b/src/arachne.c
index 35d0bcc..d6bca88 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -787,7 +787,7 @@ createDecryptionChain (const Binding b, const int run, const int index,
       indentDepth++;
 
       tdecr = keylist->term;
-      tkey = inverseKey (sys->know->inverses, TermKey (tdecr));
+      tkey = inverseKey (sys->know, TermKey (tdecr));
       smallrun = create_decryptor (tdecr, tkey);
       {
 	Roledef rddecrypt;
diff --git a/src/compiler.c b/src/compiler.c
index cd8a726..d6c2a4c 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -1101,7 +1101,7 @@ hashfunctions (Tac tcstart)
 	  error
 	    ("Bug in hashfunction generation code. Please contact the authors.\n");
 	}
-      knowledgeAddInverse (sys->know, hfuncs->term, hinvs->term);
+      knowledgeAddInverseKeys (sys->know, hfuncs->term, hinvs->term);
       hfuncs->term->stype = termlistAdd (NULL, TERM_Function);
       hinvs->term->stype = termlistAdd (NULL, TERM_Function);
       hfuncs = hfuncs->next;
@@ -1157,8 +1157,12 @@ normalDeclaration (Tac tc)
       knowledgeAddTermlist (sys->know, tacTermlist (tc->t1.tac));
       break;
     case TAC_INVERSEKEYS:
-      knowledgeAddInverse (sys->know, tacTerm (tc->t1.tac),
-			   tacTerm (tc->t2.tac));
+      knowledgeAddInverseKeys (sys->know, tacTerm (tc->t1.tac),
+			       tacTerm (tc->t2.tac));
+      break;
+    case TAC_INVERSEKEYFUNCTIONS:
+      knowledgeAddInverseKeyFunctions (sys->know, tacTerm (tc->t1.tac),
+				       tacTerm (tc->t2.tac));
       break;
     case TAC_HASHFUNCTION:
       hashfunctions (tc);
@@ -1568,8 +1572,14 @@ tacProcess (Tac tc)
 Term
 tacTerm (Tac tc)
 {
+  Term t;
+
   switch (tc->op)
     {
+    case TAC_FCALL:
+      t = makeTermEncrypt (tacTerm (tc->t1.tac), tacTerm (tc->t2.tac));
+      t->helper.fcall = true;
+      return t;
     case TAC_ENCRYPT:
       return makeTermEncrypt (tacTerm (tc->t1.tac), tacTerm (tc->t2.tac));
     case TAC_TUPLE:
diff --git a/src/dotout.c b/src/dotout.c
index 555680c..e380fab 100644
--- a/src/dotout.c
+++ b/src/dotout.c
@@ -96,7 +96,7 @@ isIntruderChoice (const Term t)
 	{
 	  // Chosen by intruder
 	  // However, if it is a rolename, this is not really what we mean
-	  if (!(t->roleVar || isAgentType (t->stype)))
+	  if (!(t->helper.roleVar || isAgentType (t->stype)))
 	    {
 	      // Not a role variable, and chosen by the intruder: that's it
 	      return true;
@@ -187,12 +187,12 @@ explainVariable (Term t)
   if (realTermVariable (t))
     {
       eprintf ("any ");
-      if (t->roleVar)
+      if (t->helper.roleVar)
 	{
 	  eprintf ("agent ");
 	}
       termPrintRemap (t);
-      if (!t->roleVar)
+      if (!t->helper.roleVar)
 	{
 	  if (switches.match == 0 && t->stype != NULL)
 	    {
diff --git a/src/knowledge.c b/src/knowledge.c
index 2c2202a..51a0adb 100644
--- a/src/knowledge.c
+++ b/src/knowledge.c
@@ -30,19 +30,10 @@
 #include "system.h"
 #include "debug.h"
 #include "error.h"
+#include "specialterm.h"
 
 /*
  * Knowledge stuff
- *
- * Note that a really weird thing is going on involving unpropagated substitutions.
- * Idea:
- *
- * 1. Substitute terms by filling in ->subst.
- * Now, either:
- * 2a. Undo this by knowledgeUndo.
- * 2b. Propagate it, modifying the knowledge beyond repair by knowledgeSubstDo. Now inKnowledge works again.
- * 2c. inKnowledge/knowledgeSet if something is in the knowledge: this does not consider the substitutions!, and 
- *     they now have some overhead.
  */
 
 //! Open knowledge code.
@@ -81,7 +72,8 @@ emptyKnowledge ()
   know = makeKnowledge ();
   know->basic = NULL;
   know->encrypt = NULL;
-  know->inverses = NULL;
+  know->inversekeys = NULL;
+  know->inversekeyfunctions = NULL;
   know->vars = NULL;
   know->publicfunctions = NULL;
   return know;
@@ -110,7 +102,8 @@ knowledgeDuplicate (Knowledge know)
   newknow->basic = termlistShallow (know->basic);
   newknow->encrypt = termlistShallow (know->encrypt);
   newknow->vars = termlistShallow (know->vars);
-  newknow->inverses = know->inverses;
+  newknow->inversekeys = know->inversekeys;
+  newknow->inversekeyfunctions = know->inversekeyfunctions;
   newknow->publicfunctions = termlistShallow (know->publicfunctions);
   return newknow;
 }
@@ -147,7 +140,8 @@ knowledgeDestroy (Knowledge know)
       termlistDestroy (know->basic);
       termlistDestroy (know->encrypt);
       termlistDestroy (know->vars);
-      // termlistDestroy(know->inverses);
+      // termlistDestroy(know->inversekeys);
+      // termlistDestroy(know->inversekeyfunctions);
       termlistDestroy (know->publicfunctions);
       free (know);
     }
@@ -195,7 +189,7 @@ knowledgeAddTerm (Knowledge know, Term term)
     }
   if (term->type == ENCRYPT)
     {
-      Term invkey = inverseKey (know->inverses, TermKey (term));
+      Term invkey = inverseKey (know, TermKey (term));
       if (inKnowledge (know, invkey))
 	{
 	  /* we can decrypt it */
@@ -227,7 +221,7 @@ knowledgeSimplify (Knowledge know, Term key)
 {
   Termlist tldecrypts = NULL;
   Termlist scan = know->encrypt;
-  Term invkey = inverseKey (know->inverses, key);
+  Term invkey = inverseKey (know, key);
 
   while (scan != NULL)
     {
@@ -257,6 +251,7 @@ knowledgeAddTermlist (Knowledge know, Termlist tl)
 
   while (tl != NULL)
     {
+      // Evil old fashioned code relies on lazy left-to-right parsing. Get rid of it.
       flag = knowledgeAddTerm (know, tl->term) || flag;
       tl = tl->next;
     }
@@ -265,21 +260,18 @@ knowledgeAddTermlist (Knowledge know, Termlist tl)
 
 //! Add an inverse pair to the knowledge
 void
-knowledgeAddInverse (Knowledge know, Term t1, Term t2)
+knowledgeAddInverseKeys (Knowledge know, Term t1, Term t2)
 {
-  know->inverses = termlistAdd (know->inverses, t1);
-  know->inverses = termlistAdd (know->inverses, t2);
-  return;
+  know->inversekeys = termlistAdd (know->inversekeys, t1);
+  know->inversekeys = termlistAdd (know->inversekeys, t2);
 }
 
-//! Set an inverse pair list for the knowledge.
-/**
- * List pointer is simply copied, so don't delete it later!
- */
+//! Add an inverse pair to the knowledge
 void
-knowledgeSetInverses (Knowledge know, Termlist tl)
+knowledgeAddInverseKeyFunctions (Knowledge know, Term t1, Term t2)
 {
-  know->inverses = tl;
+  know->inversekeyfunctions = termlistAdd (know->inversekeyfunctions, t1);
+  know->inversekeyfunctions = termlistAdd (know->inversekeyfunctions, t2);
 }
 
 //! Is a term a part of the knowledge?
@@ -341,6 +333,15 @@ knowledgePrint (Knowledge know)
   eprintf (" [Vars]: ");
   termlistPrint (know->vars);
   eprintf ("\n");
+  eprintf (" [Inversekeys]: ");
+  termlistPrint (know->inversekeys);
+  eprintf ("\n");
+  eprintf (" [Inversekeyfunctions]: ");
+  termlistPrint (know->inversekeyfunctions);
+  eprintf ("\n");
+  eprintf (" [Publicfunctions]: ");
+  termlistPrint (know->publicfunctions);
+  eprintf ("\n");
 }
 
 //! Print a knowledge set, short version (no newline)
@@ -368,43 +369,6 @@ knowledgePrintShort (const Knowledge know)
     }
 }
 
-//! Print the inverses list of a knowledge set.
-void
-knowledgeInversesPrint (Knowledge know)
-{
-  Termlist tl;
-  int after = 0;
-
-  if (know == NULL)
-    {
-      eprintf ("Empty knowledge.");
-      return;
-    }
-
-  tl = knowledgeGetInverses (know);
-  if (tl == NULL)
-    {
-      eprintf ("None.");
-    }
-  else
-    {
-      while (tl != NULL && tl->next != NULL)
-	{
-	  if (after)
-	    {
-	      eprintf (",");
-	    }
-	  eprintf ("(");
-	  termPrint (tl->term);
-	  eprintf (",");
-	  termPrint (tl->next->term);
-	  eprintf (")");
-	  after = 1;
-	  tl = tl->next->next;
-	}
-    }
-}
-
 //! Yield the set of representatives for the knowledge.
 /**
  * Note: this is a shallow copy, and needs to be termlistDelete'd.
@@ -420,17 +384,11 @@ knowledgeSet (const Knowledge know)
   return termlistConcat (tl1, tl2);
 }
 
-//! Get the inverses pointer of the knowledge.
-/**
- * Essentially the inverse function of knowledgeSetInverses()
- */
-Termlist
-knowledgeGetInverses (const Knowledge know)
+//! Check for elements in the knowledge set
+int
+inKnowledgeSet (const Knowledge know, Term t)
 {
-  if (know == NULL)
-    return NULL;
-  else
-    return know->inverses;
+  return (inTermlist (know->basic, t) || inTermlist (know->encrypt, t));
 }
 
 //! check whether any substitutions where made in a knowledge set.
@@ -457,37 +415,6 @@ knowledgeSubstNeeded (const Knowledge know)
   return 0;
 }
 
-//! Reconstruct a knowledge set.
-/**
- * This is useful after e.g. substitutions.
- * Just rebuilds the knowledge in a new (shallow) copy.
- *@return The pointer to the new knowledge.
- *\sa knowledgeSubstNeeded()
- */
-Knowledge
-knowledgeReconstruction (const Knowledge know)
-{
-  Knowledge newknow = emptyKnowledge ();
-
-  newknow->inverses = know->inverses;
-  knowledgeAddTermlist (newknow, know->basic);
-  knowledgeAddTermlist (newknow, know->encrypt);
-  return newknow;
-}
-
-//! Propagate any substitutions just made.
-/**
- * This usually involves reconstruction of the complete knowledge, which is
- * 'cheaper' than a thorough analysis, so we always make a copy.
- *\sa knowledgeReconstruction()
- */
-Knowledge
-knowledgeSubstDo (const Knowledge know)
-{
-  /* otherwise a copy (for deletion) is returned. */
-  return knowledgeReconstruction (know);
-}
-
 //! Add public function
 void
 knowledgeAddPublicFunction (const Knowledge know, const Term f)
@@ -502,3 +429,62 @@ isKnowledgePublicFunction (const Knowledge know, const Term f)
 {
   return inTermlist (know->publicfunctions, f);
 }
+
+//! Give the inverse key term of a term.
+/**
+ * Gives a duplicate of the inverse Key of some term (which is used to encrypt something), as is defined
+ * by the termlist, which is a list of key1,key1inv, key2, key2inv, etc...
+ *@param inverses The list of inverses, typically from the knowledge.
+ *@param key Any term of which the inverse will be determined.
+ *@return A pointer to a duplicate of the inverse key term. Use termDelete to remove it.
+ *\sa termDuplicate(), knowledge::inverses
+ */
+Term
+inverseKey (Knowledge know, Term key)
+{
+  Term f;
+
+  key = deVar (key);
+
+  /* inverse key function? */
+  f = getTermFunction (key);
+  if (f != NULL)
+    {
+      Termlist tl;
+
+      Term funKey (Term orig, Term f)
+      {
+	/* in: f'{op}, f
+	 * out: f{op'} */
+	return makeTermFcall (termDuplicate (TermOp (orig)),
+			      termDuplicate (f));
+      }
+
+      tl = know->inversekeyfunctions;
+      while (tl != NULL && tl->next != NULL)
+	{
+	  if (isTermEqual (TermKey (key), tl->term))
+	    return funKey (key, tl->next->term);
+	  if (isTermEqual (TermKey (key), tl->next->term))
+	    return funKey (key, tl->term);
+	  tl = tl->next->next;
+	}
+    }
+  else
+    {
+      /* scanning for a direct inverse */
+      Termlist tl;
+
+      /* scan the list */
+      tl = know->inversekeys;
+      while (tl != NULL && tl->next != NULL)
+	{
+	  if (isTermEqual (key, tl->term))
+	    return termDuplicate (tl->next->term);
+	  if (isTermEqual (key, tl->next->term))
+	    return termDuplicate (tl->term);
+	  tl = tl->next->next;
+	}
+    }
+  return termDuplicate (key);	/* defaults to symmetrical */
+}
diff --git a/src/knowledge.h b/src/knowledge.h
index 18d15d1..d9fa009 100644
--- a/src/knowledge.h
+++ b/src/knowledge.h
@@ -33,8 +33,10 @@ struct knowledge
   Termlist basic;
   //! A list of terms encrypted, such that the inverse is not in the knowledge set.
   Termlist encrypt;
-  //! List of inverse pairs (thus length of list is even)
-  Termlist inverses;
+  //! List of inverse pairs (thus length of list is even) (add,sub)
+  Termlist inversekeys;
+  //! List of inverse pairs (thus length of list is even) (pk,sk)
+  Termlist inversekeyfunctions;
   //! List of open variables in the knowledge set.
   /**
    * This list is used to determine whether the knowledge needs to be rewritten.
@@ -42,7 +44,7 @@ struct knowledge
    * and we need to reconstruct the knowledge set.
    */
   Termlist vars;		// special: denotes unsubstituted variables
-  //! A list of public functions
+  //! A list of hash functions
   Termlist publicfunctions;
 };
 
@@ -58,19 +60,19 @@ void knowledgeDelete (Knowledge know);
 void knowledgeDestroy (Knowledge know);
 int knowledgeAddTerm (Knowledge know, Term term);
 int knowledgeAddTermlist (Knowledge know, Termlist tl);
-void knowledgeAddInverse (Knowledge know, Term t1, Term t2);
-void knowledgeSetInverses (Knowledge know, Termlist tl);
+void knowledgeAddInverseKeys (Knowledge know, Term t1, Term t2);
+void knowledgeAddInverseKeyFunctions (Knowledge know, Term t1, Term t2);
+int inKnowledgeSet (const Knowledge know, Term t);
 void knowledgeSimplify (Knowledge know, Term decryptkey);
 int inKnowledge (const Knowledge know, Term term);
 void knowledgePrint (Knowledge know);
 void knowledgePrintShort (const Knowledge know);
-void knowledgeInversesPrint (Knowledge know);
 Termlist knowledgeSet (const Knowledge know);
-Termlist knowledgeGetInverses (const Knowledge know);
 int knowledgeSubstNeeded (const Knowledge know);
 Knowledge knowledgeSubstDo (const Knowledge know);
 void knowledgeAddPublicFunction (const Knowledge know, const Term f);
 int isKnowledgePublicFunction (const Knowledge know, const Term f);
+Term inverseKey (Knowledge know, Term key);
 
 //! Harnass macro for recursive procedures.
 #define mindwipe(k,recurse) \
diff --git a/src/main.c b/src/main.c
index 8efbdd5..94b48f9 100644
--- a/src/main.c
+++ b/src/main.c
@@ -149,9 +149,6 @@ main (int argc, char **argv)
       termlistPrint (sys->untrusted);
       printf ("\n");
       knowledgePrint (sys->know);
-      printf ("inverses: ");
-      knowledgeInversesPrint (sys->know);
-      printf ("\n");
       locVarPrint (sys->locals);
       protocolsPrint (sys->protocols);
 
diff --git a/src/parser.y b/src/parser.y
index ad01666..4d8c01d 100644
--- a/src/parser.y
+++ b/src/parser.y
@@ -82,6 +82,7 @@ List findMacroDefinition(Symbol s)
 %token 		SECRET
 %token 		COMPROMISED
 %token 		INVERSEKEYS
+%token 		INVERSEKEYFUNCTIONS
 %token 		UNTRUSTED
 %token 		USERTYPE
 %token		SINGULAR
@@ -356,6 +357,12 @@ declaration	: secretpref CONST basictermlist typeinfo1 ';'
 			t->t2.tac = $5;
 			$$ = t;
 		  }
+		| INVERSEKEYFUNCTIONS '(' term ',' term ')' ';'
+		  {	Tac t = tacCreate(TAC_INVERSEKEYFUNCTIONS);
+			t->t1.tac = $3;
+			t->t2.tac = $5;
+			$$ = t;
+		  }
 		| COMPROMISED termlist ';'
 		  {	Tac t = tacCreate(TAC_COMPROMISED);
 		  	t->t1.tac= $2;
@@ -456,7 +463,7 @@ term  		: ID '(' termlist ')'
 		  {
 		  	Tac t = tacCreate(TAC_STRING);
 			t->t1.sym = $1;
-			$$ = tacJoin(TAC_ENCRYPT,tacTuple($3),t,NULL);
+			$$ = tacJoin(TAC_FCALL,tacTuple($3),t,NULL);
 		  }
 		| '{' termlist '}' key
 		  {
diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time
deleted file mode 100644
index 80f32ca..0000000
--- a/src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time	
+++ /dev/null
@@ -1,2 +0,0 @@
-Passed wall time in seconds:
-0
diff --git a/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time
index 97d01d7..afe3b53 100644
--- a/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time	
+++ b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time	
@@ -1,2 +1,2 @@
 Passed wall time in seconds:
-14
+15
diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time
index 37da462..0541820 100644
--- a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time	
+++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time	
@@ -1,2 +1,2 @@
 Passed wall time in seconds:
-23
+24
diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time
index 27fb100..d1a00da 100644
--- a/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time	
+++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time	
@@ -1,2 +1,2 @@
 Passed wall time in seconds:
-28
+29
diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out
index cdd6305..20b5520 100644
--- a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out	
+++ b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out	
@@ -1,6 +1,6 @@
-claim	spliceAS-HC,I	Secret_7	N2	Ok	[no attack within bounds]	time=60
-claim	spliceAS-HC,I	Niagree_9	-	Ok	[does not occur]	time=60
-claim	spliceAS-HC,I	Nisynch_10	-	Ok	[does not occur]	time=60
-claim	spliceAS-HC,R	Secret_8	N2	Ok	[no attack within bounds]	time=60
-claim	spliceAS-HC,R	Niagree_11	-	Ok	[does not occur]	time=60
-claim	spliceAS-HC,R	Nisynch_12	-	Ok	[does not occur]	time=60
+claim	spliceAS-HC,I	Secret_7	N2	Fail	[at least 7 attacks]
+claim	spliceAS-HC,I	Niagree_9	-	Fail	[at least 1 attack]
+claim	spliceAS-HC,I	Nisynch_10	-	Fail	[at least 1 attack]
+claim	spliceAS-HC,R	Secret_8	N2	Fail	[at least 7 attacks]
+claim	spliceAS-HC,R	Niagree_11	-	Fail	[at least 1 attack]
+claim	spliceAS-HC,R	Nisynch_12	-	Fail	[at least 1 attack]
diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time
index df21598..2eb5ce9 100644
--- a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time	
+++ b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time	
@@ -1,2 +1,2 @@
 Passed wall time in seconds:
-60
+6
diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out
index a8474fb..a91f153 100644
--- a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out	
+++ b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out	
@@ -1,6 +1,6 @@
-claim	spliceAS,I	Secret_7	N2	Ok	[no attack within bounds]	time=60
-claim	spliceAS,I	Niagree_9	-	Ok	[does not occur]	time=60
-claim	spliceAS,I	Nisynch_10	-	Ok	[does not occur]	time=60
-claim	spliceAS,R	Secret_8	N2	Ok	[no attack within bounds]	time=60
-claim	spliceAS,R	Niagree_11	-	Ok	[does not occur]	time=60
-claim	spliceAS,R	Nisynch_12	-	Ok	[does not occur]	time=60
+claim	spliceAS,I	Secret_7	N2	Fail	[at least 7 attacks]
+claim	spliceAS,I	Niagree_9	-	Fail	[at least 1 attack]
+claim	spliceAS,I	Nisynch_10	-	Fail	[at least 1 attack]
+claim	spliceAS,R	Secret_8	N2	Fail	[at least 7 attacks]
+claim	spliceAS,R	Niagree_11	-	Fail	[at least 1 attack]
+claim	spliceAS,R	Nisynch_12	-	Fail	[at least 1 attack]
diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time
index df21598..2eb5ce9 100644
--- a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time	
+++ b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time	
@@ -1,2 +1,2 @@
 Passed wall time in seconds:
-60
+6
diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time
index b449a72..7ec870e 100644
--- a/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time	
+++ b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time	
@@ -1,2 +1,2 @@
 Passed wall time in seconds:
-36
+37
diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time
deleted file mode 100644
index 80f32ca..0000000
--- a/src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time	
+++ /dev/null
@@ -1,2 +0,0 @@
-Passed wall time in seconds:
-0
diff --git a/src/role.c b/src/role.c
index 139fa5f..70d4413 100644
--- a/src/role.c
+++ b/src/role.c
@@ -415,7 +415,7 @@ Readable (Knowledge know, Term t)
 		  return true;
 		}
 	      // Right disjunct
-	      inv = inverseKey (know->inverses, TermKey (t));
+	      inv = inverseKey (know, TermKey (t));
 	      either = false;
 	      if (inKnowledge (know, inv))
 		{
diff --git a/src/scanner.l b/src/scanner.l
index 7fd1570..df6152f 100644
--- a/src/scanner.l
+++ b/src/scanner.l
@@ -171,6 +171,7 @@ claim		{ return CLAIMT; }
 run		{ return RUN; }
 secret		{ return SECRET; }
 inversekeys	{ return INVERSEKEYS; }
+inversekeyfunctions	{ return INVERSEKEYFUNCTIONS; }
 untrusted	{ return UNTRUSTED; }
 compromised	{ return COMPROMISED; }
 usertype	{ return USERTYPE; }
diff --git a/src/specialterm.c b/src/specialterm.c
index 774ae87..aa67649 100644
--- a/src/specialterm.c
+++ b/src/specialterm.c
@@ -119,7 +119,7 @@ specialTermInit (const System sys)
   langcons (TERM_PK, "pk", TERM_Function);
   langcons (TERM_SK, "sk", TERM_Function);
   langcons (TERM_K, "k", TERM_Function);
-  knowledgeAddInverse (sys->know, TERM_PK, TERM_SK);
+  knowledgeAddInverseKeyFunctions (sys->know, TERM_PK, TERM_SK);
   knowledgeAddTerm (sys->know, TERM_PK);
 
   /* Define a prefix for labels for the match function */
diff --git a/src/system.c b/src/system.c
index f7fa2ad..9ea0a88 100644
--- a/src/system.c
+++ b/src/system.c
@@ -504,7 +504,7 @@ roleInstanceArachne (const System sys, const Protocol protocol,
 	newt = makeTermType (GLOBAL, TermSymb (oldt), rid);
       }
     newt->stype = oldt->stype;	// copy list of types
-    newt->roleVar = isrole;	// set role status
+    newt->helper.roleVar = isrole;	// set role status
 
     // Add to copy list
     TERMLISTADD (fromlist, oldt);
diff --git a/src/tac.h b/src/tac.h
index 0cbbaa0..2d303d1 100644
--- a/src/tac.h
+++ b/src/tac.h
@@ -32,6 +32,7 @@ enum tactypes
   TAC_SYM,
   TAC_TUPLE,
   TAC_ENCRYPT,
+  TAC_FCALL,
   TAC_VAR,
   TAC_CONST,
   TAC_FRESH,
@@ -48,6 +49,7 @@ enum tactypes
   TAC_ROLEREF,
   TAC_SECRET,
   TAC_INVERSEKEYS,
+  TAC_INVERSEKEYFUNCTIONS,
   TAC_HASHFUNCTION,
   TAC_UNTRUSTED,
   TAC_COMPROMISED,
diff --git a/src/term.c b/src/term.c
index 6fb42bb..f9517b6 100644
--- a/src/term.c
+++ b/src/term.c
@@ -84,6 +84,9 @@ makeTerm ()
 
 //! Create a fresh encrypted term from two existing terms.
 /**
+ * The first argument is the message,
+ * the second argument is the key.
+ *
  *@return A pointer to the new term.
  */
 Term
@@ -92,11 +95,32 @@ makeTermEncrypt (Term t1, Term t2)
   Term term = makeTerm ();
   term->type = ENCRYPT;
   term->stype = NULL;
+  term->helper.fcall = false;
+  term->subst = NULL;
   TermOp (term) = t1;
   TermKey (term) = t2;
   return term;
 }
 
+Term
+makeTermFcall (Term t1, Term t2)
+//! Create a fresh function application term from two existing terms.
+/**
+ * The first argument is the function argument,
+ * the second argument is the function (name).
+ *
+ * These behave like encryptions in most cases.
+ *
+ *@return A pointer to the new term.
+ */
+{
+  Term t;
+
+  t = makeTermEncrypt (t1, t2);
+  t->helper.fcall = true;
+  return t;
+}
+
 //! Create a fresh term tuple from two existing terms.
 /**
  *@return A pointer to the new term.
@@ -128,7 +152,8 @@ makeTermTuple (Term t1, Term t2)
   tt = makeTerm ();
   tt->type = TUPLE;
   tt->stype = NULL;
-  tt->roleVar = 0;
+  tt->helper.roleVar = 0;
+  tt->subst = NULL;
   TermOp1 (tt) = t1;
   TermOp2 (tt) = t2;
   return tt;
@@ -145,7 +170,16 @@ makeTermType (const int type, const Symbol symb, const int runid)
   Term term = makeTerm ();
   term->type = type;
   term->stype = NULL;
-  term->roleVar = 0;
+  if ((type == ENCRYPT) || (type == TUPLE))
+    {
+      // Non-leaf
+      term->helper.fcall = false;
+    }
+  else
+    {
+      // Leaf
+      term->helper.roleVar = 0;
+    }
   term->subst = NULL;
   TermSymb (term) = symb;
   TermRunid (term) = runid;
@@ -381,8 +415,7 @@ termPrintCustom (Term term, char *leftvar, char *rightvar, char *lefttup,
     }
   if (realTermEncrypt (term))
     {
-      if (isTermLeaf (TermKey (term))
-	  && inTermlist (TermKey (term)->stype, TERM_Function))
+      if (term->helper.fcall)
 	{
 	  /* function application */
 	  termPrintCustom (TermKey (term), leftvar, rightvar, lefttup,
@@ -695,8 +728,12 @@ termRunid (Term term, int runid)
       /* anything else, recurse */
       if (realTermEncrypt (term))
 	{
-	  return makeTermEncrypt (termRunid (TermOp (term), runid),
-				  termRunid (TermKey (term), runid));
+	  Term t;
+
+	  t = makeTermEncrypt (termRunid (TermOp (term), runid),
+			       termRunid (TermKey (term), runid));
+	  t->helper.fcall = term->helper.fcall;
+	  return t;
 	}
       else
 	{
@@ -1159,22 +1196,23 @@ term_encryption_level (const Term term)
       }
     else
       {
+	int l, r;
+
 	if (realTermTuple (t))
 	  {
-	    int l, r;
-
 	    l = iter_maxencrypt (TermOp1 (t));
 	    r = iter_maxencrypt (TermOp2 (t));
-	    if (l > r)
-	      return l;
-	    else
-	      return r;
 	  }
 	else
 	  {
 	    // encrypt
-	    return 1 + iter_maxencrypt (TermOp (t));
+	    l = 1 + iter_maxencrypt (TermOp (t));
+	    r = iter_maxencrypt (TermKey (t));
 	  }
+	if (l > r)
+	  return l;
+	else
+	  return r;
       }
   }
 
@@ -1418,9 +1456,9 @@ Term
 getTermFunction (Term t)
 {
   t = deVar (t);
-  if (t != NULL)
+  if (realTermEncrypt (t))
     {
-      if (realTermEncrypt (t) && isTermFunctionName (TermKey (t)))
+      if (t->helper.fcall)
 	{
 	  return TermKey (t);
 	}
diff --git a/src/term.h b/src/term.h
index fa65a72..c919f2b 100644
--- a/src/term.h
+++ b/src/term.h
@@ -47,7 +47,11 @@ struct term
   //! Data Type termlist (e.g. agent or nonce)
   /** Only for leaves. */
   void *stype;			// list of types
-  int roleVar;			//!< only for leaf, arachne engine: role variable flag
+  union
+  {
+    int roleVar;		//!< only for leaf, arachne engine: role variable flag
+    int fcall;			//!< only for 'encryption' to mark actual function call f(t)
+  } helper;
 
   //! Substitution term.
   /**
@@ -96,6 +100,7 @@ typedef struct term *Term;
 void termsInit (void);
 void termsDone (void);
 Term makeTermEncrypt (Term t1, Term t2);
+Term makeTermFcall (Term t1, Term t2);
 Term makeTermTuple (Term t1, Term t2);
 Term makeTermType (const int type, const Symbol symb, const int runid);
 __inline__ Term deVarScan (Term t);
diff --git a/src/termlist.c b/src/termlist.c
index 7366eb1..7d25fdc 100644
--- a/src/termlist.c
+++ b/src/termlist.c
@@ -24,6 +24,7 @@
 #include "debug.h"
 #include "error.h"
 #include "switches.h"
+#include "knowledge.h"
 
 /*
  * Shared stuff
@@ -618,68 +619,6 @@ termlistLength (Termlist tl)
   return i;
 }
 
-//! Give the inverse key term of a term.
-/**
- * Gives a duplicate of the inverse Key of some term (which is used to encrypt something), as is defined
- * by the termlist, which is a list of key1,key1inv, key2, key2inv, etc...
- *@param inverses The list of inverses, typically from the knowledge.
- *@param key Any term of which the inverse will be determined.
- *@return A pointer to a duplicate of the inverse key term. Use termDelete to remove it.
- *\sa termDuplicate(), knowledge::inverses
- */
-
-Term
-inverseKey (Termlist inverses, Term key)
-{
-  key = deVar (key);
-
-  /* is this a function application? i.e. hash? */
-  if (isTermLeaf (key) && inTermlist (key->stype, TERM_Function))
-    {
-      /* functions cannot be inverted by default */
-      return termDuplicate (TERM_Hidden);
-    }
-  /* check for the special case first: when it is effectively a function application  */
-  if (isTermEncrypt (key) && isTermLeaf (TermKey (key))
-      && inTermlist (deVar (TermKey (key))->stype, TERM_Function))
-    {
-      /* we are scanning for functions */
-      /* scan the list */
-      /* key is function application kk(op), or {op}kk */
-      Term funKey (Term orig, Term newk)
-      {
-	/* in: {op}kk, nk
-	 * out: {op'}nk */
-	return makeTermEncrypt (termDuplicate (TermOp (orig)),
-				termDuplicate (newk));
-      }
-      while (inverses != NULL && inverses->next != NULL)
-	{
-
-	  if (isTermEqual (TermKey (key), inverses->term))
-	    return funKey (key, inverses->next->term);
-	  if (isTermEqual (TermKey (key), inverses->next->term))
-	    return funKey (key, inverses->term);
-	  inverses = inverses->next->next;
-	}
-    }
-  else
-    {
-      /* scanning for a direct inverse */
-
-      /* scan the list */
-      while (inverses != NULL && inverses->next != NULL)
-	{
-	  if (isTermEqual (key, inverses->term))
-	    return termDuplicate (inverses->next->term);
-	  if (isTermEqual (key, inverses->next->term))
-	    return termDuplicate (inverses->term);
-	  inverses = inverses->next->next;
-	}
-    }
-  return termDuplicate (key);	/* defaults to symmetrical */
-}
-
 //! Create a term local to a run.
 /*
  * We assume that at this point, no variables have been instantiated yet that occur in this term.
diff --git a/src/termlist.h b/src/termlist.h
index 475e3c9..81189f7 100644
--- a/src/termlist.h
+++ b/src/termlist.h
@@ -66,7 +66,6 @@ Termlist termlistAddBasic (Termlist tl, Term t);
 Termlist termlistAddBasics (Termlist tl, Termlist scan);
 Termlist termlistMinusTerm (Termlist tl, Term t);
 int termlistLength (Termlist tl);
-Term inverseKey (Termlist inverses, Term key);
 Term termLocal (const Term t, Termlist fromlist, Termlist tolist);
 Termlist termlistLocal (Termlist tl, const Termlist fromlist,
 			const Termlist tolist);
diff --git a/src/xmlout.c b/src/xmlout.c
index 83ab337..5e541f0 100644
--- a/src/xmlout.c
+++ b/src/xmlout.c
@@ -438,7 +438,7 @@ xmlInverses (const System sys)
 
   xmlPrint ("<inversekeys>");
   xmlindent++;
-  invlist = sys->know->inverses;
+  invlist = sys->know->inversekeys;
   while (invlist != NULL && invlist->next != NULL)
     {
       xmlPrint ("<keypair>");
@@ -452,6 +452,23 @@ xmlInverses (const System sys)
     }
   xmlindent--;
   xmlPrint ("</inversekeys>");
+
+  xmlPrint ("<inversekeyfunctions>");
+  xmlindent++;
+  invlist = sys->know->inversekeyfunctions;
+  while (invlist != NULL && invlist->next != NULL)
+    {
+      xmlPrint ("<keypair>");
+      xmlindent++;
+      xmlOutTerm (NULL, invlist->term);
+      xmlOutTerm (NULL, invlist->next->term);
+      xmlindent--;
+      xmlPrint ("</keypair>");
+
+      invlist = invlist->next->next;
+    }
+  xmlindent--;
+  xmlPrint ("</inversekeyfunctions>");
 }
 
 //! Show initial knowledge