andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- [[[ Broken commit. ]]]

Browse Source 
Stuff seems to be working again, slightly less efficient though (count
  states).
This commit is contained in:
ccremers 2006-02-27 16:08:17 +00:00
parent bb16bd755e
commit b49d13b6ee
12 changed files with 714 additions and 454 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

661
src/arachne.c
View File

@ -378,41 +378,48 @@ fixAgentKeylevels (void)
int
add_read_goals (const int run, const int old, const int new)
{
int count;
int i;
Roledef rd;
if (new <= sys->runs[run].height)
{
return 0;
}
else
{
int count;
int i;
Roledef rd;
sys->runs[run].height = new;
i = old;
rd = roledef_shift (sys->runs[run].start, i);
count = 0;
while (i < new && rd != NULL)
{
if (rd->type == READ)
sys->runs[run].height = new;
i = old;
rd = roledef_shift (sys->runs[run].start, i);
count = 0;
while (i < new && rd != NULL)
{
if (switches.output == PROOF)
if (rd->type == READ)
{
if (count == 0)
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Thus, we must also produce ");
if (count == 0)
{
indentPrint ();
eprintf ("Thus, we must also produce ");
}
else
{
eprintf (", ");
}
termPrint (rd->message);
}
else
{
eprintf (", ");
}
termPrint (rd->message);
count = count + goal_add (rd->message, run, i, 0);
}
count = count + goal_add (rd->message, run, i, 0);
rd = rd->next;
i++;
}
rd = rd->next;
i++;
if ((count > 0) && switches.output == PROOF)
{
eprintf ("\n");
}
return count;
}
if ((count > 0) && switches.output == PROOF)
{
eprintf ("\n");
}
return count;
}
//! Determine the run that follows from a substitution.
@ -756,114 +763,75 @@ getPriorityOfNeededKey (const System sys, const Term keyneeded)
return prioritylevel;
}
//! Try to bind a specific existing run to a goal.
//! Make a decryption chain from a binding to some run,index using the key list, and callback if this works.
/**
* 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 key goals are bound to the goal. Iterates on success.
* Callback return value is int, but is effectively ignored.
*/
void
bind_existing_to_goal (const Binding b, const int run, const int index)
createDecryptionChain (const Binding b, const int run, const int index,
Termlist keylist, int (*callback) (void))
{
int old_length;
int newgoals;
Term goalterm;
int subterm_unification_needs (Term tbig, const int r, const int e)
{
Term t;
void bind_iterate (Termlist tl)
if (keylist == NULL)
{
if (goal_bind (b, r, e))
// Immediate binding, no key needed.
if (goal_bind (b, run, index))
{
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Iterating for ");
termPrint (b->term);
eprintf (" to occur first in ");
termPrint (roledef_shift (sys->runs[run].start, index)->
message);
eprintf ("\n");
}
iterate ();
callback ();
goal_unbind (b);
return;
}
}
else
{
Term tdecr, tkey;
int smallrun;
t = deVar (b->term);
tbig = deVar (tbig);
// Some decryptor is needed for the term in the list
// First check whether it unifies in a simple way
unify (t, tbig, NULL, bind_iterate);
indentDepth++;
// The other options are unification on subparts
if (realTermTuple (tbig))
tdecr = keylist->term;
tkey = inverseKey (sys->know->inverses, TermKey (tdecr));
smallrun = create_decryptor (tdecr, tkey);
{
// Either one will do
subterm_unification_needs (TermOp1 (tbig), r, e);
subterm_unification_needs (TermOp1 (tbig), r, e);
}
if (realTermEncrypt (tbig))
{
Term keyneeded;
Roledef rddecrypt;
int smallrun;
int prioritylevel;
int newgoals;
Binding bnew;
int newgoals;
int prioritylevel;
/*
* 2. Add goal bindings
*/
indentDepth++;
// Maybe we can bind to the inner thing. Try.
// Add decryptor run
keyneeded = inverseKey (sys->know->inverses, TermKey (tbig));
prioritylevel = getPriorityOfNeededKey (sys, keyneeded);
smallrun = create_decryptor (tbig, keyneeded);
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 (tbig);
termPrint (tdecr);
eprintf (" to be decrypted using ");
termPrint (keyneeded);
termPrint (tkey);
eprintf ("\n");
}
/*
* 2. Add goal bindings
*/
newgoals = goal_add (rddecrypt->message, smallrun, 0, 0);
if (newgoals >= 0)
{
if (newgoals > 1)
{
error
("Added more than one goal for decryptor goal 1, weird.");
}
else
{
// This is the unique new goal then
bnew = (Binding) sys->bindings->data;
}
}
else
{
error ("No new binding added for inner message.");
// No new binding? Weird, but fair enough
bnew = NULL;
}
newgoals += goal_add (rddecrypt->next->message, smallrun, 1,
prioritylevel);
if (switches.output == PROOF)
{
indentPrint ();
eprintf
("To this end, we added two new goals and one new send: ");
@ -878,257 +846,122 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
/*
* 3. Bind open goal to decryptor?
*/
if (goal_bind (bnew, r, e))
if (goal_bind (b, smallrun, 2))
{
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Bound: trying new subterm_unfication_needs.\n");
eprintf ("Bound: trying new createDecryptionChain.\n");
}
subterm_unification_needs (TermOp (tbig), smallrun, 2);
goal_unbind (bnew);
// Iterate with the new goal
createDecryptionChain (bnew, run, index, keylist->next, callback);
goal_unbind (b);
}
/*
* clean up
*/
termDelete (keyneeded);
goal_remove_last (newgoals);
semiRunDestroy ();
indentDepth--;
}
}
semiRunDestroy ();
termDelete (tkey);
old_length = sys->runs[run].height;
if (index >= old_length)
{
newgoals = add_read_goals (run, old_length, index + 1);
indentDepth--;
}
else
{
newgoals = 0;
}
goalterm = roledef_shift (sys->runs[run].start, index)->message;
subterm_unification_needs (goalterm, run, index);
if (newgoals > 0)
{
goal_remove_last (newgoals);
}
sys->runs[run].height = old_length;
}
//! Try to bind a specific existing run to a goal.
/**
* The key goals are bound to the 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.
*
*@todo This is currently NOT correct. The point is that the key chain
* cannot uniquely define a path through a term in general, and
* a rewrite of termMguSubterm is needed. It should not yield the
* needed keys, but simply the path throught the term. This would enable
* reconstruction of the keys anyway. TODO
*
*@param b binding to fix (bind), destination filled in
*@param run run of binding start
*@param index index in run of binding start
* The key goals are bound to the goal. Iterates on success.
*/
int
bind_existing_to_goal_old (const Binding b, const int run, const int index)
void
bind_existing_to_goal (const Binding b, const int run, const int index)
{
Roledef rd;
int flag;
int old_length;
int newgoals;
int found;
Term bigterm;
int subterm_iterate (Termlist substlist, Termlist cryptlist)
int unifiesWithKeys (Termlist substlist, Termlist keylist)
{
int flag;
found++;
flag = 1;
/**
* Now create the new bindings
*/
int old_length;
int newgoals;
int newruns;
int stillvalid;
Binding smalltermbinding;
// We need some adapting because the height would increase; we therefore
// have to add read goals before we know whether it unifies.
old_length = sys->runs[run].height;
newgoals = add_read_goals (run, old_length, index + 1);
stillvalid = true; // New stuff is valid (no cycles)
newgoals = 0; // No new goals introduced (yet)
newruns = 0; // New runs introduced
smalltermbinding = b; // Start off with destination binding
{
// wrap substitution lists
indentDepth++;
#ifdef DEBUG
if (DEBUGL (4))
void wrapSubst (Termlist sl)
{
eprintf ("Trying to bind the small term ");
termPrint (b->term);
eprintf (" as coming from the big send ");
termPrint (rd->message);
eprintf (" , binding ");
termPrint (b->term);
eprintf ("\nCrypted list needed: ");
termlistPrint (cryptlist);
eprintf ("\n");
}
#endif
if (cryptlist != NULL && switches.output == PROOF)
{
indentPrint ();
eprintf
("This introduces the obligation to decrypt the following encrypted subterms: ");
termlistPrint (cryptlist);
eprintf ("\n");
}
/* The order of the cryptlist is inner -> outer */
while (stillvalid && cryptlist != NULL && smalltermbinding != NULL)
{
/*
* Invariants:
*
* smalltermbinding binding to be satisfied next (and for which a decryptor is needed)
*/
Term keyneeded;
int prioritylevel;
int smallrun;
int count;
Roledef rddecrypt;
Binding bnew;
int res;
/*
* 1. Add decryptor
*/
keyneeded =
inverseKey (sys->know->inverses, TermKey (cryptlist->term));
prioritylevel = getPriorityOfNeededKey (sys, keyneeded);
smallrun = create_decryptor (cryptlist->term, keyneeded);
rddecrypt = sys->runs[smallrun].start;
termDelete (keyneeded);
newruns++;
/*
* 2. Add goal bindings
*/
count = goal_add (rddecrypt->message, smallrun, 0, 0);
newgoals = newgoals + count;
if (count >= 0)
if (sl == NULL)
{
if (count > 1)
{
error
("Added more than one goal for decryptor goal 1, weird.");
}
else
{
// This is the unique new goal then
bnew = (Binding) sys->bindings->data;
}
// new create key goals, bind etc.
createDecryptionChain (b, run, index, keylist, iterate);
}
else
{
// No new binding? Weird, but fair enough
bnew = NULL;
}
newgoals =
newgoals + goal_add (rddecrypt->next->message, smallrun, 1,
prioritylevel);
int neworders;
int allgood;
/*
* 3. Bind open goal to decryptor
*/
// 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 t)
{
int r1, e1;
res = goal_bind (smalltermbinding, smallrun, 2); // returns 0 iff invalid
if (res != 0)
{
// Allright, good binding, proceed with next
smalltermbinding = bnew;
}
else
{
stillvalid = false;
}
r1 = TermRunid (t);
e1 = firstOccurrence (sys, r1, t, SEND);
if (dependPushEvent (r1, e1, run, index))
{
neworders++;
return true;
}
else
{
allgood = false;
return false;
}
}
/* progression */
cryptlist = cryptlist->next;
}
neworders = 0;
allgood = true;
iterateTermOther (run, sl->term, makeDepend);
/*
* Decryptors for any nested keys have been added. Now we can fill the
* final binding.
*/
if (stillvalid)
{
if (goal_bind (smalltermbinding, run, index))
{
proof_suppose_binding (b);
#ifdef DEBUG
if (DEBUGL (4))
if (allgood)
{
indentPrint ();
eprintf ("Added %i new goals, iterating.\n", newgoals);
wrapSubst (sl->next);
}
while (neworders > 0)
{
neworders--;
dependPopEvent ();
}
#endif
/* Iterate process */
indentDepth++;
flag = flag && iterate ();
indentDepth--;
goal_unbind (b);
}
else
{
proof_cannot_bind (b, run, index);
}
}
wrapSubst (substlist);
}
// undo
goal_remove_last (newgoals);
while (newruns > 0)
{
semiRunDestroy ();
newruns--;
}
indentDepth--;
return flag;
sys->runs[run].height = old_length;
return true;
}
//----------------------------
// Roledef entry
rd = roledef_shift (sys->runs[run].start, index);
// Fix length
old_length = sys->runs[run].height;
if ((index + 1) > old_length)
newgoals = add_read_goals (run, old_length, index + 1);
else
newgoals = 0;
// Bind to existing run
found = 0;
flag = termMguSubTerm (b->term, rd->message,
subterm_iterate, sys->know->inverses, NULL);
// Did it work?
if (found == 0 && switches.output == PROOF)
{
indentPrint ();
eprintf ("Cannot bind ");
termPrint (b->term);
eprintf (" to run %i, index %i because it does not subterm-unify.\n",
run, index);
}
// Reset length
goal_remove_last (newgoals);
sys->runs[run].height = old_length;
return flag;
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
int
bind_existing_run (const Binding b, const Protocol p, const Role r,
@ -1181,11 +1014,12 @@ bind_new_run (const Binding b, const Protocol p, const Role r,
const int index)
{
int run;
int newgoals;
run = semiRunCreate (p, r);
proof_suppose_run (run, 0, index + 1);
{
int newgoals;
newgoals = add_read_goals (run, 0, index + 1);
indentDepth++;
bind_existing_to_goal (b, run, index);
@ -1269,6 +1103,9 @@ printSemiState ()
}
//! 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)
{
@ -1339,7 +1176,36 @@ bind_goal_new_m0 (const Binding b)
termPrint (b->term);
eprintf (" from the initial knowledge.\n");
}
flag = flag && iterate ();
{
// Now we also want to add bindings to have this run before all other runs
void wrapRunOrders (const int otherrun)
{
if (otherrun < 0)
{
// No more runs to do
flag = flag && iterate ();
}
else
{
if (otherrun != run)
{
if (dependPushEvent (run, 0, otherrun, 0))
{
wrapRunOrders (otherrun - 1);
dependPopEvent ();
}
}
else
{
wrapRunOrders (otherrun - 1);
}
}
}
wrapRunOrders (sys->maxruns - 1);
}
goal_unbind (b);
}
else
@ -1389,10 +1255,6 @@ bind_goal_new_encrypt (const Binding b)
if (!realTermLeaf (term))
{
int run;
int index;
int newgoals;
Roledef rd;
Term t1, t2;
if (!realTermEncrypt (term))
@ -1407,40 +1269,53 @@ bind_goal_new_encrypt (const Binding b)
if (t2 != TERM_Hidden)
{
int run;
can_be_encrypted = 1;
run = semiRunCreate (INTRUDER, I_RRS);
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");
}
newgoals = add_read_goals (run, 0, index + 1);
{
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");
}
indentDepth++;
if (goal_bind (b, run, index))
{
proof_suppose_binding (b);
flag = flag && iterate ();
goal_unbind (b);
int newgoals;
newgoals = add_read_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);
}
else
{
proof_cannot_bind (b, run, index);
}
indentDepth--;
goal_remove_last (newgoals);
}
semiRunDestroy ();
}
}
@ -1456,7 +1331,6 @@ bind_goal_new_encrypt (const Binding b)
}
}
return flag;
}
@ -1637,7 +1511,7 @@ bind_goal_old_intruder_run (Binding b)
//! Bind a goal in all possible ways
int
bind_goal (const Binding b)
bind_goal_all_options (const Binding b)
{
if (b->blocked)
{
@ -2091,26 +1965,28 @@ iterate ()
{
if (!prune_bounds (sys))
{
Binding b;
Binding btup;
// Are there any tuple goals?
b = select_tuple_goal ();
if (b != NULL)
btup = select_tuple_goal ();
if (btup != NULL)
{
// Expand tuple goal
int count;
// mark as blocked for iteration
binding_block (b);
binding_block (btup);
// simply adding will detect the tuple and add the new subgoals
count = goal_add (b->term, b->run_to, b->ev_to, b->level);
count =
goal_add (btup->term, btup->run_to, btup->ev_to,
btup->level);
// Show this in output
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Expanding tuple goal ");
termPrint (b->term);
termPrint (btup->term);
eprintf (" into %i subgoals.\n", count);
}
@ -2119,7 +1995,7 @@ iterate ()
// undo
goal_remove_last (count);
binding_unblock (b);
binding_unblock (btup);
}
else
{
@ -2159,7 +2035,7 @@ iterate ()
/*
* bind this goal in all possible ways and iterate
*/
flag = bind_goal (b);
flag = bind_goal_all_options (b);
}
}
}
@ -2316,9 +2192,11 @@ arachne ()
{
// 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;
@ -2338,34 +2216,57 @@ arachne ()
eprintf (" at index %i.\n", cl->ev);
}
indentDepth++;
run = semiRunCreate (p, r);
proof_suppose_run (run, 0, cl->ev + 1);
add_read_goals (run, 0, cl->ev + 1);
/**
* Add specific goal info
*/
add_claim_specifics (sys, cl,
roledef_shift (sys->runs[run].start,
cl->ev));
newruns++;
{
int newgoals;
int realStart (void)
{
#ifdef DEBUG
if (DEBUGL (5))
{
printSemiState ();
}
if (DEBUGL (5))
{
printSemiState ();
}
#endif
iterate_buffer_attacks ();
//! Destroy
while (sys->bindings != NULL)
{
goal_remove_last (1);
return iterate_buffer_attacks ();
}
while (sys->maxruns > 0)
proof_suppose_run (run, 0, cl->ev + 1);
newgoals = add_read_goals (run, 0, cl->ev + 1);
/**
* Add specific goal info and iterate
*/
add_claim_specifics (sys, cl,
roledef_shift (sys->runs[run].start,
cl->ev), realStart);
goal_remove_last (newgoals);
}
//! 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--;

23
src/claim.c
View File

@ -739,12 +739,19 @@ prune_claim_specifics (const System sys)
return 0;
}
//! Setup system for specific claim test
void
add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd)
//! Setup system for specific claim test and iterate
int
add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd,
int (*callback) (void))
{
/*
* different cases
*/
if (cl->type == CLAIM_Secret)
{
int newgoals;
int flag;
/**
* Secrecy claim
*/
@ -764,7 +771,12 @@ add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd)
* be reached (without reaching the attack).
*/
cl->count = statesIncrease (cl->count);
goal_add (rd->message, 0, cl->ev, 0); // Assumption that all claims are in run 0
newgoals = goal_add (rd->message, 0, cl->ev, 0); // Assumption that all claims are in run 0
flag = callback ();
goal_remove_last (newgoals);
return flag;
}
if (cl->type == CLAIM_Reachable)
@ -779,7 +791,10 @@ add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd)
rolecount = termlistLength (protocol->rolenames);
switches.runs = rolecount;
}
return callback ();
}
return callback ();
}
//! Count a false claim

