- Single claim check branched.
This commit is contained in:
ccremers
parent
ff87bf180f
commit
92a98a85cc
276
src/arachne.c
276
src/arachne.c
@ -2231,6 +2231,147 @@ iterate_buffer_attacks (void)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
//! Arachne single claim
|
||||||
|
int
|
||||||
|
arachneClaim (Claimlist cl)
|
||||||
|
{
|
||||||
|
// Skip the dummy claims
|
||||||
|
if (!isTermEqual (cl->type, CLAIM_Empty))
|
||||||
|
{
|
||||||
|
// Any other claims might be filterered
|
||||||
|
if (switches.filterClaim == NULL || switches.filterClaim == cl->type)
|
||||||
|
{
|
||||||
|
// Some claims are always true!
|
||||||
|
if (!cl->alwaystrue)
|
||||||
|
{
|
||||||
|
// 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_read_goals (run, 0, cl->ev + 1);
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Add initial knowledge node
|
||||||
|
*/
|
||||||
|
{
|
||||||
|
Termlist m0tl;
|
||||||
|
Term m0t;
|
||||||
|
int m0run;
|
||||||
|
|
||||||
|
m0tl = knowledgeSet (sys->know);
|
||||||
|
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;
|
||||||
|
|
||||||
|
{
|
||||||
|
/**
|
||||||
|
* Add specific goal info and iterate algorithm
|
||||||
|
*/
|
||||||
|
add_claim_specifics (sys, cl,
|
||||||
|
roledef_shift (sys->runs[run].
|
||||||
|
start, cl->ev),
|
||||||
|
realStart);
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
// 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");
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
//! Main code for Arachne
|
//! Main code for Arachne
|
||||||
/**
|
/**
|
||||||
* For this test, we manually set up some stuff.
|
* For this test, we manually set up some stuff.
|
||||||
@ -2241,6 +2382,7 @@ int
|
|||||||
arachne ()
|
arachne ()
|
||||||
{
|
{
|
||||||
Claimlist cl;
|
Claimlist cl;
|
||||||
|
int count;
|
||||||
|
|
||||||
int print_send (Protocol p, Role r, Roledef rd, int index)
|
int print_send (Protocol p, Role r, Roledef rd, int index)
|
||||||
{
|
{
|
||||||
@ -2304,145 +2446,21 @@ arachne ()
|
|||||||
indentDepth = 0;
|
indentDepth = 0;
|
||||||
proofDepth = 0;
|
proofDepth = 0;
|
||||||
cl = sys->claimlist;
|
cl = sys->claimlist;
|
||||||
|
count = 0;
|
||||||
while (cl != NULL)
|
while (cl != NULL)
|
||||||
{
|
{
|
||||||
/**
|
/**
|
||||||
* Check each claim
|
* Check each claim
|
||||||
*/
|
*/
|
||||||
|
if (arachneClaim (cl))
|
||||||
// Skip the dummy claims
|
|
||||||
if (!isTermEqual (cl->type, CLAIM_Empty))
|
|
||||||
{
|
{
|
||||||
// Any other claims might be filterered
|
count++;
|
||||||
if (switches.filterClaim == NULL
|
|
||||||
|| switches.filterClaim == cl->type)
|
|
||||||
{
|
|
||||||
// Some claims are always true!
|
|
||||||
if (!cl->alwaystrue)
|
|
||||||
{
|
|
||||||
// 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_read_goals (run, 0, cl->ev + 1);
|
|
||||||
|
|
||||||
/**
|
|
||||||
* Add initial knowledge node
|
|
||||||
*/
|
|
||||||
{
|
|
||||||
Termlist m0tl;
|
|
||||||
Term m0t;
|
|
||||||
int m0run;
|
|
||||||
|
|
||||||
m0tl = knowledgeSet (sys->know);
|
|
||||||
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;
|
|
||||||
|
|
||||||
{
|
|
||||||
/**
|
|
||||||
* Add specific goal info and iterate algorithm
|
|
||||||
*/
|
|
||||||
add_claim_specifics (sys, cl,
|
|
||||||
roledef_shift (sys->runs[run].
|
|
||||||
start, cl->ev),
|
|
||||||
realStart);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
// 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");
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
// next
|
// next
|
||||||
cl = cl->next;
|
cl = cl->next;
|
||||||
}
|
}
|
||||||
|
return count;
|
||||||
}
|
}
|
||||||
|
|
||||||
//! Construct knowledge set at some event, based on a semitrace.
|
//! Construct knowledge set at some event, based on a semitrace.
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user