Improved handling of cases with untyped variables.

When untyped variables occur, the encryption level depth pruning is for
now unjustified. Maybe we can get a proof later.  Previously this was
hidden, which was a bad design decision.  Now the output is much
clearer.

src/claim.h

@@ -17,6 +17,13 @@
  * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
  */
 
+/**
+ * ===============================================
+ * NOTE:
+ * The claim object structure is defined in role.h
+ * ===============================================
+ */
+
 #ifndef CLAIMS
 #define CLAIMS
 

src/compiler.c

@@ -1278,6 +1278,9 @@ tacTermlist (Tac tc)
 }
 
 //! Compute variables for a roles (for Arachne)
+/**
+ * This also takes care of setting the hasUntypedVariable flag, if needed.
+ */
 void
 compute_role_variables (const System sys, Protocol p, Role r)
 {
@@ -1298,13 +1301,25 @@ compute_role_variables (const System sys, Protocol p, Role r)
       roledef_iterate_events (r->roledef, process_event);
       r->variables = tl;
 
+      /*
+       * Iterate over variables for type checks
+       */
+      for (tl = r->variables; tl != NULL; tl = tl->next)
+	{
+	  if (isOpenVariable (tl->term))
+	    {
+	      sys->hasUntypedVariable = true;
+	      break;
+	    }
+	}
+
 #ifdef DEBUG
       if (DEBUGL (5))
 	{
 	  eprintf ("All variables for role ");
 	  termPrint (r->nameterm);
 	  eprintf (" are ");
-	  termlistPrint (tl);
+	  termlistPrint (r->variables);
 	  eprintf ("\n");
 	}
 #endif
@@ -1845,6 +1860,10 @@ compute_prec_sets (const System sys)
 }
 
 //! Check unused variables
+/**
+ * Some of this code is duplicated in the code that computes the role variables, so
+ * that should be cleaned up some day. TODO.
+ */
 void
 checkRoleVariables (const System sys, const Protocol p, const Role r)
 {

src/prune_theorems.c

@@ -425,15 +425,15 @@ prune_theorems (const System sys)
 
       // To be on the safe side, we currently limit the encryption level. 
       /**
-       * This is not a problem for known attacks, but should be addressed more
+       * This is valid *only* if there are no ticket-type variables.
-       * carefully at some point.  If there are variables that can contain
-       * encryptions, this is maybe not correct: make proof!
-       *
-       * @todo Fix untyped variables reasoning
        */
       if (term_encryption_level (b->term) > max_encryption_level)
 	{
 	  // Prune: we do not need to construct such terms
+	  if (sys->hasUntypedVariable)
+	    {
+	      sys->current_claim->complete = false;
+	    }
 	  if (switches.output == PROOF)
 	    {
 	      indentPrint ();

src/system.c

@@ -89,6 +89,7 @@ systemInit ()
   sys->bindings = NULL;
   sys->current_claim = NULL;
   sys->trustedRoles = NULL;
+  sys->hasUntypedVariable = false;
 
   /* reset global counters */
   systemReset (sys);

src/system.h

@@ -141,6 +141,7 @@ struct system
   Claimlist claimlist;		//!< List of claims in the system, with occurrence counts
   List labellist;		//!< List of labelinfo stuff
   int knowledgedefined;		//!< True if knowledge is defined for some role (which triggers well-formedness check etc.)
+  int hasUntypedVariable;	//!< True if there is a variable in the role specification that can contain constructors
 
   /* constructed trace pointers, static */
   Roledef *traceEvent;		//!< Trace roledefs: MaxRuns * maxRoledef