- Lots of stuff starts to take shape. Nice.
This commit is contained in:
ccremers
parent
f30207b059
commit
2191d80885
209
src/arachne.c
209
src/arachne.c
@ -7,24 +7,41 @@
|
||||
*/
|
||||
|
||||
#include "term.h"
|
||||
#include "termlist.h"
|
||||
#include "role.h"
|
||||
#include "system.h"
|
||||
#include "states.h"
|
||||
#include "mgu.h"
|
||||
#include "arachne.h"
|
||||
|
||||
Term INTRUDER_ROLE;
|
||||
static System sys;
|
||||
static Protocol INTRUDER; // Pointers, to be set by the Init
|
||||
static Role I_GOAL; // Same here.
|
||||
|
||||
struct goalstruct
|
||||
{
|
||||
int run;
|
||||
int index;
|
||||
Roledef rd;
|
||||
};
|
||||
|
||||
typedef struct goalstruct Goal;
|
||||
|
||||
/**
|
||||
* Forward declarations
|
||||
*/
|
||||
|
||||
int iterate ();
|
||||
|
||||
/**
|
||||
* Program code
|
||||
*/
|
||||
|
||||
//! Init Arachne engine
|
||||
void
|
||||
arachneInit (const System sys)
|
||||
arachneInit (const System mysys)
|
||||
{
|
||||
sys = mysys; // make sys available for this module as a global
|
||||
/*
|
||||
* Add intruder protocol roles
|
||||
*/
|
||||
@ -33,7 +50,7 @@ arachneInit (const System sys)
|
||||
|
||||
//! Close Arachne engine
|
||||
void
|
||||
arachneDone (const System sys)
|
||||
arachneDone ()
|
||||
{
|
||||
return;
|
||||
}
|
||||
@ -47,14 +64,73 @@ arachneDone (const System sys)
|
||||
* call it 'length' here.
|
||||
*/
|
||||
#define INVALID -1
|
||||
#define isGoal(rd) (rd->type == READ)
|
||||
#define isGoal(rd) (rd->type == READ && !rd->internal)
|
||||
#define isBound(rd) (rd->bind_run != INVALID)
|
||||
#define length step
|
||||
|
||||
//! Iterate but discard the info of the termlist
|
||||
int
|
||||
mgu_iterate (const Termlist tl)
|
||||
{
|
||||
return iterate ();
|
||||
}
|
||||
|
||||
|
||||
//------------------------------------------------------------------------
|
||||
// Sub
|
||||
//------------------------------------------------------------------------
|
||||
|
||||
//! 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)
|
||||
{
|
||||
int flag;
|
||||
|
||||
flag = func (p, r, rd, index);
|
||||
if (!flag)
|
||||
return 0;
|
||||
}
|
||||
index++;
|
||||
rd = rd->next;
|
||||
}
|
||||
r = r->next;
|
||||
}
|
||||
p = p->next;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
//! Generates a new intruder goal, yields runid
|
||||
int
|
||||
add_intruder_goal (Term t)
|
||||
{
|
||||
roleInstance (sys, INTRUDER, I_GOAL, NULL);
|
||||
return (sys->maxruns - 1);
|
||||
}
|
||||
|
||||
//------------------------------------------------------------------------
|
||||
// Larger logical componentents
|
||||
//------------------------------------------------------------------------
|
||||
@ -64,19 +140,20 @@ arachneDone (const System sys)
|
||||
* Should be ordered to prefer most constrained; for now, it is simply the first one encountered.
|
||||
*/
|
||||
Goal
|
||||
select_goal (const System sys)
|
||||
select_goal ()
|
||||
{
|
||||
Goal goal;
|
||||
int run;
|
||||
|
||||
goal.run = INVALID;
|
||||
goal.rd = NULL;
|
||||
for (run = 0; run < sys->maxruns; run++)
|
||||
{
|
||||
Roledef rd;
|
||||
int index;
|
||||
|
||||
index = 0;
|
||||
rd = runPointerGet (sys, run);
|
||||
rd = sys->runs[run].start;
|
||||
while (rd != NULL && index < sys->runs[run].length)
|
||||
{
|
||||
if (isGoal (rd) && !isBound (rd))
|
||||
@ -84,6 +161,7 @@ select_goal (const System sys)
|
||||
// Return this goal
|
||||
goal.run = run;
|
||||
goal.index = index;
|
||||
goal.rd = rd;
|
||||
return goal;
|
||||
}
|
||||
index++;
|
||||
@ -93,29 +171,114 @@ select_goal (const System sys)
|
||||
return goal;
|
||||
}
|
||||
|
||||
//! Bind a goal to an existing regular run, if possible
|
||||
int
|
||||
bind_existing_run (const Goal goal, const Protocol p, const Role r,
|
||||
const int index)
|
||||
{
|
||||
int run, flag;
|
||||
|
||||
flag = 1;
|
||||
for (run = 0; run < sys->maxruns; run++)
|
||||
{
|
||||
if (sys->runs[run].protocol == p && sys->runs[run].role == r)
|
||||
{
|
||||
int i;
|
||||
int old_length;
|
||||
Roledef rd;
|
||||
|
||||
// find roledef entry
|
||||
rd = sys->runs[run].start;
|
||||
for (i = 0; i < index; i++)
|
||||
rd = rd->next;
|
||||
|
||||
// mgu and iterate
|
||||
old_length = sys->runs[run].length;
|
||||
if (index >= old_length)
|
||||
sys->runs[run].length = index + 1;
|
||||
flag =
|
||||
flag & termMguInTerm (goal.rd->message, rd->message, mgu_iterate);
|
||||
sys->runs[run].length = old_length;
|
||||
}
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
|
||||
//! Bind a goal to a new run
|
||||
int
|
||||
bind_new_run (const Goal goal, const Protocol p, const Role r,
|
||||
const int index)
|
||||
{
|
||||
}
|
||||
|
||||
//! Bind a regular goal
|
||||
int
|
||||
bind_goal_regular (const System sys, const Goal goal)
|
||||
bind_goal_regular (const Goal goal)
|
||||
{
|
||||
int flag;
|
||||
|
||||
/*
|
||||
* This is a local function so we have access to goal
|
||||
*/
|
||||
int bind_this (Protocol p, Role r, Roledef rd, int index)
|
||||
{
|
||||
int element_f1 (Termlist substlist)
|
||||
{
|
||||
/**
|
||||
* Two options; as this, it is from an existing run,
|
||||
* or from a new one.
|
||||
*/
|
||||
int flag;
|
||||
|
||||
termlistSubstReset (substlist); // undo, we don't really need that
|
||||
flag = bind_existing_run (goal, p, r, index);
|
||||
if (flag)
|
||||
{
|
||||
flag = bind_new_run (goal, p, r, index);
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
|
||||
// Test for interm unification
|
||||
return termMguInTerm (goal.rd->message, rd->message, element_f1);
|
||||
}
|
||||
|
||||
// Bind to all possible sends?
|
||||
flag = iterate_role_sends (bind_this);
|
||||
// Bind to an intruder node?
|
||||
if (flag)
|
||||
{
|
||||
int run;
|
||||
|
||||
goal.rd->bind_run = add_intruder_goal (goal.rd->message); // creates a new run
|
||||
goal.rd->bind_index = 0; // such a run only has a simple read;
|
||||
|
||||
flag = iterate ();
|
||||
|
||||
roleInstanceDestroy (sys); // destroy the created run
|
||||
goal.rd->bind_run = INVALID;
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
|
||||
//! Bind an intruder goal
|
||||
int
|
||||
bind_goal_intruder (const System sys, const Goal goal)
|
||||
bind_goal_intruder (const Goal goal)
|
||||
{
|
||||
//!@todo Fix intruder goal stuff
|
||||
}
|
||||
|
||||
//! Bind a goal in all possible ways
|
||||
int
|
||||
bind_goal (const System sys, const Goal goal)
|
||||
bind_goal (const Goal goal)
|
||||
{
|
||||
if (isTermEqual (sys->runs[goal.run].protocol->nameterm, INTRUDER_ROLE))
|
||||
if (sys->runs[goal.run].protocol == INTRUDER)
|
||||
{
|
||||
return bind_goal_intruder (sys, goal);
|
||||
return bind_goal_intruder (goal);
|
||||
}
|
||||
else
|
||||
{
|
||||
return bind_goal_regular (sys, goal);
|
||||
return bind_goal_regular (goal);
|
||||
}
|
||||
}
|
||||
|
||||
@ -124,7 +287,7 @@ bind_goal (const System sys, const Goal goal)
|
||||
*@returns true iff this state is invalid for some reason
|
||||
*/
|
||||
int
|
||||
prune (const System sys)
|
||||
prune ()
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
@ -135,7 +298,7 @@ prune (const System sys)
|
||||
|
||||
//! Main recursive procedure for Arachne
|
||||
int
|
||||
iterate (const System sys)
|
||||
iterate ()
|
||||
{
|
||||
Goal goal;
|
||||
|
||||
@ -143,14 +306,20 @@ iterate (const System sys)
|
||||
* Possibly prune this state
|
||||
*/
|
||||
|
||||
if (prune (sys))
|
||||
if (prune ())
|
||||
return 0;
|
||||
|
||||
/**
|
||||
* If not pruned, check whether its a final state (i.e. all goals bound)
|
||||
* Not pruned: count
|
||||
*/
|
||||
|
||||
goal = select_goal (sys);
|
||||
sys->states = statesIncrease (sys->states);
|
||||
|
||||
/**
|
||||
* Check whether its a final state (i.e. all goals bound)
|
||||
*/
|
||||
|
||||
goal = select_goal ();
|
||||
if (goal.run == INVALID)
|
||||
{
|
||||
/*
|
||||
@ -163,7 +332,7 @@ iterate (const System sys)
|
||||
/*
|
||||
* bind this goal in all possible ways and iterate
|
||||
*/
|
||||
return bind_goal (sys, goal);
|
||||
return bind_goal (goal);
|
||||
}
|
||||
}
|
||||
|
||||
@ -172,7 +341,7 @@ iterate (const System sys)
|
||||
* For this test, we manually set up some stuff.
|
||||
*/
|
||||
int
|
||||
arachne (const System sys)
|
||||
arachne ()
|
||||
{
|
||||
/*
|
||||
* set up claim role(s)
|
||||
@ -181,5 +350,5 @@ arachne (const System sys)
|
||||
/*
|
||||
* iterate
|
||||
*/
|
||||
iterate (sys);
|
||||
iterate ();
|
||||
}
|
||||
|
||||
@ -4,7 +4,7 @@
|
||||
#include "system.h"
|
||||
|
||||
void arachneInit (const System sys);
|
||||
void arachneDone (const System sys);
|
||||
int arachne (const System sys);
|
||||
void arachneDone ();
|
||||
int arachne ();
|
||||
|
||||
#endif
|
||||
|
||||
@ -542,7 +542,7 @@ main (int argc, char **argv)
|
||||
|
||||
if (sys->engine == ARACHNE_ENGINE)
|
||||
{
|
||||
arachneInit ();
|
||||
arachneInit (sys);
|
||||
}
|
||||
/*
|
||||
* ---------------------------------------
|
||||
@ -912,7 +912,7 @@ modelCheck (const System sys)
|
||||
traverse (sys);
|
||||
break;
|
||||
case ARACHNE_ENGINE:
|
||||
arachne (sys);
|
||||
arachne ();
|
||||
break;
|
||||
default:
|
||||
error ("Unknown engine type %i.", sys->engine);
|
||||
|
||||
39
src/mgu.c
39
src/mgu.c
@ -163,49 +163,59 @@ termMguTerm (Term t1, Term t2)
|
||||
//! Most general interm unifiers of t1 interm t2
|
||||
/**
|
||||
* Try to determine the most general interm unifiers of two terms.
|
||||
*@returns Nothing. Iteration gets void.
|
||||
*@returns Nothing. Iteration gets termlist of substitutions.
|
||||
*/
|
||||
void
|
||||
termMguInTerm (Term t1, Term t2, void (*iterator) ())
|
||||
int
|
||||
termMguInTerm (Term t1, Term t2, int (*iterator) ())
|
||||
{
|
||||
Termlist tl;
|
||||
int flag;
|
||||
|
||||
flag = 1;
|
||||
t2 = deVar (t2);
|
||||
if (t2 != NULL && isTermTuple (t2))
|
||||
{
|
||||
// t2 is a tuple, consider interm options as well.
|
||||
termMguInTerm (t1, t2->left.op1, iterator);
|
||||
termMguInTerm (t1, t2->right.op2, iterator);
|
||||
flag = flag & termMguInTerm (t1, t2->left.op1, iterator);
|
||||
flag = flag & termMguInTerm (t1, t2->right.op2, iterator);
|
||||
}
|
||||
// simple clause or combined
|
||||
tl = termMguTerm (t1, t2);
|
||||
if (tl != MGUFAIL)
|
||||
{
|
||||
// Iterate
|
||||
iterator ();
|
||||
flag = flag & iterator (tl);
|
||||
// Reset variables
|
||||
termlistSubstReset (tl);
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
|
||||
//! Most general subterm unifiers of t1 subterm t2
|
||||
/**
|
||||
* Try to determine the most general subterm unifiers of two terms.
|
||||
*@returns Nothing. Iteration gets list of keys needed to decrypt.
|
||||
*@returns Nothing. Iteration gets termlist of subst, and list of keys needed to decrypt.
|
||||
*/
|
||||
void
|
||||
termMguSubTerm (Term t1, Term t2, void (*iterator) (),
|
||||
int
|
||||
termMguSubTerm (Term t1, Term t2, int (*iterator) (),
|
||||
const Termlist inverses, Termlist keylist)
|
||||
{
|
||||
int flag;
|
||||
Termlist tl;
|
||||
|
||||
flag = 1;
|
||||
t2 = deVar (t2);
|
||||
if (t2 != NULL && !isTermLeaf (t2))
|
||||
{
|
||||
if (isTermTuple (t2))
|
||||
{
|
||||
// 'simple' tuple
|
||||
termMguSubTerm (t1, t2->left.op1, iterator, inverses, keylist);
|
||||
termMguSubTerm (t1, t2->right.op2, iterator, inverses, keylist);
|
||||
flag =
|
||||
flag & termMguSubTerm (t1, t2->left.op1, iterator, inverses,
|
||||
keylist);
|
||||
flag =
|
||||
flag & termMguSubTerm (t1, t2->right.op2, iterator, inverses,
|
||||
keylist);
|
||||
}
|
||||
else
|
||||
{
|
||||
@ -219,7 +229,9 @@ termMguSubTerm (Term t1, Term t2, void (*iterator) (),
|
||||
keylist_new = termlistAdd (keylist_new, newkey);
|
||||
|
||||
// Recurse
|
||||
termMguSubTerm (t1, t2->left.op, iterator, inverses, keylist_new);
|
||||
flag =
|
||||
flag & termMguSubTerm (t1, t2->left.op, iterator, inverses,
|
||||
keylist_new);
|
||||
|
||||
termlistDelete (keylist_new);
|
||||
termDelete (newkey);
|
||||
@ -230,8 +242,9 @@ termMguSubTerm (Term t1, Term t2, void (*iterator) (),
|
||||
if (tl != MGUFAIL)
|
||||
{
|
||||
// Iterate
|
||||
iterator (keylist);
|
||||
flag = flag & iterator (tl, keylist);
|
||||
// Reset variables
|
||||
termlistSubstReset (tl);
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
|
||||
@ -15,8 +15,9 @@
|
||||
#define MGUFAIL (Termlist) -1
|
||||
|
||||
Termlist termMguTerm (Term t1, Term t2);
|
||||
void termMguInTerm (Term t1, Term t2, void (*iterator) ());
|
||||
void termMguSubTerm (Term t1, Term t2, void (*iterator) (),
|
||||
const Termlist inverses, Termlist keylist);
|
||||
int termMguInTerm (Term t1, Term t2, int (*iterator) ());
|
||||
int termMguSubTerm (Term t1, Term t2, int (*iterator) (),
|
||||
const Termlist inverses, Termlist keylist);
|
||||
void termlistSubstReset (Termlist tl);
|
||||
|
||||
#endif
|
||||
|
||||
Loading…
Reference in New Issue
Block a user