scyther/src/arachne.c

/*
 * Scyther : An automatic verifier for security protocols.
 * Copyright (C) 2007-2013 Cas Cremers
 * 
 * This program is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
 */

/**
 *
 *@file arachne.c
 *
 * Introduces a method for proofs akin to the Athena modelchecker
 * http://www.ece.cmu.edu/~dawnsong/athena/
 *
 */

#include <stdlib.h>
#include <limits.h>
#include <float.h>
#include <string.h>

#include "mymalloc.h"
#include "term.h"
#include "termlist.h"
#include "role.h"
#include "system.h"
#include "knowledge.h"
#include "compiler.h"
#include "states.h"
#include "mgu.h"
#include "arachne.h"
#include "error.h"
#include "claim.h"
#include "debug.h"
#include "binding.h"
#include "warshall.h"
#include "timer.h"
#include "type.h"
#include "switches.h"
#include "specialterm.h"
#include "cost.h"
#include "dotout.h"
#include "prune_bounds.h"
#include "prune_theorems.h"
#include "arachne.h"
#include "hidelevel.h"
#include "depend.h"
#include "xmlout.h"
#include "heuristic.h"
#include "tempfile.h"

extern int *graph;
extern int nodes;
extern int graph_uordblks;

static System sys;		//!< local buffer for the system pointer

int attack_length;		//!< length of the attack
int attack_leastcost;		//!< cost of the best attack sofar \sa cost.c

Protocol INTRUDER;		//!< intruder protocol
Role I_M;			//!< Initial knowledge role of the intruder
Role I_RRS;			//!< Encrypt role of the intruder
Role I_RRSD;			//!< Decrypt role of the intruder

int proofDepth;			//!< Current depth of the proof
int max_encryption_level;	//!< Maximum encryption level of any term

static int indentDepth;
static int prevIndentDepth;
static int indentDepthChanges;
static FILE *attack_stream;

/*
 * Forward declarations
 */

int iterate ();

/*
 * Program code
 */

//! Init Arachne engine
void
arachneInit (const System mysys)
{
  Roledef rd;

  void add_event (int event, Term message)
  {
    rd = roledefAdd (rd, event, NULL, NULL, NULL, message, NULL);
  }

  Role add_role (const char *rolenamestring)
  {
    Role r;
    Term rolename;

    rolename = makeGlobalConstant (rolenamestring);
    r = roleCreate (rolename);
    r->roledef = rd;
    rd = NULL;
    r->next = INTRUDER->roles;
    INTRUDER->roles = r;
    // compute_role_variables (sys, INTRUDER, r);
    return r;
  }

  sys = mysys;			// make sys available for this module as a global

  /**
   * Very important: turn role terms that are local to a run, into variables.
   */
  term_rolelocals_are_variables ();

  /*
   * Add intruder protocol roles
   */

  INTRUDER = protocolCreate (makeGlobalConstant (" INTRUDER "));

  // Initially empty roledef
  rd = NULL;

  add_event (SEND, NULL);
  I_M = add_role ("I_M: Atomic message");

  add_event (RECV, NULL);
  add_event (RECV, NULL);
  add_event (SEND, NULL);
  I_RRS = add_role ("I_E: Encrypt");

  add_event (RECV, NULL);
  add_event (RECV, NULL);
  add_event (SEND, NULL);
  I_RRSD = add_role ("I_D: Decrypt");

  sys->num_regular_runs = 0;
  sys->num_intruder_runs = 0;
  max_encryption_level = 0;

  indentDepth = 0;
  prevIndentDepth = 0;
  indentDepthChanges = 0;

  return;
}

//! Close Arachne engine
void
arachneDone ()
{
  return;
}

//------------------------------------------------------------------------
// Detail
//------------------------------------------------------------------------

//! Just a defined integer for invalid
#define INVALID		-1
//! can this roledef constitute a recv Goal?
#define isGoal(rd)	(rd->type == RECV && !rd->internal)
//! is this roledef already bound?
#define isBound(rd)	(rd->bound)

//! Indent prefix print
void
indentPrefixPrint (const int annotate, const int jumps)
{
  void counterPrint ()
  {
    statesFormat (sys->current_claim->states);
    eprintf ("\t");
    eprintf ("%i", annotate);
    eprintf ("\t");
  }

  if (switches.output == ATTACK && globalError == 0)
    {
      // Arachne, attack, not an error
      // We assume that means DOT output
      eprintf ("// ");
      counterPrint ();
    }
  else
    {
      // If it is not to stdout, or it is not an attack...
      int i;

      counterPrint ();
      for (i = 0; i < jumps; i++)
	{
	  if (i % 3 == 0)
	    eprintf ("|");
	  else
	    eprintf (" ");
	  eprintf (" ");
	}
    }
}

//! Indent print
/**
 * More subtle than before. Indentlevel changes now cause a counter to be increased, which is printed. Nice to find stuff in attacks.
 */
void
indentPrint ()
{
  if (indentDepth != prevIndentDepth)
    {
      indentDepthChanges++;
      while (indentDepth != prevIndentDepth)
	{
	  if (prevIndentDepth < indentDepth)
	    {
	      indentPrefixPrint (indentDepthChanges, prevIndentDepth);
	      eprintf ("{\n");
	      prevIndentDepth++;
	    }
	  else
	    {
	      prevIndentDepth--;
	      indentPrefixPrint (indentDepthChanges, prevIndentDepth);
	      eprintf ("}\n");
	    }
	}
    }
  indentPrefixPrint (indentDepthChanges, indentDepth);
}

//! Print indented binding
void
binding_indent_print (const Binding b, const int flag)
{
  indentPrint ();
  if (flag)
    eprintf ("!! ");
  binding_print (b);
  eprintf ("\n");
}

//! Keylevel tester: can this term ever be sent at this keylevel?
int
isKeylevelRight (Term t, const int kl)
{
  t = deVar (t);
  if (realTermLeaf (t))
    {
      // Leaf
      if (isTermVariable (t))
	{
	  // Variables are okay
	  return 1;
	}
      else
	{
	  // Constant, does it have a keylevel?
	  int mykl;

	  mykl = TermSymb (t)->keylevel;
	  if (mykl < INT_MAX)
	    {
	      // Sensible keylevel, so it must be possible
	      return (mykl <= kl);
	    }
	  else
	    {
	      // Never sent?
	      // So we can not expect it to come from that
	      return 0;
	    }
	}
    }
  else
    {
      // Node
      if (realTermTuple (t))
	{
	  // Tuple
	  return isKeylevelRight (TermOp1 (t), kl)
	    && isKeylevelRight (TermOp2 (t), kl);
	}
      else
	{
	  // Crypt
	  return isKeylevelRight (TermOp1 (t), kl)
	    && isKeylevelRight (TermOp2 (t), kl + 1);
	}
    }
}

//! Keylevel tester: can this term ever be sent at this keylevel?
/**
 * Depends on the keylevel lemma (so this will not be called when those lemmas
 * are disabled) and the keylevel constructors in symbol.c The idea is that
 * certain terms will never be sent.
 */
int
isPossiblySent (Term t)
{
  return isKeylevelRight (t, 0);
}

//! Wrapper for roleInstance
/**
 *@return Returns the run number
 */
int
semiRunCreate (const Protocol p, const Role r)
{
  int run;

  if (p == INTRUDER)
    sys->num_intruder_runs++;
  else
    sys->num_regular_runs++;
#ifdef DEBUG
  if (DEBUGL (5))
    {
      globalError++;
      eprintf ("Adding a run %i with semiRunCreate, ", sys->maxruns);
      termPrint (p->nameterm);
      eprintf (", ");
      termPrint (r->nameterm);
      eprintf ("\n");
      globalError--;
    }
#endif
  roleInstance (sys, p, r, NULL, NULL);
  run = sys->maxruns - 1;
  sys->runs[run].height = 0;
  return run;
}