4
src/claim.h
View File

@ -9,8 +9,8 @@ int arachne_claim_nisynch (const System sys, const int claim_run,
const int claim_index);
int prune_claim_specifics (const System sys);
void add_claim_specifics (const System sys, const Claimlist cl, const
Roledef rd);
int add_claim_specifics (const System sys, const Claimlist cl, const
Roledef rd, int (*callback) (void));
void count_false_claim (const System sys);
int property_check (const System sys);

13
src/compiler.c
View File

@ -1427,10 +1427,10 @@ compute_prec_sets (const System sys)
r1 = 0;
while (r1 < sys->rolecount)
{
ev1 = 0;
while (ev1 < (sys->roleeventmax - 1))
ev1 = 1;
while (ev1 < (sys->roleeventmax))
{
SETBIT (prec + rowsize * index (r1, ev1), index (r1, ev1 + 1));
SETBIT (prec + rowsize * index (r1, ev1 - 1), index (r1, ev1));
ev1++;
}
r1++;
@ -1472,6 +1472,13 @@ compute_prec_sets (const System sys)
r1++;
}
#ifdef DEBUG
if (DEBUGL (5))
{
show_matrix ();
}
#endif
/*
* Compute transitive closure (Warshall).
*/

94
src/depend.c
View File

@ -40,6 +40,14 @@ struct depeventgraph
//! Pointer shorthard
typedef struct depeventgraph *Depeventgraph;
/*
* External
* ---------------------------------------------------------------
*/
extern Protocol INTRUDER; //!< The intruder protocol
extern Role I_M; //!< special role; precedes all other events always
/*
* Globals
* ---------------------------------------------------------------
@ -266,18 +274,12 @@ dependPopGeneric (void)
currentdepgraph = dgprev;
}
//! Construct graph dependencies from sys
/**
* uses currentdepgraph->sys
*/
// Dependencies from role order
void
dependFromSys (void)
dependDefaultRoleOrder (void)
{
int r;
List bl;
// There are two types of orderings.
// 1. Role orderings (within runs)
for (r = 0; r < currentdepgraph->sys->maxruns; r++)
{
int e;
@ -287,10 +289,14 @@ dependFromSys (void)
setDependEvent (r, e - 1, r, e);
}
}
}
// Dependencies fro bindings order
void
dependDefaultBindingOrder (void)
{
List bl;
// 2. Binding orderings
// We implicitly assume these cause no cycles (by construction this is
// correct)
for (bl = currentdepgraph->sys->bindings; bl != NULL; bl = bl->next)
{
Binding b;
@ -313,6 +319,17 @@ dependFromSys (void)
}
}
//! Construct graph dependencies from sys
/**
* uses currentdepgraph->sys
*/
void
dependFromSys (void)
{
dependDefaultRoleOrder ();
dependDefaultBindingOrder ();
}
//! Detect whether the graph has a cycle. If so, a node can get to itself (through the cycle)
int
hasCycle ()
@ -386,6 +403,9 @@ isDependEvent (const int r1, const int e1, const int r2, const int e2)
void
dependPushRun (const System sys)
{
#ifdef DEBUG
debug (5, "Push dependGraph for new run\n");
#endif
dependPushGeneric (dependCreate (sys));
dependFromSys ();
}
@ -401,6 +421,9 @@ dependPopRun (void)
globalError--;
error ("Trying to pop graph created for new binding.");
}
#ifdef DEBUG
debug (5, "Pop dependGraph for new run\n");
#endif
dependPopGeneric ();
}
@ -432,12 +455,21 @@ dependPushEvent (const int r1, const int e1, const int r2, const int e2)
else
{
// No immediate cycle: new graph, return true TODO disabled
if ((1 == 0) && ((r1 == r2) && (e1 == e2))
|| isDependEvent (r1, e1, r2, e2))
if ((1 == 1) && (((r1 == r2) && (e1 == e2))
|| isDependEvent (r1, e1, r2, e2)))
{
// if n->n or the binding already existed, no changes
// no change: add zombie
currentdepgraph->zombie += 1;
#ifdef DEBUG
debug (5, "Push dependGraph for new event (zombie push)\n");
if (DEBUGL (5))
{
globalError++;
eprintf ("r%ii%i --> r%ii%i\n", r1, e1, r2, e2);
globalError--;
}
#endif
}
else
{
@ -455,6 +487,15 @@ dependPushEvent (const int r1, const int e1, const int r2, const int e2)
dependPopEvent ();
return false;
}
#ifdef DEBUG
debug (5, "Push dependGraph for new event (real push)\n");
if (DEBUGL (5))
{
globalError++;
eprintf ("r%ii%i --> r%ii%i\n", r1, e1, r2, e2);
globalError--;
}
#endif
}
return true;
}
@ -464,22 +505,31 @@ dependPushEvent (const int r1, const int e1, const int r2, const int e2)
void
dependPopEvent (void)
{
if (currentdepgraph->fornewrun)
{
globalError++;
dependPrint ();
globalError--;
error ("Trying to pop graph created for new run.");
}
if (currentdepgraph->zombie > 0)
{
// zombie pushed
#ifdef DEBUG
debug (5, "Pop dependGraph for new event (zombie pop)\n");
#endif
currentdepgraph->zombie -= 1;
}
else
{
// real graph
dependPopGeneric ();
if (currentdepgraph->fornewrun)
{
globalError++;
dependPrint ();
globalError--;
error ("Trying to pop graph created for new run.");
}
else
{
// real graph
#ifdef DEBUG
debug (5, "Pop dependGraph for new event (real pop)\n");
#endif
dependPopGeneric ();
}
}
}

