diff --git a/src/arachne.c b/src/arachne.c index 8d4661c..c155d13 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -33,6 +33,7 @@ #include "type.h" #include "switches.h" #include "specialterm.h" +#include "cost.h" extern int *graph; extern int nodes; @@ -40,6 +41,7 @@ extern int graph_uordblks; static System sys; static int attack_length; +static int attack_leastcost; Protocol INTRUDER; // Pointers, to be set by the Init Role I_M; // Same here. @@ -3194,14 +3196,25 @@ prune_bounds () } // Limit on exceeding any attack length - if (switches.prune == 2 && get_semitrace_length () >= attack_length) + if (get_semitrace_length () >= attack_length) { + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned: attack length %i.\n", attack_length); + } + return 1; + } + + /* prune for cheaper */ + if (switches.prune == 2 && attack_leastcost <= attackCost (sys)) + { + // We already had an attack at least this cheap. if (switches.output == PROOF) { indentPrint (); eprintf - ("Pruned: we already know an attack of length %i.\n", - attack_length); + ("Pruned: attack cost exceeds a previously found attack.\n"); } return 1; } @@ -3584,7 +3597,7 @@ int property_check () { int flag; - int attack_this; + int cost; flag = 1; @@ -3600,17 +3613,16 @@ property_check () { arachneOutputAttack (); } - // Store attack length if shorter - attack_this = get_semitrace_length (); - if (attack_this < attack_length) + // Store attack cost if cheaper + cost = attackCost (sys); + if (cost < attack_leastcost) { - // Shortest attack - attack_length = attack_this; + // Cheapest attack + attack_leastcost = cost; if (switches.output == PROOF) { indentPrint (); - eprintf ("New shortest attack found with trace length %i.\n", - attack_length); + eprintf ("New cheaper attack found with cost %i.\n", cost); } } @@ -3855,6 +3867,7 @@ arachne () sys->current_claim = cl; attack_length = INT_MAX; + attack_leastcost = INT_MAX; cl->complete = 1; p = (Protocol) cl->protocol; r = (Role) cl->role; diff --git a/src/cost.c b/src/cost.c new file mode 100644 index 0000000..8cfc2d5 --- /dev/null +++ b/src/cost.c @@ -0,0 +1,90 @@ +/** + * + *@file cost.c + * + * Determine cost of a given semitrace in sys + * Constructed for Arachne results, unreliable otherwise. + * + */ +#include "switches.h" + +//************************************************************************ +// Private methods +//************************************************************************ + +int selfInitiator(const System sys, const int run) +{ + int self_initiator; + + self_initiator = false; + if (sys->runs[run].role->initiator) + { + // An initiator + Termlist agents; + Termlist seen; + + agents = sys->runs[run].agents; + seen = NULL; + while (agents != NULL) + { + Term agent; + + agent = agents->term; + if (inTermlist (seen, agent)) + { + // This agent was already in the seen list + self_initiator = true; + } + else + { + termlistAdd (seen, agent); + } + agents = agents->next; + } + termlistDelete (seen); + } + return self_initiator; +} + +//! Count the number of any self-initiators +int selfInitiators(const System sys) +{ + int count; + int run; + + count = 0; + run = 0; + while (run < sys->maxruns) + { + if (selfInitiator (sys, run)) + { + count++; + } + run++; + } + return count; +} + +//************************************************************************ +// Public methods +//************************************************************************ + +//! Determine cost of an attack +/* + * This should also work on uncompleted semitraces, and should be monotonous + * (i.e. further iterations should increase the cost only) so that it can be + * used for branch and bound. + * + * A lower value (closer to 0) is a more feasible attack. + */ +int attackCost(const System sys) +{ + int cost; + + cost = 0; + + cost += get_semitrace_length(); + cost += 5 * selfInitiators(sys); + + return cost; +} diff --git a/src/cost.h b/src/cost.h new file mode 100644 index 0000000..f660e44 --- /dev/null +++ b/src/cost.h @@ -0,0 +1,6 @@ +#ifndef COST +#define COST + +int attackCost(const System sys); + +#endif