//! Wrapper for roleDestroy
void
semiRunDestroy ()
{
  if (sys->maxruns > 0)
    {
      Protocol p;

      p = sys->runs[sys->maxruns - 1].protocol;
      roleInstanceDestroy (sys);
      if (p == INTRUDER)
	sys->num_intruder_runs--;
      else
	sys->num_regular_runs--;
    }
}

//! Fix the keylevels of any agents
/**
 * We simply extract the agent names from m0 (ugly hack)
 */
void
fixAgentKeylevels (void)
{
  Termlist tl, m0tl;

  m0tl = knowledgeSet (sys->know);
  tl = m0tl;
  while (tl != NULL)
    {
      Term t;

      t = deVar (tl->term);
      if (realTermLeaf (t))
	{
	  {
	    // a real agent type thing
	    if (TermSymb (t)->keylevel == INT_MAX)
	      {
		// Fix the keylevel
		TermSymb (t)->keylevel = 0;
	      }
	  }
	}
      tl = tl->next;
    }
  termlistDelete (m0tl);
}


//! After a role instance, or an extension of a run, we might need to add some goals
/**
 * From old to new. Sets the new height to new.
 *@returns The number of goals added (for destructions)
 */
int
add_recv_goals (const int run, const int old, const int new)
{
  if (new <= sys->runs[run].height)
    {
      return 0;
    }
  else
    {
      int count;
      int i;
      Roledef rd;

      sys->runs[run].height = new;
      i = old;
      rd = eventRoledef (sys, run, i);
      count = 0;
      while (i < new && rd != NULL)
	{
	  if (rd->type == RECV)
	    {
	      if (switches.output == PROOF)
		{
		  if (count == 0)
		    {
		      indentPrint ();
		      eprintf ("Thus, we must also produce ");
		    }
		  else
		    {
		      eprintf (", ");
		    }
		  termPrint (rd->message);
		}
	      count = count + goal_add (rd->message, run, i, 0);
	    }
	  rd = rd->next;
	  i++;
	}
      if ((count > 0) && switches.output == PROOF)
	{
	  eprintf ("\n");
	}
      return count;
    }
}

//! Determine trace length
int
get_semitrace_length ()
{
  int run;
  int length;

  run = 0;
  length = 0;
  while (run < sys->maxruns)
    {
      if (sys->runs[run].protocol != INTRUDER)
	{
	  // Non-intruder run: count length
	  // Subtract 'firstReal' to ignore chooses.
	  length = length + sys->runs[run].height - sys->runs[run].firstReal;
	}
      run++;
    }
  return length;
}

//! Count intruder events
int
countIntruderActions ()
{
  int count;
  int run;

  count = 0;
  run = 0;
  while (run < sys->maxruns)
    {
      if (sys->runs[run].protocol == INTRUDER)
	{
	  // Only intruder roles
	  if (sys->runs[run].role != I_M)
	    {
	      // The M_0 (initial knowledge) events don't count.
	      count++;
	    }
	}
      run++;
    }
  return count;
}

//------------------------------------------------------------------------
// Proof reporting
//------------------------------------------------------------------------

//! Protocol/role name of a run
void
role_name_print (const int run)
{
  eprintf ("protocol ");
  termPrint (sys->runs[run].protocol->nameterm);
  eprintf (", role ");
  termPrint (sys->runs[run].role->nameterm);
}

//! Adding a run/extending a run
void
proof_suppose_run (const int run, const int oldlength, const int newlength)
{
  if (switches.output == PROOF)
    {
      int reallength;

      indentPrint ();
      eprintf ("Suppose ");
      if (oldlength == 0)
	eprintf ("there is a ");
      else
	eprintf ("we extend ");
      reallength = roledef_length (sys->runs[run].start);
      if (reallength > newlength)
	eprintf ("semi-");
      eprintf ("run #%i of ", run);
      role_name_print (run);
      if (reallength > newlength)
	{
	  if (oldlength == 0)
	    eprintf (" of");
	  else
	    eprintf (" to");
	  eprintf (" length %i", newlength);
	}
      eprintf ("\n");
    }
}

//! Select a goal
void
proof_select_goal (Binding b)
{
  if (switches.output == PROOF)
    {
      Roledef rd;

      rd = roledef_shift (sys->runs[b->run_to].start, b->ev_to);
      indentPrint ();
      eprintf ("Selected goal: Where does term ");
      termPrint (b->term);
      eprintf (" occur first as an interm?\n");
      indentPrint ();
      eprintf ("* It is required for ");
      roledefPrint (rd);
      eprintf (" at index %i in run %i\n", b->ev_to, b->run_to);
    }
}

//! Cannot bind because of cycle
void
proof_cannot_bind (const Binding b, const int run, const int index)
{
  if (switches.output == PROOF)
    {
      indentPrint ();
      eprintf
	("Cannot bind this to run %i, index %i because that introduces a cycle.\n",
	 run, index);
    }
}

//! Test a binding
void
proof_suppose_binding (Binding b)
{
  if (switches.output == PROOF)
    {
      Roledef rd;

      indentPrint ();
      rd = roledef_shift (sys->runs[b->run_from].start, b->ev_from);
      eprintf ("Suppose it originates in run %i, at index %i\n", b->run_from,
	       b->ev_from);
      indentPrint ();
      eprintf ("* I.e. event ");
      roledefPrint (rd);
      eprintf ("\n");
      indentPrint ();
      eprintf ("* from ");
      role_name_print (b->run_from);
      eprintf ("\n");
    }
}

//------------------------------------------------------------------------
// Sub
//------------------------------------------------------------------------

//! Iterate over all events in the roles (including the intruder ones)
/**
 * Function is called with (protocol pointer, role pointer, roledef pointer, index)
 * and returns an integer. If it is false, iteration aborts.
 */
int
iterate_role_events (int (*func) ())
{
  Protocol p;

  p = sys->protocols;
  while (p != NULL)
    {
      Role r;

      r = p->roles;
      while (r != NULL)
	{
	  Roledef rd;
	  int index;

	  rd = r->roledef;
	  index = 0;
	  while (rd != NULL)
	    {
	      if (!func (p, r, rd, index))
		return 0;
	      index++;
	      rd = rd->next;
	    }
	  r = r->next;
	}
      p = p->next;
    }
  return 1;
}

//! Iterate over all send types in the roles (including the intruder ones)
/**
 * Function is called with (protocol pointer, role pointer, roledef pointer, index)
 * and returns an integer. If it is false, iteration aborts.
 */
int
iterate_role_sends (int (*func) ())
{
  Protocol p;

  p = sys->protocols;
  while (p != NULL)
    {
      Role r;

      r = p->roles;
      while (r != NULL)
	{
	  Roledef rd;
	  int index;

	  rd = r->roledef;
	  index = 0;
	  while (rd != NULL)
	    {
	      if (rd->type == SEND)
		{
		  if (!func (p, r, rd, index))
		    return 0;
		}
	      index++;
	      rd = rd->next;
	    }
	  r = r->next;
	}
      p = p->next;
    }
  return 1;
}


//! Create decryption role instance
/**
 * Note that this does not add any bindings for the receives.
 *
 *@param term	The term to be decrypted (implies decryption key)
 *@param key	The key that is needed to decrypt the term
 *
 *@returns The run id of the decryptor instance
 */
int
create_decryptor (const Term term, const Term key)
{
  if (term != NULL && isTermEncrypt (term))
    {
      Roledef rd;
      int run;

#ifdef DEBUG
      if (DEBUGL (5))
	{
	  globalError++;
	  eprintf ("Creating decryptor for term ");
	  termPrint (term);
	  eprintf (" and key ");
	  termPrint (key);
	  eprintf ("\n");
	  globalError--;
	}
#endif

      run = semiRunCreate (INTRUDER, I_RRSD);
      rd = sys->runs[run].start;
      rd->message = termDuplicateUV (term);
      rd->next->message = termDuplicateUV (key);
      rd->next->next->message = termDuplicateUV (TermOp (term));
      sys->runs[run].height = 3;
      proof_suppose_run (run, 0, 3);

      return run;
    }

  globalError++;
  eprintf ("Term for which a decryptor instance is requested: ");
  termPrint (term);
  eprintf ("\n");
  error ("Trying to build a decryptor instance for a non-encrypted term.");
  return -1;
}