116
src/mgu.c
View File

@ -117,30 +117,36 @@ termlistSubstReset (Termlist tl)
* The callback receives a list of variables, that were previously open, but are now closed
* in such a way that the two terms unify.
*
* The callback must return true for the iteration to proceed: if it returns false, a single call would abort the scan.
* The return value shows this: it is false if the scan was aborted, and true if not.
*/
void
unify (Term t1, Term t2, Termlist tl, void (*callback) (Termlist))
int
unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
{
int proceed;
proceed = true;
/* added for speed */
t1 = deVar (t1);
t2 = deVar (t2);
if (t1 == t2)
{
callback (tl);
return;
return proceed && callback (tl);
}
int callsubst (Termlist tl, Term t, Term tsubst)
{
int proceed;
t->subst = tsubst;
#ifdef DEBUG
showSubst (t);
#endif
tl = termlistAdd (tl, t);
callback (tl);
proceed = callback (tl);
tl = termlistDelTerm (tl);
t->subst = NULL;
return;
return proceed;
}
if (!(hasTermVariable (t1) || hasTermVariable (t2)))
@ -149,13 +155,12 @@ unify (Term t1, Term t2, Termlist tl, void (*callback) (Termlist))
if (isTermEqual (t1, t2))
{
// Equal!
callback (tl);
return;
return proceed && callback (tl);
}
else
{
// Can never be fixed, no variables
return;
return proceed;
}
}
@ -183,8 +188,7 @@ unify (Term t1, Term t2, Termlist tl, void (*callback) (Termlist))
t1 = t2;
t2 = t3;
}
callsubst (tl, t1, t2);
return;
return proceed && callsubst (tl, t1, t2);
}
/* symmetrical tests for single variable.
@ -193,61 +197,115 @@ unify (Term t1, Term t2, Termlist tl, void (*callback) (Termlist))
if (realTermVariable (t2))
{
if (termSubTerm (t1, t2) || !goodsubst (t2, t1))
return;
return proceed;
else
{
callsubst (tl, t2, t1);
return;
return proceed && callsubst (tl, t2, t1);
}
}
if (realTermVariable (t1))
{
if (termSubTerm (t2, t1) || !goodsubst (t1, t2))
return;
return proceed;
else
{
callsubst (tl, t1, t2);
return;
return proceed && callsubst (tl, t1, t2);
}
}
/* left & right are compounds with variables */
if (t1->type != t2->type)
return;
return proceed;
/* identical compound types */
/* encryption first */
if (realTermEncrypt (t1))
{
void unify_combined_enc (Termlist tl)
int unify_combined_enc (Termlist tl)
{
// now the keys are unified (subst in this tl)
// and we try the inner terms
unify (TermOp (t1), TermOp (t2), tl, callback);
return;
return unify (TermOp (t1), TermOp (t2), tl, callback);
}
unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc);
return;
return proceed
&& unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc);
}
/* tupling second
non-associative version ! TODO other version */
if (isTermTuple (t1))
{
void unify_combined_tup (Termlist tl)
int unify_combined_tup (Termlist tl)
{
// now the keys are unified (subst in this tl)
// and we try the inner terms
unify (TermOp2 (t1), TermOp2 (t2), tl, callback);
return;
return unify (TermOp2 (t1), TermOp2 (t2), tl, callback);
}
unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup);
return;
return proceed
&& unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup);
}
return;
return proceed;
}
//! Subterm unification
/**
* Try to unify (a subterm of) tbig with tsmall.
*
* Callback is called with a list of substitutions, and a list of terms that
* need to be decrypted in order for this to work.
*
* E.g. subtermUnify ( {{m}k1}k2, m ) yields a list : {{m}k1}k2, {m}k1 (where
* the {m}k1 is the last added node to the list)
*
* The callback should return true for the iteration to proceed, or false to abort.
* The final result is this flag.
*/
int
subtermUnify (Term tbig, Term tsmall, Termlist tl, Termlist keylist,
int (*callback) (Termlist, Termlist))
{
int proceed;
int keycallback (Termlist tl)
{
return callback (tl, keylist);
}
proceed = true;
// Devar
tbig = deVar (tbig);
tsmall = deVar (tsmall);
// Three options:
// 1. simple unification
proceed = proceed && unify (tbig, tsmall, tl, keycallback);
// [2/3]: complex
// 2. interm unification
if (realTermTuple (tbig))
{
proceed = proceed
&& subtermUnify (TermOp1 (tbig), tsmall, tl, keylist, callback);
proceed = proceed
&& subtermUnify (TermOp2 (tbig), tsmall, tl, keylist, callback);
}
// 3. unification with encryption needed
if (realTermEncrypt (tbig))
{
// extend the keylist
keylist = termlistAdd (keylist, tbig);
proceed = proceed
&& subtermUnify (TermOp (tbig), tsmall, tl, keylist, callback);
// remove last item again
keylist = termlistDelTerm (keylist);
}
return proceed;
}

