andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
369ae1e3f8
scyther/src/arachne.c
Cas Cremers 7956eb5953 Removed a simple nested function.
2018-10-14 17:43:13 +02:00

2796 lines
58 KiB
C
Raw Blame History

/*
* 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;
}
//! 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)
{
int test_sub_unification (Termlist substlist, Termlist keylist)
{
// A unification exists; return the signal
return false;
}
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;
}
Reference in New Issue View Git Blame Copy Permalink