//! Get the priority level of a key that is needed for a term (typical pk/sk distinction)
int
getPriorityOfNeededKey (const System sys, const Term keyneeded)
{
  int prioritylevel;

  /* Normally, a key gets higher priority, but unfortunately this is not propagated at the moment. Maybe later.
   */
  prioritylevel = 1;
  if (realTermEncrypt (keyneeded))
    {
      /* the key is a construction itself */
      if (inKnowledge (sys->know, TermKey (keyneeded)))
	{
	  /* the key is constructed by a public thing */
	  /* typically, this is a public key, so we postpone it  */
	  prioritylevel = -1;
	}
    }
  return prioritylevel;
}

//! Report failed binding
void
report_failed_binding (Binding b, int run, int index)
{
  if (switches.output == PROOF)
    {
      indentPrint ();
      eprintf ("Failed to bind the binding at r%ii%i with term ", b->run_to,
	       b->ev_to);
      termPrint (b->term);
      eprintf (" to the source r%ii%i because of orderings.\n", run, index);
#ifdef DEBUG
      if (DEBUGL (5))
	{
	  dependPrint ();
	}
#endif
    }
}

//! Make a decryption chain from a binding to some run,index using the key list, and callback if this works.
/**
 * The key goals are bound to the goal, and then we iterate on that.
 *
 *@param b	binding to fix (bind), destination filled in
 *@param run	run of binding start
 *@param index	index in run of binding start
 * Callback return value is int, but is effectively ignored.
 */
void
createDecryptionChain (const Binding b, const int run, const int index,
		       Termlist keylist, int (*callback) (void))
{
  if (keylist == NULL)
    {
      // Immediate binding, no key needed.
      if (goal_bind (b, run, index))
	{
	  callback ();
	  goal_unbind (b);
	  return;
	}
      else
	{
	  report_failed_binding (b, run, index);
	}
    }
  else
    {
      Term tdecr, tkey;
      int smallrun;

      // Some decryptor is needed for the term in the list

      indentDepth++;

      tdecr = keylist->term;
      tkey = inverseKey (sys->know, TermKey (tdecr));
      smallrun = create_decryptor (tdecr, tkey);
      {
	Roledef rddecrypt;
	Binding bnew;
	int newgoals;
	int prioritylevel;

	/*
	 * 2. Add goal bindings
	 */

	rddecrypt = sys->runs[smallrun].start;
	// Add goal for tdecr copy
	newgoals = goal_add (rddecrypt->message, smallrun, 0, 0);
	if (newgoals != 1)
	  {
	    error
	      ("Added %i goals (instead of one) for decryptor goal 1, weird.",
	       newgoals);
	  }

	// This is the unique new goal 
	bnew = (Binding) sys->bindings->data;

	// Add goal for needed key copy
	prioritylevel = getPriorityOfNeededKey (sys, tkey);
	newgoals += goal_add (rddecrypt->next->message, smallrun, 1,
			      prioritylevel);

	if (switches.output == PROOF)
	  {
	    indentPrint ();
	    eprintf
	      ("This introduces the obligation to decrypt the following subterm: ");
	    termPrint (tdecr);
	    eprintf (" to be decrypted using ");
	    termPrint (tkey);
	    eprintf ("\n");

	    indentPrint ();
	    eprintf
	      ("To this end, we added two new goals and one new send: ");
	    termPrint (rddecrypt->message);
	    eprintf (",");
	    termPrint (rddecrypt->next->message);
	    eprintf (",");
	    termPrint (rddecrypt->next->next->message);
	    eprintf ("\n");
	  }

	/*
	 * 3. Bind open goal to decryptor? 
	 */
	if (goal_bind (b, smallrun, 2))
	  {
	    if (switches.output == PROOF)
	      {
		indentPrint ();
		eprintf ("Bound ");
		termPrint (b->term);
		eprintf (" to r%ii%i: trying new createDecryptionChain.\n",
			 smallrun, 2);
	      }

	    // Iterate with the new goal
	    createDecryptionChain (bnew, run, index, keylist->next, callback);
	    goal_unbind (b);
	  }
	else
	  {
	    report_failed_binding (b, smallrun, 2);
	  }
	/*
	 * clean up
	 */
	goal_remove_last (newgoals);
      }
      semiRunDestroy ();
      termDelete (tkey);

      indentDepth--;
    }
}


//! Try to bind a specific existing run to a goal.
/**
 * The idea is that we try to bind it this specific run and index. If this
 * requires keys, then we should add such goals as well with the required
 * decryptor things.
 *
 * The 'newdecr' boolean signals the addition of decryptors. If it is false, we should not add any.
 *
 * The key goals are bound to the goal. Iterates on success.
 */
void
bind_existing_to_goal (const Binding b, const int run, const int index,
		       int newdecr)
{
  Term bigterm;

  int unifiesWithKeys (Termlist substlist, Termlist keylist)
  {
    int old_length;
    int newgoals;

    // TODO this is a hack: in this case we really should not use subterm
    // unification but interm instead. However, this effectively does the same
    // by avoiding branches that get immediately pruned anyway.
    if (!newdecr && keylist != NULL)
      {
	return true;
      }
    // We need some adapting because the height would increase; we therefore
    // have to add recv goals before we know whether it unifies.
    old_length = sys->runs[run].height;
    newgoals = add_recv_goals (run, old_length, index + 1);

    {
      // wrap substitution lists

      void wrapSubst (Termlist sl)
      {
	if (sl == NULL)
	  {
	    if (switches.output == PROOF)
	      {
		Roledef rd;

		indentPrint ();
		eprintf ("Suppose ");
		termPrint (b->term);
		eprintf (" originates first at run %i, event %i, as part of ",
			 run, index);
		rd = roledef_shift (sys->runs[run].start, index);
		termPrint (rd->message);
		eprintf ("\n");
	      }
	    // new create key goals, bind etc.
	    createDecryptionChain (b, run, index, keylist, iterate);
	  }
	else
	  {
	    int neworders;
	    int allgood;
	    Term tvar;

	    // the idea is, that a substitution in run x with
	    // something containing should be wrapped; this
	    // occurs for all subterms of other runs.
	    int makeDepend (Term tsmall)
	    {
	      Term tsubst;

	      tsubst = deVar (tsmall);
	      if (!realTermVariable (tsubst))
		{
		  // Only for non-variables (i.e. local constants)
		  int r1, e1;

		  r1 = TermRunid (tsubst);
		  e1 = firstOccurrence (sys, r1, tsubst, SEND);
		  if (e1 >= 0)
		    {
		      int r2, e2;

		      r2 = TermRunid (tvar);
		      e2 = firstOccurrence (sys, r2, tsubst, RECV);
		      if (e2 >= 0)
			{

			  if (dependPushEvent (r1, e1, r2, e2))
			    {
			      neworders++;
			      return true;
			    }
			  else
			    {
			      allgood = false;
			      if (switches.output == PROOF)
				{
				  indentPrint ();
				  eprintf ("Substitution for ");
				  termSubstPrint (sl->term);
				  eprintf (" (subterm ");
				  termPrint (tsmall);
				  eprintf (") could not be safely bound.\n");
				}
			      return false;
			    }
			}
		    }
		}
	      return true;
	    }

	    neworders = 0;
	    allgood = true;
	    tvar = sl->term;
	    iterateTermOther (run, tvar, makeDepend);
	    if (allgood)
	      {
		wrapSubst (sl->next);
	      }
	    while (neworders > 0)
	      {
		neworders--;
		dependPopEvent ();
	      }
	  }
      }

      wrapSubst (substlist);
    }

    // undo
    goal_remove_last (newgoals);
    sys->runs[run].height = old_length;
    return true;
  }

  bigterm = roledef_shift (sys->runs[run].start, index)->message;
  subtermUnify (bigterm, b->term, NULL, NULL, unifiesWithKeys);
}