6
src/mgu.h
View File

@ -20,6 +20,10 @@ int termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist));
int termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
Termlist inverses, Termlist keylist);
void termlistSubstReset (Termlist tl);
void unify (Term t1, Term t2, Termlist tl, void (*callback) (Termlist));
// The new iteration methods
int unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist));
int
subtermUnify (Term tbig, Term tsmall, Termlist tl, Termlist keylist,
int (*callback) (Termlist, Termlist));
#endif

52
src/prune_theorems.c
View File

@ -17,6 +17,53 @@ extern Protocol INTRUDER;
extern int proofDepth;
extern int max_encryption_level;
//! Check locals occurrence
/*
* Returns true if the order is correct
*/
int
correctLocalOrder (const System sys)
{
int checkRun (int r1)
{
int checkTerm (Term t)
{
if (!isTermVariable (t))
{
int r2;
int e1, e2;
// t is a term from r2 that occurs in r1
r2 = TermRunid (t);
e1 = firstOccurrence (sys, r1, t, READ);
e2 = firstOccurrence (sys, r2, t, SEND);
// thus, it should not be the case that e1 occurs before e2
if (isDependEvent (r1, e1, r2, e2))
{
// That's not good!
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Pruned because ordering for term ");
termPrint (t);
eprintf
(" cannot be correct: the first send r%ii%i occurs after the read r%ii%i.\n",
r2, e2, r1, e1);
}
return false;
}
}
return true;
}
return iterateLocalToOther (sys, r1, checkTerm);
}
return iterateRegularRuns (sys, checkRun);
}
//! Check initiator roles
/**
* Returns false iff an agent type is wrong
@ -232,6 +279,11 @@ prune_theorems (const System sys)
}
}
/*
* Check for correct orderings involving local constants
*/
correctLocalOrder (sys);
/**
* Check whether the bindings are valid
*/

