BROKEN
- Working on new algorithm. Some memory error can occur.
This commit is contained in:
ccremers
parent
c5695d6fe8
commit
b2d21f0a8a
506
src/arachne.c
506
src/arachne.c
@ -36,6 +36,7 @@ Role I_E;
|
||||
Role I_D;
|
||||
|
||||
static int indentDepth;
|
||||
static int max_encryption_level;
|
||||
|
||||
#ifdef DEBUG
|
||||
static char *explanation; // Pointer to a string that describes what we just tried to do
|
||||
@ -68,6 +69,7 @@ int iterate ();
|
||||
void
|
||||
arachneInit (const System mysys)
|
||||
{
|
||||
Term GVT;
|
||||
Roledef rd = NULL;
|
||||
Termlist tl, know0;
|
||||
|
||||
@ -102,8 +104,9 @@ arachneInit (const System mysys)
|
||||
*/
|
||||
|
||||
INTRUDER = protocolCreate (makeGlobalConstant (" INTRUDER "));
|
||||
GVT = makeGlobalVariable ("GlobalVariable");
|
||||
|
||||
add_event (SEND, NULL);
|
||||
add_event (SEND, GVT);
|
||||
I_M = add_role ("I_M: Atomic message");
|
||||
|
||||
add_event (READ, NULL);
|
||||
@ -148,6 +151,18 @@ indentPrint ()
|
||||
#endif
|
||||
}
|
||||
|
||||
//! Print indented binding
|
||||
void
|
||||
binding_indent_print (Binding b, int flag)
|
||||
{
|
||||
indentPrint ();
|
||||
if (flag)
|
||||
eprintf ("!! ");
|
||||
binding_print (b);
|
||||
eprintf ("\n");
|
||||
}
|
||||
|
||||
|
||||
//! Iterate but discard the info of the termlist
|
||||
int
|
||||
mgu_iterate (const Termlist tl)
|
||||
@ -161,7 +176,7 @@ mgu_iterate (const Termlist tl)
|
||||
*@returns The number of goals added (for destructions)
|
||||
*/
|
||||
int
|
||||
add_read_goals (const int run, int old, int new)
|
||||
add_read_goals (const int run, const int old, const int new)
|
||||
{
|
||||
int count;
|
||||
int i;
|
||||
@ -170,11 +185,13 @@ add_read_goals (const int run, int old, int new)
|
||||
sys->runs[run].length = new;
|
||||
i = old;
|
||||
rd = roledef_shift (sys->runs[run].start, i);
|
||||
while (i < new)
|
||||
count = 0;
|
||||
while (i < new && rd != NULL)
|
||||
{
|
||||
if (rd->type == READ)
|
||||
{
|
||||
goal_add (rd->message, run, i);
|
||||
count++;
|
||||
}
|
||||
rd = rd->next;
|
||||
i++;
|
||||
@ -186,7 +203,7 @@ add_read_goals (const int run, int old, int new)
|
||||
void
|
||||
remove_read_goals (int n)
|
||||
{
|
||||
while (n>0)
|
||||
while (n > 0)
|
||||
{
|
||||
goal_remove_last ();
|
||||
n--;
|
||||
@ -301,43 +318,59 @@ bind_existing_to_goal (const Binding b, const int index, const int run,
|
||||
|
||||
int subterm_iterate (Termlist substlist, Termlist keylist)
|
||||
{
|
||||
int keycount;
|
||||
int flag;
|
||||
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Adding key list : ");
|
||||
termlistPrint (keylist);
|
||||
eprintf ("\n");
|
||||
}
|
||||
#endif
|
||||
flag = 1;
|
||||
keycount = 0;
|
||||
while (flag && keylist != NULL)
|
||||
if (goal_bind (b, run, index))
|
||||
{
|
||||
int keyrun;
|
||||
int keycount;
|
||||
Termlist tl;
|
||||
|
||||
goal_add (keylist->term, b->run_to, b->ev_to);
|
||||
keylist = keylist->next;
|
||||
keycount++;
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
binding_indent_print (b, 0);
|
||||
indentPrint ();
|
||||
eprintf ("Adding key list for subterm iteration: ");
|
||||
termlistPrint (keylist);
|
||||
eprintf ("\n");
|
||||
}
|
||||
#endif
|
||||
keycount = 0;
|
||||
tl = keylist;
|
||||
while (tl != NULL)
|
||||
{
|
||||
int keyrun;
|
||||
|
||||
goal_add (tl->term, b->run_to, b->ev_to);
|
||||
tl = tl->next;
|
||||
keycount++;
|
||||
}
|
||||
|
||||
flag = flag && iterate ();
|
||||
|
||||
while (keycount > 0)
|
||||
{
|
||||
goal_remove_last ();
|
||||
keycount--;
|
||||
}
|
||||
termlistDestroy (keylist);
|
||||
}
|
||||
flag = flag && iterate ();
|
||||
while (keycount > 0)
|
||||
else
|
||||
{
|
||||
goal_remove_last ();
|
||||
keycount--;
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Aborted binding existing run because of cycle.\n");
|
||||
}
|
||||
#endif
|
||||
flag = 0;
|
||||
}
|
||||
termlistDestroy (keylist);
|
||||
goal_unbind (b);
|
||||
return flag;
|
||||
}
|
||||
|
||||
int interm_iterate (Termlist substlist)
|
||||
{
|
||||
iterate ();
|
||||
}
|
||||
|
||||
//----------------------------
|
||||
// Roledef entry
|
||||
rd = roledef_shift (sys->runs[run].start, index);
|
||||
@ -345,13 +378,9 @@ bind_existing_to_goal (const Binding b, const int index, const int run,
|
||||
// Fix length
|
||||
old_length = sys->runs[run].length;
|
||||
if ((index + 1) > old_length)
|
||||
{
|
||||
newgoals = add_read_goals (run, old_length, index+1);
|
||||
}
|
||||
newgoals = add_read_goals (run, old_length, index + 1);
|
||||
else
|
||||
{
|
||||
newgoals = 0;
|
||||
}
|
||||
newgoals = 0;
|
||||
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (3))
|
||||
@ -361,30 +390,8 @@ bind_existing_to_goal (const Binding b, const int index, const int run,
|
||||
e_term1 = b->term;
|
||||
}
|
||||
#endif
|
||||
if (goal_bind (b, run, index))
|
||||
{
|
||||
if (subterm)
|
||||
{
|
||||
flag = termMguSubTerm (b->term, rd->message,
|
||||
subterm_iterate, sys->know->inverses, NULL);
|
||||
}
|
||||
else
|
||||
{
|
||||
flag = termMguInTerm (b->term, rd->message,
|
||||
interm_iterate);
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Aborted binding existing run because of cycle.\n");
|
||||
}
|
||||
#endif
|
||||
}
|
||||
goal_unbind (b);
|
||||
flag = termMguSubTerm (b->term, rd->message,
|
||||
subterm_iterate, sys->know->inverses, NULL);
|
||||
// Reset length
|
||||
remove_read_goals (newgoals);
|
||||
sys->runs[run].length = old_length;
|
||||
@ -404,7 +411,7 @@ bind_existing_run (const Binding b, const Protocol p, const Role r,
|
||||
indentPrint ();
|
||||
eprintf ("Trying to bind ");
|
||||
termPrint (b->term);
|
||||
eprintf (" to an existing instance of ");
|
||||
eprintf (" to an existing (of %i runs) instance of ", sys->maxruns);
|
||||
termPrint (p->nameterm);
|
||||
eprintf (", ");
|
||||
termPrint (r->nameterm);
|
||||
@ -433,7 +440,7 @@ bind_new_run (const Binding b, const Protocol p, const Role r,
|
||||
|
||||
roleInstance (sys, p, r, NULL, NULL);
|
||||
run = sys->maxruns - 1;
|
||||
newgoals = add_read_goals (run, 0, index+1);
|
||||
newgoals = add_read_goals (run, 0, index + 1);
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (4))
|
||||
{
|
||||
@ -447,9 +454,9 @@ bind_new_run (const Binding b, const Protocol p, const Role r,
|
||||
eprintf (", run %i (subterm:%i)\n", run, subterm);
|
||||
}
|
||||
#endif
|
||||
flag = bind_existing_to_goal (b, index, run, subterm);
|
||||
roleInstanceDestroy (sys);
|
||||
flag = bind_existing_to_goal (b, index, run, 1);
|
||||
remove_read_goals (newgoals);
|
||||
roleInstanceDestroy (sys);
|
||||
return flag;
|
||||
}
|
||||
|
||||
@ -461,11 +468,9 @@ printSemiState ()
|
||||
int open;
|
||||
List bl;
|
||||
|
||||
int binding_indent_print (void *data)
|
||||
int binding_state_print (void *dt)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("!! ");
|
||||
binding_print (data);
|
||||
binding_indent_print ((Binding) dt, 1);
|
||||
return 1;
|
||||
}
|
||||
|
||||
@ -515,7 +520,7 @@ printSemiState ()
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("!!\n");
|
||||
list_iterate (sys->bindings, binding_indent_print);
|
||||
list_iterate (sys->bindings, binding_state_print);
|
||||
}
|
||||
indentPrint ();
|
||||
eprintf ("!!\n");
|
||||
@ -536,7 +541,9 @@ select_goal ()
|
||||
{
|
||||
List bl;
|
||||
Binding best;
|
||||
float min_constrain;
|
||||
|
||||
min_constrain = 2; // 1 is the maximum, but we want to initialize it.
|
||||
best = NULL;
|
||||
bl = sys->bindings;
|
||||
while (bl != NULL)
|
||||
@ -546,141 +553,20 @@ select_goal ()
|
||||
b = (Binding) bl->data;
|
||||
if (!b->done)
|
||||
{
|
||||
// For now, we simply take the first encountered goal
|
||||
return b;
|
||||
float cons;
|
||||
|
||||
cons = term_constrain_level (b->term);
|
||||
if (cons < min_constrain)
|
||||
{
|
||||
min_constrain = cons;
|
||||
best = b;
|
||||
}
|
||||
}
|
||||
bl = bl->next;
|
||||
}
|
||||
return best;
|
||||
}
|
||||
|
||||
//! Bind a regular goal
|
||||
int
|
||||
bind_goal_regular (const Binding b)
|
||||
{
|
||||
int flag;
|
||||
/*
|
||||
* 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_unification (Termlist substlist)
|
||||
{
|
||||
// A unification exists; return the signal
|
||||
return 0;
|
||||
}
|
||||
|
||||
if (p == INTRUDER)
|
||||
{
|
||||
/* only bind to regular runs */
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
// 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 (!termMguInTerm (b->term, rd->message, test_unification))
|
||||
{
|
||||
// A good candidate
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Term ");
|
||||
termPrint (b->term);
|
||||
eprintf (" can possibly be bound by role ");
|
||||
termPrint (r->nameterm);
|
||||
eprintf (", index %i\n", index);
|
||||
}
|
||||
#endif
|
||||
return (bind_new_run (b, p, r, index, 0) &&
|
||||
bind_existing_run (b, p, r, index, 0));
|
||||
}
|
||||
else
|
||||
{
|
||||
// Cannot unify: no attacks
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Bind to all possible sends or intruder node;
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Try regular role send.\n");
|
||||
}
|
||||
#endif
|
||||
flag = iterate_role_sends (bind_this_role_send);
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Try intruder send.\n");
|
||||
}
|
||||
#endif
|
||||
return flag;
|
||||
// return (flag && add_intruder_goal_iterate (b));
|
||||
}
|
||||
|
||||
//! Bind an intruder goal to a regular run
|
||||
int
|
||||
bind_intruder_to_regular (Binding b)
|
||||
{
|
||||
int bind_this_roleevent (Protocol p, Role r, Roledef rd, int index)
|
||||
{
|
||||
int cannotUnify;
|
||||
|
||||
int test_unification (Termlist substlist, Termlist keylist)
|
||||
{
|
||||
// Signal that unification is possible.
|
||||
return 0;
|
||||
}
|
||||
|
||||
/**
|
||||
* Note that we only bind to regular runs here
|
||||
*/
|
||||
if (p == INTRUDER)
|
||||
{
|
||||
return 1; // don't abort scans
|
||||
}
|
||||
else
|
||||
{ // Test for subterm unification
|
||||
if (termMguSubTerm
|
||||
(b->term, rd->message, test_unification,
|
||||
sys->know->inverses, NULL))
|
||||
{
|
||||
// cannot unify
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
/**
|
||||
* Either from an existing, or from a new run.
|
||||
*/
|
||||
return (bind_new_run (b, p, r, index, 1)
|
||||
&& bind_existing_run (b, p, r, index, 1));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Bind to all possible sends?
|
||||
return iterate_role_sends (bind_this_roleevent);
|
||||
}
|
||||
|
||||
//! Bind an intruder goal by intruder construction
|
||||
/**
|
||||
* Handles the case where the intruder constructs a composed term himself.
|
||||
@ -696,9 +582,9 @@ bind_intruder_to_construct (const Binding b)
|
||||
flag = 1;
|
||||
term = b->term;
|
||||
/**
|
||||
* Two options.
|
||||
* Three options.
|
||||
*
|
||||
* 1. Constructed from composite terms
|
||||
* 1. Constructed from smaller composite terms
|
||||
*/
|
||||
if (!realTermLeaf (term))
|
||||
{
|
||||
@ -706,6 +592,7 @@ bind_intruder_to_construct (const Binding b)
|
||||
|
||||
if (realTermTuple (term))
|
||||
{
|
||||
warning ("Goal that is a tuple should not occur!");
|
||||
// tuple construction
|
||||
t1 = term->left.op1;
|
||||
t2 = term->right.op2;
|
||||
@ -719,12 +606,61 @@ bind_intruder_to_construct (const Binding b)
|
||||
|
||||
goal_add (t1, b->run_to, b->ev_to);
|
||||
goal_add (t2, b->run_to, b->ev_to);
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (3))
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Constructing ");
|
||||
termPrint (term);
|
||||
eprintf (" from smaller terms ");
|
||||
termPrint (t1);
|
||||
eprintf (" and ");
|
||||
termPrint (t2);
|
||||
eprintf ("\n");
|
||||
}
|
||||
#endif
|
||||
flag = flag && iterate ();
|
||||
goal_remove_last ();
|
||||
goal_remove_last ();
|
||||
}
|
||||
/**
|
||||
* 2. Retrieved from M_0
|
||||
* 2. Constructed from bigger term and decryption key
|
||||
*/
|
||||
/*
|
||||
if (!realTermLeaf (term))
|
||||
{
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
Term t1, t2;
|
||||
|
||||
t1 = term->left.op;
|
||||
t2 = term->right.key;
|
||||
|
||||
goal_add (t1, b->run_to, b->ev_to);
|
||||
goal_add (t2, b->run_to, b->ev_to);
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (3))
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Deriving ");
|
||||
termPrint (term);
|
||||
eprintf (" from encrypted term ");
|
||||
termPrint (t1);
|
||||
eprintf (" and key ");
|
||||
termPrint (t2);
|
||||
eprintf ("\n");
|
||||
}
|
||||
#endif
|
||||
flag = flag && iterate ();
|
||||
goal_remove_last ();
|
||||
goal_remove_last ();
|
||||
}
|
||||
|
||||
}
|
||||
*/
|
||||
|
||||
/**
|
||||
* 3. Retrieved from M_0
|
||||
*/
|
||||
m0tl = knowledgeSet (sys->know);
|
||||
while (flag && m0tl != NULL)
|
||||
@ -747,15 +683,20 @@ bind_intruder_to_construct (const Binding b)
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (3))
|
||||
{
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
binding_indent_print (b, 0);
|
||||
}
|
||||
indentPrint ();
|
||||
eprintf ("Retrieving ");
|
||||
termPrint (term);
|
||||
eprintf (" from the initial knowledge.\n");
|
||||
}
|
||||
#endif
|
||||
iterate ();
|
||||
flag = flag && iterate ();
|
||||
}
|
||||
goal_unbind (b);
|
||||
roleInstanceDestroy (sys);
|
||||
termlistSubstReset (subst);
|
||||
termlistDelete (subst);
|
||||
}
|
||||
@ -770,57 +711,104 @@ bind_intruder_to_construct (const Binding b)
|
||||
}
|
||||
|
||||
|
||||
//! Bind an intruder goal
|
||||
/**
|
||||
* Computes F2 as in Athena explanations.
|
||||
*/
|
||||
//! Bind a regular goal
|
||||
int
|
||||
bind_goal_intruder (const Binding b)
|
||||
bind_goal_regular (const Binding b)
|
||||
{
|
||||
/**
|
||||
* Special case: when the intruder can bind it to the initial knowledge.
|
||||
*/
|
||||
Termlist tl;
|
||||
int flag;
|
||||
|
||||
flag = 1;
|
||||
tl = knowledgeSet (sys->know);
|
||||
while (flag && tl != NULL)
|
||||
/*
|
||||
* 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_unification (Termlist substlist)
|
||||
{
|
||||
int hasvars;
|
||||
Termlist substlist;
|
||||
|
||||
substlist = termMguTerm (tl->term, b->term);
|
||||
if (substlist != MGUFAIL)
|
||||
{
|
||||
// This seems to work
|
||||
flag = flag && iterate ();
|
||||
termlistSubstReset (substlist);
|
||||
termlistDelete (substlist);
|
||||
}
|
||||
tl = tl->next;
|
||||
// A unification exists; return the signal
|
||||
return 0;
|
||||
}
|
||||
termlistDelete (tl);
|
||||
return (flag && bind_intruder_to_regular (b) &&
|
||||
bind_intruder_to_construct (b));
|
||||
|
||||
// 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 (!termMguSubTerm
|
||||
(b->term, rd->message, test_unification, sys->know->inverses, NULL))
|
||||
{
|
||||
int flag;
|
||||
|
||||
// A good candidate
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Term ");
|
||||
termPrint (b->term);
|
||||
eprintf (" can possibly be bound by role ");
|
||||
termPrint (r->nameterm);
|
||||
eprintf (", index %i\n", index);
|
||||
}
|
||||
#endif
|
||||
// Bind to existing run
|
||||
flag = bind_existing_run (b, p, r, index, 1);
|
||||
if (p != INTRUDER)
|
||||
{
|
||||
// No intruder: bind to new run
|
||||
flag = flag && bind_new_run (b, p, r, index, 1);
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
else
|
||||
{
|
||||
// Cannot unify: no attacks
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
// Bind to all possible sends or intruder node;
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Try regular role send.\n");
|
||||
}
|
||||
#endif
|
||||
flag = iterate_role_sends (bind_this_role_send);
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Try intruder send.\n");
|
||||
}
|
||||
#endif
|
||||
|
||||
// Other option: bind to term construction
|
||||
|
||||
flag = flag && bind_intruder_to_construct (b);
|
||||
|
||||
// Return result
|
||||
return flag;
|
||||
}
|
||||
|
||||
|
||||
|
||||
//! Bind a goal in all possible ways
|
||||
int
|
||||
bind_goal (const Binding b)
|
||||
{
|
||||
if (!b->done)
|
||||
{
|
||||
int flag;
|
||||
if (sys->runs[b->run_to].protocol == INTRUDER)
|
||||
{
|
||||
flag = bind_goal_intruder (b);
|
||||
}
|
||||
else
|
||||
{
|
||||
flag = bind_goal_regular (b);
|
||||
}
|
||||
return flag;
|
||||
return bind_goal_regular (b);
|
||||
}
|
||||
else
|
||||
{
|
||||
@ -906,6 +894,19 @@ prune ()
|
||||
tl = tl->next;
|
||||
}
|
||||
|
||||
// Check for c-minimality
|
||||
if (!bindings_c_minimal ())
|
||||
{
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (3))
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Pruned because this is not <=c-minimal.\n");
|
||||
}
|
||||
#endif
|
||||
return 1;
|
||||
}
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
||||
@ -976,7 +977,7 @@ iterate ()
|
||||
*/
|
||||
|
||||
b = select_goal ();
|
||||
if (b != NULL)
|
||||
if (b == NULL)
|
||||
{
|
||||
/*
|
||||
* all goals bound, check for property
|
||||
@ -1046,11 +1047,26 @@ arachne ()
|
||||
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);
|
||||
if (tlevel > max_encryption_level)
|
||||
max_encryption_level = tlevel;
|
||||
return 1;
|
||||
}
|
||||
|
||||
max_encryption_level = 0;
|
||||
iterate_role_sends (determine_encrypt_max);
|
||||
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (1))
|
||||
{
|
||||
eprintf ("Maximum encryption level: %i\n", max_encryption_level);
|
||||
iterate_role_sends (print_send);
|
||||
}
|
||||
#endif
|
||||
@ -1123,13 +1139,3 @@ arachne ()
|
||||
cl = cl->next;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Done: add_read_goals, remove_read_goals.
|
||||
*
|
||||
* Now we must make the new algorithm.
|
||||
* At role instance (of e.g. claim), fix add_read_goals.
|
||||
*
|
||||
* Iterate on roles. Create new roles for intruder (encrypt RRS, decrypt RRS, and M_0 S)
|
||||
* Check for bindings_c_minimal.
|
||||
*/
|
||||
|
||||
@ -11,7 +11,7 @@
|
||||
#include "term.h"
|
||||
|
||||
static System sys;
|
||||
static int* graph;
|
||||
static int *graph;
|
||||
static int nodes;
|
||||
|
||||
/*
|
||||
@ -78,7 +78,8 @@ bindingDone ()
|
||||
}
|
||||
|
||||
//! Destroy graph
|
||||
void goal_graph_destroy ()
|
||||
void
|
||||
goal_graph_destroy ()
|
||||
{
|
||||
if (graph != NULL)
|
||||
{
|
||||
@ -88,13 +89,14 @@ void goal_graph_destroy ()
|
||||
}
|
||||
|
||||
//! Compute unclosed graph
|
||||
void goal_graph_create ()
|
||||
void
|
||||
goal_graph_create ()
|
||||
{
|
||||
int run, ev;
|
||||
List bl;
|
||||
|
||||
goal_graph_destroy ();
|
||||
|
||||
|
||||
// Setup graph
|
||||
nodes = node_count ();
|
||||
graph = memAlloc ((nodes * nodes) * sizeof (int));
|
||||
@ -120,14 +122,18 @@ void goal_graph_create ()
|
||||
Binding b;
|
||||
|
||||
b = (Binding) bl->data;
|
||||
if (b->done)
|
||||
{
|
||||
#ifdef DEBUG
|
||||
if (graph_nodes (nodes, b->run_from, b->ev_from, b->run_to, b->ev_to) >=
|
||||
(nodes * nodes))
|
||||
error ("Node out of scope for %i,%i -> %i,%i.\n", b->run_from,
|
||||
b->ev_from, b->run_to, b->ev_to);
|
||||
if (graph_nodes
|
||||
(nodes, b->run_from, b->ev_from, b->run_to,
|
||||
b->ev_to) >= (nodes * nodes))
|
||||
error ("Node out of scope for %i,%i -> %i,%i.\n", b->run_from,
|
||||
b->ev_from, b->run_to, b->ev_to);
|
||||
#endif
|
||||
graph[graph_nodes (nodes, b->run_from, b->ev_from, b->run_to, b->ev_to)]
|
||||
= 1;
|
||||
graph[graph_nodes
|
||||
(nodes, b->run_from, b->ev_from, b->run_to, b->ev_to)] = 1;
|
||||
}
|
||||
bl = bl->next;
|
||||
}
|
||||
}
|
||||
@ -203,13 +209,14 @@ graph_nodes (const int nodes, const int run1, const int ev1, const int run2,
|
||||
|
||||
//! Print a binding (given a binding list pointer)
|
||||
int
|
||||
binding_print (void *bindany)
|
||||
binding_print (const Binding b)
|
||||
{
|
||||
Binding b;
|
||||
|
||||
b = (Binding) bindany;
|
||||
eprintf ("Binding (%i,%i) --->> (%i,%i)\n", b->run_from, b->ev_from,
|
||||
b->run_to, b->ev_to);
|
||||
if (b->done)
|
||||
eprintf ("Binding (%i,%i) --( ", b->run_from, b->ev_from);
|
||||
else
|
||||
eprintf ("Unbound --( ");
|
||||
termPrint (b->term);
|
||||
eprintf (" )->> (%i,%i)", b->run_to, b->ev_to);
|
||||
return 1;
|
||||
}
|
||||
|
||||
@ -306,51 +313,63 @@ goal_unbind (const Binding b)
|
||||
*
|
||||
*@returns True, if it's okay. If false, it needs to be pruned.
|
||||
*/
|
||||
int bindings_c_minimal ()
|
||||
int
|
||||
bindings_c_minimal ()
|
||||
{
|
||||
List bl;
|
||||
|
||||
// Ensure a state graph
|
||||
goal_graph_create ();
|
||||
if (graph == NULL)
|
||||
{
|
||||
goal_graph_create ();
|
||||
// Recompute closure; does that work?
|
||||
if (!warshall (graph, nodes))
|
||||
{
|
||||
// Hmm, cycle
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
// For all goals
|
||||
bl = sys->bindings;
|
||||
while (bl != NULL)
|
||||
{
|
||||
Binding b;
|
||||
int run;
|
||||
int node_from;
|
||||
|
||||
b = (Binding) bl->data;
|
||||
node_from = node_number (b->run_from, b->ev_from);
|
||||
// Find all preceding events
|
||||
for (run = 0; run <= sys->maxruns; run++)
|
||||
if (b->done)
|
||||
{
|
||||
int ev;
|
||||
int run;
|
||||
int node_from;
|
||||
|
||||
//!@todo hardcoded reference to step, should be length
|
||||
for (ev = 0; run < sys->runs[run].step; ev++)
|
||||
node_from = node_number (b->run_from, b->ev_from);
|
||||
// Find all preceding events
|
||||
for (run = 0; run <= sys->maxruns; run++)
|
||||
{
|
||||
int node_comp;
|
||||
int ev;
|
||||
|
||||
node_comp = node_number (run, ev);
|
||||
if (graph[ graph_index (node_comp, node_from)] > 0)
|
||||
//!@todo hardcoded reference to step, should be length
|
||||
for (ev = 0; run < sys->runs[run].step; ev++)
|
||||
{
|
||||
// this node is *before* the from node
|
||||
Roledef rd;
|
||||
int node_comp;
|
||||
|
||||
rd = roledef_shift (sys->runs[run].start, ev);
|
||||
if (termInTerm (rd->message, b->term))
|
||||
node_comp = node_number (run, ev);
|
||||
if (graph[graph_index (node_comp, node_from)] > 0)
|
||||
{
|
||||
// This term already occurs as interm in a previous node!
|
||||
return 0;
|
||||
// this node is *before* the from node
|
||||
Roledef rd;
|
||||
|
||||
rd = roledef_shift (sys->runs[run].start, ev);
|
||||
if (termInTerm (rd->message, b->term))
|
||||
{
|
||||
// This term already occurs as interm in a previous node!
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bl = bl->next;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
||||
@ -9,8 +9,8 @@
|
||||
*/
|
||||
struct binding
|
||||
{
|
||||
int done; //!< Iff true, it is bound
|
||||
int child; //!< Signifies some tuple unfolding, to remove created bindings.
|
||||
int done; //!< Iff true, it is bound
|
||||
int child; //!< Signifies some tuple unfolding, to remove created bindings.
|
||||
|
||||
int run_from;
|
||||
int ev_from;
|
||||
@ -34,7 +34,7 @@ int node_count ();
|
||||
int node_number (int run, int ev);
|
||||
|
||||
|
||||
int binding_print (void *bindany);
|
||||
int binding_print (Binding b);
|
||||
|
||||
void goal_add (Term term, const int run, const int ev);
|
||||
void goal_remove_last ();
|
||||
|
||||
@ -109,6 +109,13 @@ makeGlobalConstant (const char *s)
|
||||
return levelDeclare (symbolSysConst (s), 0, 0);
|
||||
}
|
||||
|
||||
//! Make a global variable
|
||||
Term
|
||||
makeGlobalVariable (const char *s)
|
||||
{
|
||||
return levelDeclare (symbolSysConst (s), 1, 0);
|
||||
}
|
||||
|
||||
//! Clean up afterwards
|
||||
void
|
||||
compilerDone (void)
|
||||
|
||||
@ -12,6 +12,7 @@ void compile (Tac tc, int maxruns);
|
||||
void preprocess (const System sys);
|
||||
Term findGlobalConstant (const char *s);
|
||||
Term makeGlobalConstant (const char *s);
|
||||
Term makeGlobalVariable (const char *s);
|
||||
void compute_role_variables (const System sys, Protocol p, Role r);
|
||||
|
||||
#endif
|
||||
|
||||
48
src/ns3
48
src/ns3
@ -12,8 +12,8 @@ protocol ns3(I,R)
|
||||
send_1(I,R, {I,ni}pk(R) );
|
||||
read_2(R,I, {ni,nr}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
claim_4(I,Secret,ni,nr);
|
||||
claim_6(I,Nisynch);
|
||||
// claim_4(I,Secret,ni,nr);
|
||||
// claim_6(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
@ -24,49 +24,13 @@ protocol ns3(I,R)
|
||||
read_1(I,R, {I,ni}pk(R) );
|
||||
send_2(R,I, {ni,nr}pk(I) );
|
||||
read_3(I,R, {nr}pk(R) );
|
||||
claim_5(R,Secret,ni,nr);
|
||||
claim_7(R,Nisynch);
|
||||
claim_5(R,Secret,nr);
|
||||
// claim_5(R,Secret,ni,nr);
|
||||
// claim_7(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
// We leave out: M (from M_0) and Decryption, because that causes
|
||||
// problems with the inverse key.
|
||||
protocol I_MALICE (I_F, I_T, I_V, I_R, I_E)
|
||||
{
|
||||
role I_F {
|
||||
var t;
|
||||
read_if1 (F,F, t);
|
||||
}
|
||||
role I_T {
|
||||
var t;
|
||||
read_it1 (T,T, t);
|
||||
send_it2 (T,T, t);
|
||||
send_it3 (T,T, t);
|
||||
}
|
||||
role I_V {
|
||||
var t1;
|
||||
var t2;
|
||||
read_iv1 (V,V, t1);
|
||||
read_iv2 (V,V, t2);
|
||||
send_iv3 (V,V, (t1,t2));
|
||||
}
|
||||
role I_R {
|
||||
var t1;
|
||||
var t2;
|
||||
read_ir1 (I_R,I_R, (t1,t2));
|
||||
read_ir2 (I_R,I_R, t1);
|
||||
send_ir3 (I_R,I_R, t2);
|
||||
}
|
||||
role I_E {
|
||||
var t1;
|
||||
var t2;
|
||||
read_ie1 (I_E,I_E, t1);
|
||||
read_ie2 (I_E,I_E, t2);
|
||||
send_ie3 (I_E,I_E, {t1}t2);
|
||||
}
|
||||
}
|
||||
|
||||
const Alice,Bob,Eve: Agent;
|
||||
const Alice,Eve: Agent;
|
||||
|
||||
untrusted Eve;
|
||||
const nc: Nonce;
|
||||
|
||||
66
src/term.c
66
src/term.c
@ -1037,3 +1037,69 @@ term_rolelocals_are_variables ()
|
||||
{
|
||||
rolelocal_variable = 1;
|
||||
}
|
||||
|
||||
//! Count the encryption level of a term
|
||||
int
|
||||
term_encryption_level (const Term term)
|
||||
{
|
||||
int level, maxlevel, flag;
|
||||
|
||||
int nodel (const Term term)
|
||||
{
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
level++;
|
||||
if (level > maxlevel)
|
||||
maxlevel = level;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
int noder (const Term term)
|
||||
{
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
level--;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
maxlevel = 0;
|
||||
level = 0;
|
||||
flag = term_iterate_deVar (term, NULL, nodel, NULL, noder);
|
||||
return maxlevel;
|
||||
}
|
||||
|
||||
//! Determine 'constrained factor' of a term
|
||||
/**
|
||||
* Actually this is (#vars/structure).
|
||||
* Thus, 0 means very constrained, no variables.
|
||||
* Everything else has higher float, but always <=1. In fact, only a single variable has a level 1.
|
||||
*/
|
||||
float
|
||||
term_constrain_level (const Term term)
|
||||
{
|
||||
int vars;
|
||||
int structure;
|
||||
int flag;
|
||||
|
||||
int leaf (const Term t)
|
||||
{
|
||||
structure++;
|
||||
if (realTermVariable (t))
|
||||
vars++;
|
||||
return 1;
|
||||
}
|
||||
int nodel (const Term t)
|
||||
{
|
||||
structure++;
|
||||
return 1;
|
||||
}
|
||||
|
||||
if (term == NULL)
|
||||
error ("Cannot determine constrain level of empty term.");
|
||||
|
||||
vars = 0;
|
||||
structure = 0;
|
||||
flag = term_iterate_deVar (term, leaf, nodel, NULL, NULL);
|
||||
return ((float) vars / (float) structure);
|
||||
}
|
||||
|
||||
@ -175,5 +175,7 @@ int term_iterate_deVar (const Term term, int (*leaf) (), int (*nodel) (),
|
||||
int term_iterate_leaves (const Term t, int (*func) ());
|
||||
int term_iterate_open_leaves (const Term term, int (*func) ());
|
||||
void term_rolelocals_are_variables ();
|
||||
int term_encryption_level (const Term term);
|
||||
float term_constrain_level (const Term term);
|
||||
|
||||
#endif
|
||||
|
||||
@ -1,8 +1,10 @@
|
||||
/**
|
||||
* Temp file. I just forgot Warshall...
|
||||
*
|
||||
* Warshall's algorithm for transitive closure computation.
|
||||
*/
|
||||
|
||||
#include "warshall.h"
|
||||
#include "debug.h"
|
||||
|
||||
void
|
||||
graph_fill (int *graph, int nodes, int value)
|
||||
{
|
||||
@ -17,7 +19,8 @@ graph_fill (int *graph, int nodes, int value)
|
||||
}
|
||||
|
||||
//! Show a graph
|
||||
void graph_display (int *graph, int nodes)
|
||||
void
|
||||
graph_display (int *graph, int nodes)
|
||||
{
|
||||
int i;
|
||||
|
||||
@ -31,9 +34,9 @@ void graph_display (int *graph, int nodes)
|
||||
{
|
||||
int j;
|
||||
j = 0;
|
||||
while (j<nodes)
|
||||
while (j < nodes)
|
||||
{
|
||||
eprintf ("%i ", graph[index(i,j)]);
|
||||
eprintf ("%i ", graph[index (i, j)]);
|
||||
j++;
|
||||
}
|
||||
eprintf ("\n");
|
||||
@ -78,11 +81,20 @@ warshall (int *graph, int nodes)
|
||||
{
|
||||
if (graph[index (k, j)] == 1)
|
||||
{
|
||||
if (k == i)
|
||||
/**
|
||||
* Previously, we tested k == i (self-loop).
|
||||
* Now we test 2-node loops, i.e. wether there is also a path from i to k.
|
||||
*/
|
||||
if (graph[index (i, k)] > 0)
|
||||
{
|
||||
// Oh no! A cycle.
|
||||
graph [index (k,i)] = 2;
|
||||
graph_display (graph, nodes);
|
||||
graph[index (k, i)] = 2;
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
graph_display (graph, nodes);
|
||||
}
|
||||
#endif
|
||||
return 0;
|
||||
}
|
||||
graph[index (k, i)] = 1;
|
||||
|
||||
Loading…
Reference in New Issue
Block a user