//! Bind a goal to an existing regular run, if possible, by adding decr events
int
bind_existing_run (const Binding b, const Protocol p, const Role r,
		   const int index)
{
  int run, flag;
  int found;

  flag = 1;
  found = 0;
  for (run = 0; run < sys->maxruns; run++)
    {
      if (sys->runs[run].protocol == p && sys->runs[run].role == r)
	{
	  found++;
	  if (switches.output == PROOF)
	    {
	      if (found == 1)
		{
		  indentPrint ();
		  eprintf ("Can we bind it to an existing regular run of ");
		  termPrint (p->nameterm);
		  eprintf (", ");
		  termPrint (r->nameterm);
		  eprintf ("?\n");
		}
	      indentPrint ();
	      eprintf ("%i. Can we bind it to run %i?\n", found, run);
	    }
	  indentDepth++;
	  bind_existing_to_goal (b, run, index, true);
	  indentDepth--;
	}
    }
  if (switches.output == PROOF && found == 0)
    {
      indentPrint ();
      eprintf ("There is no existing run for ");
      termPrint (p->nameterm);
      eprintf (", ");
      termPrint (r->nameterm);
      eprintf ("\n");
    }
  return flag;
}

//! Bind a goal to a new run, possibly adding decr events
int
bind_new_run (const Binding b, const Protocol p, const Role r,
	      const int index)
{
  int run;

  run = semiRunCreate (p, r);
  proof_suppose_run (run, 0, index + 1);
  {
    int newgoals;

    newgoals = add_recv_goals (run, 0, index + 1);
    indentDepth++;
    bind_existing_to_goal (b, run, index, true);
    indentDepth--;
    goal_remove_last (newgoals);
  }
  semiRunDestroy ();
  return true;
}

//! Proof markers
void
proof_go_down (const Term label, const Term t)
{
  Termlist l;
  int depth;
  int len;

  if (switches.output != PROOF)
    return;
  // Prepend the terms (the list is in reverse)
  TERMLISTPREPEND (sys->proofstate, label);
  TERMLISTPREPEND (sys->proofstate, t);
  len = termlistLength (sys->proofstate) / 2;
  // Display state
  eprintf ("Proof state: branch at level %i\n", len);
  l = termlistForward (sys->proofstate);
  depth = 0;
  while (l != NULL)
    {
      int i;
      eprintf ("Proof state: ");

      for (i = 0; i < depth; i++)
	{
	  eprintf ("  ");
	}
      termPrint (l->prev->term);
      eprintf ("(");
      termPrint (l->term);
      eprintf ("); ");
      l = l->prev->prev;
      eprintf ("\n");
      depth++;
    }
}

void
proof_go_up (void)
{
  if (switches.output != PROOF)
    return;
  sys->proofstate = termlistDelTerm (sys->proofstate);
  sys->proofstate = termlistDelTerm (sys->proofstate);
  return;
}

//! Print the current semistate
void
printSemiState ()
{
  int run;
  int open;

  int binding_state_print (void *dt)
  {
    binding_indent_print ((Binding) dt, 1);
    return 1;
  }

  indentPrint ();
  eprintf ("!! --=[ Semistate ]=--\n");
  indentPrint ();
  eprintf ("!!\n");
  indentPrint ();
  eprintf ("!! Trace length: %i\n", get_semitrace_length ());
  open = 0;
  for (run = 0; run < sys->maxruns; run++)
    {
      int index;
      Role r;
      Roledef rd;
      Term oldagent;

      indentPrint ();
      eprintf ("!!\n");
      indentPrint ();
      eprintf ("!! [ Run %i, ", run);
      termPrint (sys->runs[run].protocol->nameterm);
      eprintf (", ");
      r = sys->runs[run].role;
      oldagent = r->nameterm->subst;
      r->nameterm->subst = NULL;
      termPrint (r->nameterm);
      r->nameterm->subst = oldagent;
      if (oldagent != NULL)
	{
	  eprintf (": ");
	  termPrint (oldagent);
	}
      eprintf (" ]\n");

      index = 0;
      rd = sys->runs[run].start;
      while (index < sys->runs[run].height)
	{
	  indentPrint ();
	  eprintf ("!! %i ", index);
	  roledefPrint (rd);
	  eprintf ("\n");
	  if (isGoal (rd) && !isBound (rd))
	    open++;
	  index++;
	  rd = rd->next;
	}
    }
  if (sys->bindings != NULL)
    {
      indentPrint ();
      eprintf ("!!\n");
      list_iterate (sys->bindings, binding_state_print);
    }
  indentPrint ();
  eprintf ("!!\n");
  indentPrint ();
  eprintf ("!! - open: %i -\n", open);
}

//! Check if a binding duplicates an old one: if so, simply connect
/**
 * If it returns true, it has bound the b_new binding, which we must unbind later.
 */
int
bind_old_goal (const Binding b_new)
{
  if (!b_new->done)
    {
      List bl;

      bl = sys->bindings;
      while (bl != NULL)
	{
	  Binding b_old;

	  b_old = (Binding) bl->data;
	  if (b_old->done && isTermEqual (b_new->term, b_old->term))
	    {
	      // Old is done and has the same term!
	      // So we try to copy this binding, and fix it.
	      if (goal_bind (b_new, b_old->run_from, b_old->ev_from))
		{
		  return true;
		}
	    }
	  bl = bl->next;
	}
    }
  // No old binding to connect to
  return false;
}

//! Bind an intruder goal by intruder composition construction
/**
 * Handles the case where the intruder constructs a composed term himself.
 */
int
bind_goal_new_encrypt (const Binding b)
{
  Term term;
  int flag;
  int can_be_encrypted;


  flag = 1;
  term = deVar (b->term);
  can_be_encrypted = 0;

  if (!realTermLeaf (term))
    {
      Term t1, t2;

      if (switches.intruder && (!realTermEncrypt (term)))
	{
	  // tuple construction
	  error ("Goal that is a tuple should not occur!");
	}

      // must be encryption
      t1 = TermOp (term);
      t2 = TermKey (term);

      if (t2 != TERM_Hidden)
	{
	  int run;

	  can_be_encrypted = 1;
	  run = semiRunCreate (INTRUDER, I_RRS);
	  {
	    int index;
	    Roledef rd;

	    rd = sys->runs[run].start;
	    rd->message = termDuplicateUV (t1);
	    rd->next->message = termDuplicateUV (t2);
	    rd->next->next->message = termDuplicateUV (term);
	    index = 2;
	    proof_suppose_run (run, 0, index + 1);
	    if (switches.output == PROOF)
	      {
		indentPrint ();
		eprintf ("* Encrypting ");
		termPrint (term);
		eprintf (" using term ");
		termPrint (t1);
		eprintf (" and key ");
		termPrint (t2);
		eprintf ("\n");
	      }

	    {
	      int newgoals;
	      newgoals = add_recv_goals (run, 0, index + 1);
	      {

		indentDepth++;
		if (goal_bind (b, run, index))
		  {
		    proof_suppose_binding (b);
		    flag = flag && iterate ();
		    goal_unbind (b);
		  }
		else
		  {
		    proof_cannot_bind (b, run, index);
		  }
		indentDepth--;
	      }
	      goal_remove_last (newgoals);
	    }
	  }
	  semiRunDestroy ();
	}
    }

  if (!can_be_encrypted)
    {
      if (switches.output == PROOF)
	{
	  indentPrint ();
	  eprintf ("Term ");
	  termPrint (b->term);
	  eprintf (" cannot be constructed by encryption.\n");
	}
    }

  return flag;
}

//! Bind an intruder goal by intruder construction
/**
 * Handles the case where the intruder constructs a composed term himself, or retrieves it from m0.
 * However, it must not already have been created in an intruder run; then it gets bound to that.
 */
int
bind_goal_new_intruder_run (const Binding b)
{
  int flag;

  if (switches.output == PROOF)
    {
      indentPrint ();
      eprintf ("Can we bind ");
      termPrint (b->term);
      eprintf (" from a new intruder run?\n");
    }
  indentDepth++;
  //flag = flag && bind_goal_new_encrypt (b);
  flag = bind_goal_new_encrypt (b);
  indentDepth--;
  return flag;
}