140
src/system.c
View File

@ -30,6 +30,9 @@ int globalLatex;
//! Global count of protocols
int protocolCount;
//! External
extern Protocol INTRUDER;
//! Switch for indent or not.
static int indentState = 0;
//! Current indent depth.
@ -1513,3 +1516,140 @@ enoughAttacks (const System sys)
}
return 0;
}
//! Iterate over runs.
/**
* Callback should return true in order to continue.
*/
int
iterateRuns (const System sys, int (*callback) (int r))
{
int r;
for (r = 0; r < sys->maxruns; r++)
{
if (!callback (r))
{
return false;
}
}
return true;
}
//! Iterate over non-intruder runs.
/**
* Callback should return true in order to continue.
*/
int
iterateRegularRuns (const System sys, int (*callback) (int r))
{
int regular (int r)
{
if (sys->runs[r].protocol != INTRUDER)
{
return callback (r);
}
return true;
}
return iterateRuns (sys, regular);
}
// Iterate over events in a certain run (increasing through role)
int
iterateEvents (const System sys, const int run,
int (*callback) (Roledef rd, int ev))
{
int e;
Roledef rd;
rd = sys->runs[run].start;
for (e = 0; e < sys->runs[run].step; e++)
{
if (!callback (rd, e))
{
return false;
}
rd = rd->next;
}
return true;
}
// Iterate over event type in a certain run (increasing through role)
int
iterateEventsType (const System sys, const int run, const int evtype,
int (*callback) (Roledef rd, int ev))
{
int selectEvent (Roledef rd, int e)
{
if (rd->type == evtype)
{
return callback (rd, e);
}
return true;
}
return iterateEvents (sys, run, selectEvent);
}
// Iterate over all 'others': local variables of a run that are instantiated and contain some term of another run.
int
iterateLocalToOther (const System sys, const int myrun,
int (*callback) (Term t))
{
Termlist tlo, tls;
int addOther (Term t)
{
tlo = termlistAddNew (tlo, t);
return true;
}
tlo = NULL;
// construct all others occuring in the reads
for (tls = sys->runs[myrun].locals; tls != NULL; tls = tls->next)
{
iterateTermOther (myrun, tls->term, addOther);
}
// now iterate over all of them
for (tls = tlo; tls != NULL; tls = tls->next)
{
if (!callback (tls->term))
{
return false;
}
}
// clean up
termlistDelete (tlo);
return true;
}
//! Get first read/send occurrence (event index) of term t in run r
int
firstOccurrence (const System sys, const int r, Term t, int evtype)
{
int firste;
int checkOccurs (Roledef rd, int e)
{
if (termSubTerm (rd->message, t) || termSubTerm (rd->from, t)
|| termSubTerm (rd->to, t))
{
firste = e;
return false;
}
return true;
}
if (iterateEventsType (sys, r, evtype, checkOccurs))
{
globalError++;
eprintf ("Desired term ");
termPrint (t);
eprintf (" does not occur.\n");
globalError--;
error ("(in run %i in event type %i.)", r, evtype);
}
return firste;
}

