- Works better all the time. Huge shift of main logic. Much better.
This commit is contained in:
ccremers 2004-08-18 15:46:33 +00:00
parent b2d21f0a8a
commit 341f519bbb
4 changed files with 107 additions and 51 deletions

View File

@ -1,4 +1,5 @@
/** /**
*
*@file arachne.c *@file arachne.c
* *
* Introduces a method for proofs akin to the Athena modelchecker * Introduces a method for proofs akin to the Athena modelchecker
@ -34,6 +35,7 @@ Role I_V;
Role I_R; Role I_R;
Role I_E; Role I_E;
Role I_D; Role I_D;
Role I_RRS;
static int indentDepth; static int indentDepth;
static int max_encryption_level; static int max_encryption_level;
@ -112,7 +114,7 @@ arachneInit (const System mysys)
add_event (READ, NULL); add_event (READ, NULL);
add_event (READ, NULL); add_event (READ, NULL);
add_event (SEND, NULL); add_event (SEND, NULL);
I_D = add_role ("I_D: Decrypt"); I_RRS = add_role ("I_D: Encrypt");
return; return;
} }
@ -354,7 +356,6 @@ bind_existing_to_goal (const Binding b, const int index, const int run,
goal_remove_last (); goal_remove_last ();
keycount--; keycount--;
} }
termlistDestroy (keylist);
} }
else else
{ {
@ -553,13 +554,17 @@ select_goal ()
b = (Binding) bl->data; b = (Binding) bl->data;
if (!b->done) if (!b->done)
{ {
float cons; // We don't care about singular variables, so...
if (!isTermVariable (b->term))
cons = term_constrain_level (b->term);
if (cons < min_constrain)
{ {
min_constrain = cons; float cons;
best = b;
cons = term_constrain_level (b->term);
if (cons < min_constrain)
{
min_constrain = cons;
best = b;
}
} }
} }
bl = bl->next; bl = bl->next;
@ -572,7 +577,7 @@ select_goal ()
* Handles the case where the intruder constructs a composed term himself. * Handles the case where the intruder constructs a composed term himself.
*/ */
int int
bind_intruder_to_construct (const Binding b) bind_goal_new_intruder_run (const Binding b)
{ {
Term term; Term term;
Termlist m0tl; Termlist m0tl;
@ -588,40 +593,50 @@ bind_intruder_to_construct (const Binding b)
*/ */
if (!realTermLeaf (term)) if (!realTermLeaf (term))
{ {
int run;
int index;
int newgoals;
Roledef rd;
Term t1, t2; Term t1, t2;
if (realTermTuple (term)) if (realTermTuple (term))
{ {
warning ("Goal that is a tuple should not occur!");
// tuple construction // tuple construction
t1 = term->left.op1; error ("Goal that is a tuple should not occur!");
t2 = term->right.op2;
}
else
{
// must be encryption
t1 = term->left.op;
t2 = term->right.key;
} }
goal_add (t1, b->run_to, b->ev_to); // must be encryption
goal_add (t2, b->run_to, b->ev_to); t1 = term->left.op;
t2 = term->right.key;
roleInstance (sys, INTRUDER, I_RRS, NULL, NULL);
run = sys->maxruns - 1;
rd = sys->runs[run].start;
rd->message = termDuplicate (t1);
rd->next->message = termDuplicate (t2);
rd->next->next->message = termDuplicate (term);
index = 2;
newgoals = add_read_goals (run, 0, index+1);
#ifdef DEBUG #ifdef DEBUG
if (DEBUGL (3)) if (DEBUGL (3))
{ {
indentPrint (); indentPrint ();
eprintf ("Constructing "); eprintf ("Encrypting ");
termPrint (term); termPrint (term);
eprintf (" from smaller terms "); eprintf (" using term ");
termPrint (t1); termPrint (t1);
eprintf (" and "); eprintf (" and key ");
termPrint (t2); termPrint (t2);
eprintf ("\n"); eprintf ("\n");
} }
#endif #endif
flag = flag && iterate (); if (goal_bind (b, run, index))
goal_remove_last (); {
goal_remove_last (); flag = flag && iterate ();
}
goal_unbind (b);
remove_read_goals (newgoals);
roleInstanceDestroy (sys);
} }
/** /**
* 2. Constructed from bigger term and decryption key * 2. Constructed from bigger term and decryption key
@ -713,7 +728,7 @@ bind_intruder_to_construct (const Binding b)
//! Bind a regular goal //! Bind a regular goal
int int
bind_goal_regular (const Binding b) bind_goal_regular_run (const Binding b)
{ {
int flag; int flag;
@ -728,6 +743,12 @@ bind_goal_regular (const Binding b)
return 0; return 0;
} }
if (p == INTRUDER)
{
// No intruder roles here
return 1;
}
// Test for interm unification // Test for interm unification
#ifdef DEBUG #ifdef DEBUG
if (DEBUGL (5)) if (DEBUGL (5))
@ -761,11 +782,8 @@ bind_goal_regular (const Binding b)
#endif #endif
// Bind to existing run // Bind to existing run
flag = bind_existing_run (b, p, r, index, 1); flag = bind_existing_run (b, p, r, index, 1);
if (p != INTRUDER) // bind to new run
{ flag = flag && bind_new_run (b, p, r, index, 1);
// No intruder: bind to new run
flag = flag && bind_new_run (b, p, r, index, 1);
}
return flag; return flag;
} }
else else
@ -775,7 +793,7 @@ bind_goal_regular (const Binding b)
} }
} }
// Bind to all possible sends or intruder node; // Bind to all possible sends of regular runs
#ifdef DEBUG #ifdef DEBUG
if (DEBUGL (5)) if (DEBUGL (5))
{ {
@ -783,32 +801,60 @@ bind_goal_regular (const Binding b)
eprintf ("Try regular role send.\n"); eprintf ("Try regular role send.\n");
} }
#endif #endif
flag = iterate_role_sends (bind_this_role_send); return iterate_role_sends (bind_this_role_send);
}
// Bind to all possible sends of intruder runs
int bind_goal_old_intruder_run (Binding b)
{
int run;
int flag;
#ifdef DEBUG #ifdef DEBUG
if (DEBUGL (5)) if (DEBUGL (5))
{ {
indentPrint (); indentPrint ();
eprintf ("Try intruder send.\n"); eprintf ("Try regular intruder send.\n");
} }
#endif #endif
// Other option: bind to term construction flag = 1;
for (run = 0; run < sys->maxruns; run++)
{
if (sys->runs[run].protocol == INTRUDER)
{
int ev;
Roledef rd;
flag = flag && bind_intruder_to_construct (b); rd = sys->runs[run].start;
ev = 0;
// Return result while (ev < sys->runs[run].length)
{
if (rd->type == SEND)
{
flag = flag && bind_existing_to_goal (b, ev, run, 1);
}
rd = rd->next;
ev++;
}
}
}
return flag; return flag;
} }
//! Bind a goal in all possible ways //! Bind a goal in all possible ways
int int
bind_goal (const Binding b) bind_goal (const Binding b)
{ {
if (!b->done) if (!b->done)
{ {
return bind_goal_regular (b); int flag;
flag = bind_goal_regular_run (b);
flag = flag && bind_goal_old_intruder_run (b);
flag = flag && bind_goal_new_intruder_run (b);
return flag;
} }
else else
{ {

View File

@ -226,6 +226,14 @@ void
goal_add (Term term, const int run, const int ev) goal_add (Term term, const int run, const int ev)
{ {
term = deVar (term); term = deVar (term);
#ifdef DEBUG
if (term == NULL)
error ("Trying to add an emtpy goal term");
if (run >= sys->maxruns)
error ("Trying to add a goal for a run that does not exist.");
if (ev >= sys->runs[run].step)
error ("Trying to add a goal for an event that is not in the semistate yet.");
#endif
if (realTermTuple (term)) if (realTermTuple (term))
{ {
int width; int width;
@ -280,6 +288,10 @@ goal_bind (const Binding b, const int run, const int ev)
{ {
if (!b->done) if (!b->done)
{ {
#ifdef DEBUG
if (run >= sys->maxruns || sys->runs[run].step <= ev)
error ("Trying to bind to something not yet in the semistate.");
#endif
b->done = 1; b->done = 1;
b->run_from = run; b->run_from = run;
b->ev_from = ev; b->ev_from = ev;
@ -326,7 +338,7 @@ bindings_c_minimal ()
if (!warshall (graph, nodes)) if (!warshall (graph, nodes))
{ {
// Hmm, cycle // Hmm, cycle
return 0; error ("Detected a cycle when testing for c-minimality");
} }
} }
@ -344,12 +356,12 @@ bindings_c_minimal ()
node_from = node_number (b->run_from, b->ev_from); node_from = node_number (b->run_from, b->ev_from);
// Find all preceding events // Find all preceding events
for (run = 0; run <= sys->maxruns; run++) for (run = 0; run < sys->maxruns; run++)
{ {
int ev; int ev;
//!@todo hardcoded reference to step, should be length //!@todo hardcoded reference to step, should be length
for (ev = 0; run < sys->runs[run].step; ev++) for (ev = 0; ev < sys->runs[run].step; ev++)
{ {
int node_comp; int node_comp;
@ -360,7 +372,7 @@ bindings_c_minimal ()
Roledef rd; Roledef rd;
rd = roledef_shift (sys->runs[run].start, ev); rd = roledef_shift (sys->runs[run].start, ev);
if (termInTerm (rd->message, b->term)) if (termInTerm (b->term, rd->message))
{ {
// This term already occurs as interm in a previous node! // This term already occurs as interm in a previous node!
return 0; return 0;

View File

@ -1092,6 +1092,8 @@ term_constrain_level (const Term term)
int nodel (const Term t) int nodel (const Term t)
{ {
structure++; structure++;
if (realTermTuple (t))
structure++;
return 1; return 1;
} }

View File

@ -81,11 +81,7 @@ warshall (int *graph, int nodes)
{ {
if (graph[index (k, j)] == 1) 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. // Oh no! A cycle.
graph[index (k, i)] = 2; graph[index (k, i)] = 2;