//! Dummy helper function for iterator; abort if sub-unification found
int
test_sub_unification (Termlist substlist, Termlist keylist)
{
  // A unification exists; return the signal
  return false;
}

//! Bind a regular goal
/**
 * Problem child. Valgrind does not like it.
 */
int
bind_goal_regular_run (const Binding b)
{
  int flag;
  int found;

  /*
   * This is a local function so we have access to goal
   */
  int bind_this_role_send (Protocol p, Role r, Roledef rd, int index)
  {
    if (p == INTRUDER)
      {
	// No intruder roles here
	return true;
      }

    // Test for interm unification
#ifdef DEBUG
    if (DEBUGL (5))
      {
	indentPrint ();
	eprintf ("Checking send candidate with message ");
	termPrint (rd->message);
	eprintf (" from ");
	termPrint (p->nameterm);
	eprintf (", ");
	termPrint (r->nameterm);
	eprintf (", index %i\n", index);
      }
#endif
    if (!subtermUnify
	(rd->message, b->term, NULL, NULL, test_sub_unification))
      {
	int sflag;

	// A good candidate
	found++;
	if (switches.output == PROOF && found == 1)
	  {
	    indentPrint ();
	    eprintf ("The term ", found);
	    termPrint (b->term);
	    eprintf
	      (" matches patterns from the role definitions. Investigate.\n");
	  }
	if (switches.output == PROOF)
	  {
	    indentPrint ();
	    eprintf ("%i. It matches the pattern ", found);
	    termPrint (rd->message);
	    eprintf (" from ");
	    termPrint (p->nameterm);
	    eprintf (", ");
	    termPrint (r->nameterm);
	    eprintf (", at %i\n", index);
	  }
	indentDepth++;

	// Bind to existing run
#ifdef DEBUG
	debug (5, "Trying to bind to existing run.");
#endif
	proof_go_down (TERM_DeEx, b->term);
	sflag = bind_existing_run (b, p, r, index);
	proof_go_up ();
	// bind to new run
#ifdef DEBUG
	debug (5, "Trying to bind to new run.");
#endif
	proof_go_down (TERM_DeNew, b->term);
	sflag = sflag && bind_new_run (b, p, r, index);
	proof_go_up ();

	indentDepth--;
	return sflag;
      }
    else
      {
	return true;
      }
  }


  // Bind to all possible sends of regular runs
  found = 0;
  flag = iterate_role_sends (bind_this_role_send);
  if (switches.output == PROOF && found == 0)
    {
      indentPrint ();
      eprintf ("The term ");
      termPrint (b->term);
      eprintf (" does not match any pattern from the role definitions.\n");
    }
  return flag;
}


//! Bind to all possible sends of intruder runs
int
bind_goal_old_intruder_run (Binding b)
{
  int run;
  int flag;
  int found;

  found = 0;
  flag = 1;
  for (run = 0; run < sys->maxruns; run++)
    {
      if (sys->runs[run].protocol == INTRUDER)
	{
	  int ev;
	  Roledef rd;

	  rd = sys->runs[run].start;
	  ev = 0;
	  while (ev < sys->runs[run].height)
	    {
	      if (rd->type == SEND)
		{
		  found++;
		  if (switches.output == PROOF && found == 1)
		    {
		      indentPrint ();
		      eprintf
			("Suppose it is from an existing intruder run.\n");
		    }
		  indentDepth++;
		  bind_existing_to_goal (b, run, ev,
					 (sys->runs[run].role != I_RRS));
		  indentDepth--;
		}
	      rd = rd->next;
	      ev++;
	    }
	}
    }
  if (switches.output == PROOF && found == 0)
    {
      indentPrint ();
      eprintf ("No existing intruder runs to match to.\n");
    }
  return flag;
}

//! Bind a goal in all possible ways
int
bind_goal_all_options (const Binding b)
{
  if (b->blocked)
    {
      error ("Trying to bind a blocked goal!");
    }
  if (!b->done)
    {
      int flag;

      flag = 1;
      proof_select_goal (b);
      indentDepth++;

      // Consider a duplicate goal that we already bound before (C-minimality)
      // if (1 == 0)
      if (bind_old_goal (b))
	{
	  if (switches.output == PROOF)
	    {
	      indentPrint ();
	      eprintf ("Goal for term ");
	      termPrint (b->term);
	      eprintf (" was bound once before, linking up to #%i, %i.\n",
		       b->run_from, b->ev_from);
	    }

	  flag = flag && iterate ();

	  // Unbind again
	  goal_unbind (b);
	  indentDepth--;
	  return flag;
	}
      else
	{
	  int know_only;

	  know_only = false;

	  if (1 == 0)		// blocked for now
	    {
	      // 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)
		{
		  if (!inKnowledge (sys->know, function))
		    {
		      // 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 = true;
		    }
		}
	    }

	  if (switches.experimental & 16)
	    {
	      // Keylevel lemmas: improves on the previous one
	      if (!isPossiblySent (b->term))
		{
		  if (switches.output == PROOF)
		    {
		      eprintf
			("Rejecting a term as a regular bind because key levels are off: ");
		      termPrint (b->term);
		      if (know_only)
			{
			  eprintf (" [in accordance with function lemma]");
			}
		      else
			{
			  eprintf (" [stronger than function lemma]");
			}
		      eprintf ("\n");
		    }
		  know_only = true;
		}
	    }

	  if (!(switches.experimental & 32))
	    {
		    /**
		     * Note: this is slightly weaker than the previous & 16,
		     * but it actually differs in such minimal cases that it
		     * might be better to simply have the (much cleaner)
		     * keylevel lemma.
		     *
		     * That's why this is default and the other isn't.
		     */

	      // Hidelevel variant
	      int hlf;

	      hlf = hidelevelFlag (sys, b->term);
	      if (hlf == HLFLAG_NONE || hlf == HLFLAG_KNOW)
		{
		  know_only = true;
		}
	    }


	  // Allright, proceed

	  proofDepth++;
	  if (know_only)
	    {
	      // Special case: only from intruder
	      proof_go_down (TERM_CoOld, b->term);
	      flag = flag && bind_goal_old_intruder_run (b);
	      //flag = flag && bind_goal_new_intruder_run (b);
	      proof_go_up ();
	    }
	  else
	    {
	      // Normal case
	      flag = bind_goal_regular_run (b);
	      proof_go_down (TERM_CoOld, b->term);
	      flag = flag && bind_goal_old_intruder_run (b);
	      proof_go_up ();
	      proof_go_down (TERM_CoNew, b->term);
	      flag = flag && bind_goal_new_intruder_run (b);
	      proof_go_up ();
	    }
	  proofDepth--;

	  indentDepth--;
	  return flag;
	}
    }
  else
    {
      return 1;
    }
}

//! Create a generic new term of the same type, with a new run identifier.
/**
 * Output: the first element of the returned list.
 */
Termlist
createNewTermGeneric (Termlist tl, Term t)
{
  int freenumber;
  Termlist tlscan;
  Term newterm;

  /* Determine first free number */
  freenumber = sys->maxruns;
  tlscan = tl;
  while (tlscan != NULL)
    {
      Term ts;

      ts = tlscan->term;
      if (isLeafNameEqual (t, ts))
	{
	  if (TermRunid (ts) >= freenumber)
	    {
	      freenumber = TermRunid (ts) + 1;
	    }
	}
      tlscan = tlscan->next;
    }

  /* Make a new term with the free number */
  newterm = (Term) malloc (sizeof (struct term));
  memcpy (newterm, t, sizeof (struct term));
  TermRunid (newterm) = freenumber;

  /* The type of the new term should be that of the parent! */
  newterm->stype = termlistAppend (NULL, t);

  /* return */
  return termlistPrepend (tl, newterm);
}