11
src/system.h
View File

@ -224,6 +224,17 @@ int isAgentTrusted (const System sys, Term agent);
int isAgentlistTrusted (const System sys, Termlist agents);
int isRunTrusted (const System sys, const int run);
int iterateRuns (const System sys, int (*callback) (int r));
int iterateRegularRuns (const System sys, int (*callback) (int r));
int iterateEvents (const System sys, const int run,
int (*callback) (Roledef rd, int ev));
int iterateEventsType (const System sys, const int run, const int evtype,
int (*callback) (Roledef rd, int ev));
int iterateLocalToOther (const System sys, const int myrun,
int (*callback) (Term t));
int firstOccurrence (const System sys, const int r, Term t, int evtype);
//! Equality for run structure naming
/**
* For the modelchecker, there was an index called step. In Strand Space

33
src/term.c
View File

@ -925,8 +925,8 @@ termOrder (Term t1, Term t2)
//! Generic term iteration
int
term_iterate (const Term term, int (*leaf) (), int (*nodel) (),
int (*nodem) (), int (*noder) ())
term_iterate (const Term term, int (*leaf) (Term t), int (*nodel) (Term t),
int (*nodem) (Term t), int (*noder) (Term t))
{
if (term != NULL)
{
@ -977,8 +977,8 @@ term_iterate (const Term term, int (*leaf) (), int (*nodel) (),
//! Generic term iteration
int
term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
int (*nodem) (), int (*noder) ())
term_iterate_deVar (Term term, int (*leaf) (Term t), int (*nodel) (Term t),
int (*nodem) (Term t), int (*noder) (Term t))
{
term = deVar (term);
if (term != NULL)
@ -1045,7 +1045,7 @@ term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
* well. It is up to func to decide wether or not to recurse.
*/
int
term_iterate_leaves (const Term term, int (*func) ())
term_iterate_leaves (const Term term, int (*func) (Term t))
{
if (term != NULL)
{
@ -1069,13 +1069,13 @@ term_iterate_leaves (const Term term, int (*func) ())
//! Iterate over open leaves (i.e. respect variable closure)
int
term_iterate_open_leaves (const Term term, int (*func) ())
term_iterate_open_leaves (const Term term, int (*func) (Term t))
{
int testleaf (const Term t)
{
if (substVar (t))
{
return term_iterate_open_leaves (t, func);
return term_iterate_open_leaves (t->subst, func);
}
else
{
@ -1427,3 +1427,22 @@ termHidelevel (const Term tsmall, Term tbig)
}
}
}
// Iterate over subterm constants of other runs in a term
// Callback should return true to progress. This is reported in the final thing.
int
iterateTermOther (const int myrun, Term t, int (*callback) (Term t))
{
int testOther (Term t)
{
int run;
run = TermRunid (t);
if (run >= 0 && run != myrun)
{
return callback (t);
}
return true;
}
return term_iterate_deVar (t, testOther, NULL, NULL, NULL);
}

15
src/term.h
View File

@ -186,12 +186,14 @@ Term tupleProject (Term tt, int n);
int termSize (Term t);
float termDistance (Term t1, Term t2);
int termOrder (Term t1, Term t2);
int term_iterate (const Term term, int (*leaf) (), int (*nodel) (),
int (*nodem) (), int (*noder) ());
int term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
int (*nodem) (), int (*noder) ());
int term_iterate_leaves (const Term t, int (*func) ());
int term_iterate_open_leaves (const Term term, int (*func) ());
int term_iterate (const Term term, int (*leaf) (Term t),
int (*nodel) (Term t), int (*nodem) (Term t),
int (*noder) (Term t));
int term_iterate_deVar (Term term, int (*leaf) (Term t),
int (*nodel) (Term t), int (*nodem) (Term t),
int (*noder) (Term t));
int term_iterate_leaves (const Term t, int (*func) (Term t));
int term_iterate_open_leaves (const Term term, int (*func) (Term t));
void term_rolelocals_are_variables ();
int term_encryption_level (const Term term);
float term_constrain_level (const Term term);
@ -203,5 +205,6 @@ int isTermFunctionName (Term t);
Term getTermFunction (Term t);
unsigned int termHidelevel (const Term tsmall, Term tbig);
int iterateTermOther (const int myrun, Term t, int (*callback) (Term t));
#endif