//! Construct a list of already used constants
Termlist
findUsedConstants (const System sys)
{
  int run;
  Termlist tl;
  Termlist tlconst;

  tl = NULL;
  tlconst = NULL;
  for (run = 0; run < sys->maxruns; run++)
    {
      tl = termlistAddBasics (tl, sys->runs[run].rho);
      tl = termlistAddBasics (tl, sys->runs[run].sigma);
    }
  while (tl != NULL)
    {
      Term t;

      t = tl->term;
      if (!realTermVariable (t))
	{
	  tlconst = termlistAddNew (tlconst, t);
	}
      tl = tl->next;
    }
  termlistDelete (tl);
  return tlconst;
}

//! Retrieve a list of agent name candidates
Termlist
getAgentCandidates (Termlist seen)
{
  Termlist knowlist;
  Termlist candidatelist;
  Termlist li;			// list loop pointer

  knowlist = knowledgeSet (sys->know);
  candidatelist = NULL;
  for (li = knowlist; li != NULL; li = li->next)
    {
      Term t;

      t = li->term;
      if (isAgentType (t->stype))
	{
	  /* agent */
	  /* We don'typeterm want to instantiate untrusted agents. */
	  if (!inTermlist (sys->untrusted, t))
	    {
	      /* trusted agent */
	      if (!inTermlist (seen, t))
		{
		  /* This agent name is not in the list yet, so could be chosen */
		  candidatelist = termlistPrepend (candidatelist, t);
		}
	    }
	}
    }
  termlistDelete (knowlist);
  return candidatelist;
}

//! Get to string of term
const char *
getTermString (Term t)
{
  if (t != NULL)
    {
      if (TermSymb (t) != NULL)
	{
	  return (TermSymb (t)->text);
	}
    }
  return NULL;
}

//! Check the first character of two terms
int
isFirstCharEqual (Term t1, Term t2)
{
  const char *c1, *c2;

  c1 = getTermString (t1);
  c2 = getTermString (t2);
  if ((c1 == NULL) || (c2 == NULL))
    {
      return false;
    }
  else
    {
      return (c1[0] == c2[0]);
    }
}

//! Choose the best term from the (non-null) candidate list for the variable var
Term
chooseBestCandidate (Termlist candidatelist, Term var)
{
  Term last;
  Termlist li;			// list loop pointer

  // See if we have a candidate that starts with the same first character
  for (li = candidatelist; li != NULL; li = li->next)
    {
      last = li->term;
      if (isFirstCharEqual (last, var))
	{
	  return last;
	}
    }
  // If not, we may still want to invoke heuristics (Alice initiates, Bob responds)
  if (li == NULL)
    {
      // li==null happens if we did not break out of the loop, i.e., found nothing
      const char *c;

      c = getTermString (var);
      if (c != NULL)
	{
	  // Check if name starts with common prefix, resort to common name if still a candidate
	  if (strchr ("Ii", *c) && inTermlist (candidatelist, AGENT_Alice))
	    {
	      return AGENT_Alice;
	    }
	  if (strchr ("Rr", *c) && inTermlist (candidatelist, AGENT_Bob))
	    {
	      return AGENT_Bob;
	    }
	}
    }
  return last;
}

//! Create a new term with incremented run rumber, starting at sys->maxruns.
/**
 * This is a rather intricate function that tries to generate new terms of a
 * certain type. It first looks up things in the initial knowledge, checking
 * whether they are used already. After that, new ones are generated.
 *
 * Input:
 * - seen is a termlist that contains newly generated terms (usage: seen = createNewTerm(seen,.. )
 * - typeterm is the type name term (e.g., "Agent" term, "Data" in case not clear.)
 * - isagent is a boolean that is true iff we are looking for an agent name from the initial knowledge for a role
 * - var is the variable term of which we use the name
 *
 * Output: the first element of the returned list, which is otherwise equal to seen.
 */
Termlist
createNewTerm (Termlist seen, Term typeterm, int isagent, Term nameterm)
{
  /* Does if have an explicit type?
   * If so, we try to find a fresh name from the intruder knowledge first.
   */
  if (isagent)
    {
      Termlist candidatelist;

      candidatelist = getAgentCandidates (seen);
      if (candidatelist != NULL)
	{
	  Term t;

	  t = chooseBestCandidate (candidatelist, nameterm);
	  termlistDelete (candidatelist);
	  return termlistPrepend (seen, t);
	}
    }

  /* Not an agent or no free one found */
  return createNewTermGeneric (seen, typeterm);
}

//! Delete a term made in the previous constructions
/**
 * \sa createNewTerm
 */
void
deleteNewTerm (Term t)
{
  if (TermRunid (t) >= 0)
    {
      /* if it has a positive runid, it did not come from the intruder
       * knowledge, so it must have been constructed.
       */
      free (t);
    }
}

//! Make a trace concrete
/**
 * People find reading variables in attack outputs difficult.
 * Thus, we instantiate open variables in a sensible way to make things more readable.
 *
 * This happens after sys->maxruns is fixed. Intruder constants thus are numbered from sys->maxruns onwards.
 *
 * \sa makeTraceClass
 */
Termlist
makeTraceConcrete (const System sys)
{
  Termlist changedvars;
  Termlist tlnew;
  int run;

  changedvars = NULL;
  tlnew = findUsedConstants (sys);

  for (run = 0; run < sys->maxruns; run++)
    {
      Termlist tl;

      for (tl = termlistForward (sys->runs[run].locals); tl != NULL;
	   tl = tl->prev)
	{
	  Term basevar;

	  basevar = tl->term;

	  /* variable, and of some run? */
	  if (isTermVariable (basevar) && TermRunid (basevar) >= 0)
	    {
	      Term var;
	      Term name;
	      Termlist vartype;

	      var = deVar (basevar);
	      vartype = basevar->stype;
	      // Determine class name
	      if (vartype != NULL)
		{
		  // Take first type name
		  name = vartype->term;
		}
	      else
		{
		  // Just a generic name
		  name = TERM_Data;
		}
	      // We should turn this into an actual term
	      tlnew =
		createNewTerm (tlnew, name, isAgentType (var->stype),
			       basevar);
	      var->subst = tlnew->term;

	      // Store for undo later
	      TERMLISTADD (changedvars, var);
	    }
	}
    }
  termlistDelete (tlnew);
  return changedvars;
}

//! Make a trace a class again
/**
 * \sa makeTraceConcrete
 */
void
makeTraceClass (const System sys, Termlist varlist)
{
  Termlist tl;

  tl = varlist;
  while (tl != NULL)
    {
      Term var;

      var = tl->term;
      if (realTermVariable (var))
	{
	  deleteNewTerm (var->subst);
	  var->subst = NULL;
	}
      tl = tl->next;
    }
  termlistDelete (varlist);
}

//! Determine whether to filter to a single attack
int
useAttackBuffer (void)
{
  if (switches.useAttackBuffer)
    {
      // it is possible
      if (switches.prune != 0)
	{
	  // it is also desired
	  return true;
	}
    }
  return false;
}

//! Start attack output
void
attackOutputStart (void)
{
  if (useAttackBuffer ())
    {
      FILE *fd;

      // Close old file (if any)
      if (attack_stream != NULL)
	{
	  fclose (attack_stream);	// this automatically discards the old temporary file
	}
      // Create new file
      fd = (FILE *) scyther_tempfile ();
      attack_stream = fd;
      globalStream = (char *) attack_stream;
    }
}

//! Stop attack output
void
attackOutputStop (void)
{
  // Nothing to do, just leave the opened tmpfile
}

//! Copy one (finite) stream from beginning to end to another
/**
 * Ugly first implementation, something to improve later (although it is not
 * crucial code in any way)
 */
void
fcopy (FILE * fromstream, FILE * tostream)
{
  int c;

  // 'Just to be sure'
  fflush (fromstream);
  fseek (fromstream, 0, SEEK_SET);

  // Urgh, using the assignment in the loop condition, brrr. Fugly.
  // Discourage.
  while ((c = fgetc (fromstream)) != EOF)
    {
      fputc (c, tostream);
    }
}

//! Output an attack in the desired way
void
arachneOutputAttack ()
{
  Termlist varlist;

  // Make concrete
  if (switches.concrete)
    {
      varlist = makeTraceConcrete (sys);
    }
  else
    {
      varlist = NULL;
    }

  // Wrapper for the real output
  attackOutputStart ();

  // Generate the output, already!
  if (switches.xml)
    {
      xmlOutSemitrace (sys);
    }
  else
    {
      dotSemiState (sys);
    }

  // End wrapper
  attackOutputStop ();

  // Undo concretization
  makeTraceClass (sys, varlist);
}

//------------------------------------------------------------------------
// Main logic core
//------------------------------------------------------------------------


//! Selector to select the first tuple goal.
/**
 * Basically to get rid of -m2 tuple goals.
 * Nice iteration, I'd suppose
 */
Binding
select_tuple_goal ()
{
  List bl;
  Binding tuplegoal;

  bl = sys->bindings;
  tuplegoal = NULL;
  while (bl != NULL && tuplegoal == NULL)
    {
      Binding b;

      b = (Binding) bl->data;
      // Ignore done stuff
      if (!b->blocked && !b->done)
	{
	  if (isTermTuple (b->term))
	    {
	      tuplegoal = b;
	    }
	}
      bl = bl->next;
    }
  return tuplegoal;
}


//! Iterate a binding
/**
 * For DY model, we unfold any tuples first, otherwise we skip that.
 */
int
iterateOneBinding (void)
{
  Binding btup;
  int flag;

  // marker
  flag = true;

  // Are there any tuple goals?
  if (switches.intruder)
    {
      // Maybe... (well, test)
      btup = select_tuple_goal ();
    }
  else
    {
      // No, there are non that need to be expanded (no intruder)
      btup = NULL;
    }
  if (btup != NULL)
    {
      /* Substitution or something resulted in a tuple goal: we immediately split them into compounds.
       */
      Term tuple;

      tuple = deVar (btup->term);
      if (realTermTuple (tuple))
	{
	  int count;
	  Term tupletermbuffer;

	  tupletermbuffer = btup->term;
	  /*
	   * We solve this by replacing the tuple goal by the left term, and adding a goal for the right term.
	   */
	  btup->term = TermOp1 (tuple);
	  count =
	    goal_add (TermOp2 (tuple), btup->run_to,
		      btup->ev_to, btup->level);

	  // Show this in output
	  if (switches.output == PROOF)
	    {
	      indentPrint ();
	      eprintf ("Expanding tuple goal ");
	      termPrint (tupletermbuffer);
	      eprintf (" into %i subgoals.\n", count);
	    }

	  // iterate
	  flag = iterate ();

	  // undo
	  goal_remove_last (count);
	  btup->term = tupletermbuffer;
	}
    }
  else
    {
      // No tuple goals; good
      Binding b;

		  /**
		   * Not pruned: count
		   */

      sys->states = statesIncrease (sys->states);
      sys->current_claim->states =
	statesIncrease (sys->current_claim->states);

		  /**
		   * Check whether its a final state (i.e. all goals bound)
		   */

      b = (Binding) select_goal (sys);
      if (b == NULL)
	{
	  /*
	   * all goals bound, check for property
	   */
	  if (switches.output == PROOF)
	    {
	      indentPrint ();
	      eprintf ("All goals are now bound.\n");
	    }
	  sys->claims = statesIncrease (sys->claims);
	  sys->current_claim->count =
	    statesIncrease (sys->current_claim->count);
	  flag = property_check (sys);
	}
      else
	{
	  /*
	   * bind this goal in all possible ways and iterate
	   */
	  flag = bind_goal_all_options (b);
	}
    }
  return flag;
}

//! Unfold this particular name in this way
void
iterateAgentUnfoldThis (const Term rolevar, const Term agent)
{
  Term buffer;

  buffer = rolevar->subst;
  rolevar->subst = agent;
  iterate ();
  rolevar->subst = buffer;
}

//! Unfold this particular name
void
iterateAgentUnfolding (const System sys, const Term rolevar)
{
  Termlist kl;
  int count;

  iterateAgentUnfoldThis (rolevar, AGENT_Eve);
  kl = knowledgeSet (sys->know);
  count = 0;
  while (kl != NULL && count < switches.agentUnfold)
    {
      Term t;

      t = deVar (kl->term);
      if (realTermLeaf (t) && inTermlist (t->stype, TERM_Agent))
	{
	  if (!inTermlist (sys->untrusted, t))
	    {
	      iterateAgentUnfoldThis (rolevar, t);
	      count++;
	    }
	}
      kl = kl->next;
    }
  termlistDelete (kl);
}

//! Unfold names 
/**
 * Returns true if nothing was unfolded and the iteration must be done.
 * Returns false when the iteration should not be done.
 */
int
doAgentUnfolding (const System sys)
{
  int run;

  for (run = 0; run < sys->maxruns; run++)
    {
      Termlist tl;

      tl = sys->runs[run].rho;
      while (tl != NULL)
	{
	  Term t;

	  t = deVar (tl->term);
	  if (realTermVariable (t))
	    {
	      // Hey, this role name is still a variable.
	      // We don't want that and so we unfold it as expected.
	      iterateAgentUnfolding (sys, t);
	      return false;
	    }
	  tl = tl->next;
	}
    }
  return true;
}

//! Main recursive procedure for Arachne
int
iterate ()
{
  int flag;

  flag = 1;

  // check unfolding agent names
  if (switches.agentUnfold > 0)
    {
      if (!doAgentUnfolding (sys))
	return flag;
    }

  if (!prune_theorems (sys))
    {
      if (!prune_claim_specifics (sys))
	{
	  if (!prune_bounds (sys))
	    {

	      // Go and pick a binding for iteration
	      flag = iterateOneBinding ();
	    }
	  else
	    {
	      // Pruned because of bound!
	      sys->current_claim->complete = 0;
	    }
	}
    }

#ifdef DEBUG
  if (DEBUGL (5) && !flag)
    {
      warning ("Flag has turned 0!");
    }
#endif

  return flag;
}

//! Just before starting output of an attack.
//
//! A wrapper for the case in which we need to buffer attacks.
int
iterate_buffer_attacks (void)
{
  if (useAttackBuffer ())
    {
      // We are pruning attacks, so they should go into a temporary file.
      /*
       * Set up the temporary file pointer
       */
      char *buffer;
      int result;

      // Push the old situation onto the stack
      buffer = globalStream;

      // Start stuff
      attack_stream = NULL;
      attackOutputStart ();

      // Finally, proceed with iteration procedure
      result = iterate ();

      /* Now, if it has been set, we need to copy the output to the normal streams.
       */
      fcopy (attack_stream, (FILE *) buffer);

      // Close
      fclose (attack_stream);
      attack_stream = NULL;

      // Restore
      globalStream = buffer;

      return result;
    }
  else
    {
      // No attack buffering, just output all of them
      return iterate ();
    }
}

//! Arachne single claim test
void
arachneClaimTest (Claimlist cl)
{
  // others we simply test...
  int run;
  int newruns;
  Protocol p;
  Role r;

  newruns = 0;
  sys->current_claim = cl;
  attack_length = INT_MAX;
  attack_leastcost = INT_MAX;
  cl->complete = 1;
  p = (Protocol) cl->protocol;
  r = (Role) cl->role;

  if (switches.output == PROOF)
    {
      indentPrint ();
      eprintf ("Testing Claim ");
      termPrint (cl->type);
      eprintf (" from ");
      termPrint (p->nameterm);
      eprintf (", ");
      termPrint (r->nameterm);
      eprintf (" at index %i.\n", cl->ev);
    }
  indentDepth++;

  run = semiRunCreate (p, r);
  newruns++;
  {
    int newgoals;

    int realStart (void)
    {
#ifdef DEBUG
      if (DEBUGL (5))
	{
	  printSemiState ();
	}
#endif
      return iterate_buffer_attacks ();
    }

    proof_suppose_run (run, 0, cl->ev + 1);
    newgoals = add_recv_goals (run, 0, cl->ev + 1);

		    /**
		     * Add initial knowledge node
		     */
    {
      Termlist m0tl;
      Term m0t;
      int m0run;

      m0tl = knowledgeSet (sys->know);
      if (m0tl != NULL)
	{
	  m0t = termlist_to_tuple (m0tl);
	  // eprintf("Initial intruder knowledge node for ");
	  // termPrint(m0t);
	  // eprintf("\n");
	  I_M->roledef->message = m0t;
	  m0run = semiRunCreate (INTRUDER, I_M);
	  newruns++;
	  proof_suppose_run (m0run, 0, 1);
	  sys->runs[m0run].height = 1;
	}
      else
	{
	  m0run = -1;
	}

      {
		      /**
		       * Add specific goal info and iterate algorithm
		       */
	add_claim_specifics (sys, cl,
			     roledef_shift (sys->runs[run].start, cl->ev),
			     realStart);
      }


      if (m0run != -1)
	{
	  // remove initial knowledge node
	  termDelete (m0t);
	  termlistDelete (m0tl);
	  semiRunDestroy ();
	  newruns--;
	}
    }
    // remove claiming run goals 
    goal_remove_last (newgoals);
    semiRunDestroy ();
    newruns--;
  }
  //! Destroy
  while (sys->maxruns > 0 && newruns > 0)
    {
      semiRunDestroy ();
      newruns--;
    }
#ifdef DEBUG
  if (sys->bindings != NULL)
    {
      error ("sys->bindings NOT empty after claim test.");
    }
  if (sys->maxruns != 0)
    {
      error ("%i undestroyed runs left after claim test.", sys->maxruns);
    }
  if (newruns != 0)
    {
      error ("Lost %i runs after claim test.", newruns);
    }
#endif

  //! Indent back
  indentDepth--;

  if (switches.output == PROOF)
    {
      indentPrint ();
      eprintf ("Proof complete for this claim.\n");
    }
}

//! Arachne single claim inspection
int
arachneClaim ()
{
  Claimlist cl;

  // Skip the dummy claims or SID markers
  cl = sys->current_claim;
  if (!isClaimSignal (cl))
    {
      // Some claims are always true!
      if (!cl->alwaystrue)
	{
	  // others we simply test...
	  arachneClaimTest (cl);
	}
      claimStatusReport (sys, cl);
      if (switches.xml)
	{
	  xmlOutClaim (sys, cl);
	}
      return true;
    }
  return false;
}


//! Main code for Arachne
/**
 * For this test, we manually set up some stuff.
 *
 * But later, this will just iterate over all claims.
 *
 * @TODO what does it return? And is that -1 valid, if nothing is tested?
 */
int
arachne ()
{
  Claimlist cl;
  int count;

  int print_send (Protocol p, Role r, Roledef rd, int index)
  {
    eprintf ("IRS: ");
    termPrint (p->nameterm);
    eprintf (", ");
    termPrint (r->nameterm);
    eprintf (", %i, ", index);
    roledefPrint (rd);
    eprintf ("\n");
    return 1;
  }

  int determine_encrypt_max (Protocol p, Role r, Roledef rd, int index)
  {
    int tlevel;

    tlevel = term_encryption_level (rd->message);
#ifdef DEBUG
    if (DEBUGL (3))
      {
	eprintf ("Encryption level %i found for term ", tlevel);
	termPrint (rd->message);
	eprintf ("\n");
      }
#endif
    if (tlevel > max_encryption_level)
      max_encryption_level = tlevel;
    return 1;
  }

  /*
   * set up claim role(s)
   */

  if (switches.runs == 0)
    {
      // No real checking.
      return -1;
    }

  if (sys->maxruns > 0)
    {
      error ("Something is wrong, number of runs >0.");
    }

  sys->num_regular_runs = 0;
  sys->num_intruder_runs = 0;

  max_encryption_level = 0;
  iterate_role_events (determine_encrypt_max);
#ifdef DEBUG
  if (DEBUGL (1))
    {
      eprintf ("Maximum encryption level: %i\n", max_encryption_level);
    }
#endif

  fixAgentKeylevels ();

  indentDepth = 0;
  proofDepth = 0;
  cl = sys->claimlist;
  count = 0;
  while (cl != NULL)
    {
      /**
       * Check each claim
       */
      sys->current_claim = cl;
      if (isClaimRelevant (cl))	// check for any filtered claims (switch)
	{
	  if (arachneClaim ())
	    {
	      count++;
	    }
	}

      // next
      cl = cl->next;
    }
  return count;
}

//! Construct knowledge set at some event, based on a semitrace.
/**
 * This is a very 'stupid' algorithm; it is just there because GijsH
 * requested it. It does in no way guarantee that this is the actual
 * knowledge set at the given point. It simply gives an underapproximation,
 * that will be correct in most cases. The main reason for this is that it
 * completely ignores any information on unbound variables, and regards them
 * as bound constants.
 *
 * Because everything is supposed to be bound, we conclude that even 'recv'
 * events imply a certain knowledge.
 *
 * If aftercomplete is 0 or false, we actually check the ordering; otherwise we
 * just assume the trace has finished.
 *
 * Use knowledgeDelete later to clean up.
 */
Knowledge
knowledgeAtArachne (const System sys, const int myrun, const int myindex,
		    const int aftercomplete)
{
  Knowledge know;
  int run;

  know = knowledgeDuplicate (sys->know);	// duplicate initial knowledge
  run = 0;
  while (run < sys->maxruns)
    {
      int index;
      int maxheight;
      Roledef rd;

      index = 0;
      rd = sys->runs[run].start;
      maxheight = sys->runs[run].height;
      if (run == myrun && myindex > maxheight)
	{
	  // local run index can override real step
	  maxheight = myindex;
	}

      while (rd != NULL && index < maxheight)
	{
	  // Check whether this event precedes myevent
	  if (aftercomplete || isDependEvent (run, index, myrun, myindex))
	    {
	      // If it is a send (trivial) or a recv (remarkable, but true
	      // because of bindings) we can add the message and the agents to
	      // the knowledge.
	      if (rd->type == SEND || rd->type == RECV)
		{
		  knowledgeAddTerm (know, rd->message);
		  if (rd->from != NULL)
		    knowledgeAddTerm (know, rd->from);
		  if (rd->to != NULL)
		    knowledgeAddTerm (know, rd->to);
		}
	      index++;
	      rd = rd->next;
	    }
	  else
	    {
	      // Not ordered before anymore, so we skip to the next run.
	      rd = NULL;
	    }
	}
      run++;
    }
  return know;
}

//! Determine whether a term is trivially known at some event in a partially ordered structure.
/**
 * Important: read disclaimer at knowledgeAtArachne()
 *
 * Returns true iff the term is certainly known at that point in the
 * semitrace.
 */
int
isTriviallyKnownAtArachne (const System sys, const Term t, const int run,
			   const int index)
{
  int result;
  Knowledge knowset;

  knowset = knowledgeAtArachne (sys, run, index, false);
  result = inKnowledge (knowset, t);
  knowledgeDelete (knowset);
  return result;
}

//! Determine whether a term is trivially known after execution of some partially ordered structure.
/**
 * Important: read disclaimer at knowledgeAtArachne()
 *
 * Returns true iff the term is certainly known after all events in the
 * semitrace.
 */
int
isTriviallyKnownAfterArachne (const System sys, const Term t, const int run,
			      const int index)
{
  int result;
  Knowledge knowset;

  knowset = knowledgeAtArachne (sys, run, index, true);
  result = inKnowledge (knowset, t);
  knowledgeDelete (knowset);
  return result;
}

//! Mark that we have no full proof
/**
 * Provides an interface for marking incomplete proofs.
 * Currently used in mgusubterm in mgu.c
 */
void
markNoFullProof (const Term tbig, const Term tsmall)
{
  // Comment in proof
  if (switches.output == PROOF)
    {
      indentPrint ();
      eprintf ("Note: the pattern set will be incomplete, because ");
      termPrint (tbig);
      eprintf (" allows for infinitely many ways to subtermUnify ");
      termPrint (tsmall);
      eprintf (".\n");
    }
  sys->current_claim->complete = false;
}