diff --git a/src/arachne.c b/src/arachne.c index 25fef0d..934843f 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -37,6 +37,7 @@ #include "dotout.h" #include "prune_bounds.h" #include "prune_theorems.h" +#include "arachne.h" extern int *graph; extern int nodes; @@ -62,15 +63,6 @@ static int prevIndentDepth; static int indentDepthChanges; static FILE *attack_stream; -struct goalstruct -{ - int run; - int index; - Roledef rd; -}; - -typedef struct goalstruct Goal; - /** * Forward declarations */ @@ -505,71 +497,6 @@ countIntruderActions () return count; } -//! Check this variables whether it is a good agent type -/** - * Checks for leaf/etc and correct agent type - */ -int -goodAgentType (Term agent) -{ - agent = deVar (agent); - - if (!realTermLeaf (agent)) - { // not a leaf - return false; - } - else - { // real leaf - if (isTermVariable (agent)) - { - // Variable: check type consistency (should have a solution) - // Not yet: depends on matching mode also - } - else - { - // Constant: allow only exact type - if (!inTermlist (agent->stype, TERM_Agent)) - { - return false; - } - } - } - - return true; -} - -//! Check initiator roles -/** - * Returns false iff an agent type is wrong - */ -int -initiatorAgentsType () -{ - int run; - - run = 0; - while (run < sys->maxruns) - { - // Only for initiators - if (sys->runs[run].role->initiator) - { - Termlist agents; - - agents = sys->runs[run].agents; - while (agents != NULL) - { - if (!goodAgentType (agents->term)) - { - return false; - } - agents = agents->next; - } - } - run++; - } - return true; // seems to be okay -} - //------------------------------------------------------------------------ // Proof reporting //------------------------------------------------------------------------ @@ -1080,234 +1007,6 @@ bind_new_run (const Binding b, const Protocol p, const Role r, return flag; } -//! Convert a list of ranks to a list of lines (0..) -/** - * The interesting bit is that the ranks include the intruder events. Thus, we need to filter those out of - * the system. - * - * Returns the baseline of the highest number + 1; thus the number of lines. - */ -int -ranks_to_lines (int *ranks, const int nodes) -{ - int ranksdone, baseline; - - ranksdone = 0; // All values lower than this have been done, so it is the next value - baseline = 0; // The line numbers that get assigned - while (1) - { - int newlow; - int run; - int i; - - // Determine lowest rank for non-intruder events, that has not been done - newlow = INT_MAX; - run = 0; - while (run < sys->maxruns) - { - if (sys->runs[run].protocol != INTRUDER) - { - int ev; - - ev = 0; - while (ev < sys->runs[run].step) - { - int nrank; - - nrank = ranks[node_number (run, ev)]; - if (nrank < newlow && nrank >= ranksdone) - { - newlow = nrank; - } - ev++; - } - } - run++; - } - if (newlow == INT_MAX) - { - // All are done - return baseline; - } - // Convert the nodes between ranksdone and newlow to baseline - i = 0; - while (i < nodes) - { - if (ranks[i] <= newlow && ranks[i] >= ranksdone) - { - ranks[i] = baseline; - } - i++; - } - baseline++; - ranksdone = newlow + 1; - } -} - - -//! Iterate over all events that have an incoming arrow to the current one (forgetting the intruder for a moment) -void -iterate_incoming_arrows (void (*func) (), const int run, const int ev) -{ - /** - * Determine wheter to draw an incoming arrow to this event. - * We check all other runs, to see if they are ordered. - */ - int run2; - - run2 = 0; - while (run2 < sys->maxruns) - { - if (run2 != run && sys->runs[run2].protocol != INTRUDER) - { - // Is this run before the event? - int ev2; - int found; - - found = 0; - ev2 = sys->runs[run2].length; - while (found == 0 && ev2 > 0) - { - ev2--; - if (graph[graph_nodes (nodes, run2, ev2, run, ev)] != 0) - { - found = 1; - } - } - - if (found == 1) - { - // It is before the event, and thus we would like to draw it. - // However, if there is another path along which we can get here, forget it - /** - * Note that this algorithm is similar to Floyd's algorithm for all shortest paths. - * The goal here is to select only the path with distance 1 (as viewed from the regular runs), - * so we can simplify stuff a bit. - * Nevertheless, using Floyd first would probably be faster. - */ - int other_route; - int run3; - int ev3; - - other_route = 0; - run3 = 0; - ev3 = 0; - while (other_route == 0 && run3 < sys->maxruns) - { - if (sys->runs[run3].protocol != INTRUDER) - { - ev3 = 0; - while (other_route == 0 && ev3 < sys->runs[run3].length) - { - if (graph - [graph_nodes - (nodes, run2, ev2, run3, ev3)] != 0 - && - graph[graph_nodes - (nodes, run3, ev3, run, ev)] != 0) - { - // other route found - other_route = 1; - } - ev3++; - } - } - run3++; - } - if (other_route == 0) - { - func (run2, ev2); - } - - - } - } - run2++; - } -} - -//! Iterate over all events that have an outgoing arrow from the current one (forgetting the intruder for a moment) -void -iterate_outgoing_arrows (void (*func) (), const int run, const int ev) -{ - /** - * Determine wheter to draw an incoming arrow to this event. - * We check all other runs, to see if they are ordered. - */ - int run2; - - run2 = 0; - while (run2 < sys->maxruns) - { - if (run2 != run && sys->runs[run2].protocol != INTRUDER) - { - // Is this run after the event? - int ev2; - int found; - - found = 0; - ev2 = 0; - while (found == 0 && ev2 < sys->runs[run2].length) - { - if (graph[graph_nodes (nodes, run, ev, run2, ev2)] != 0) - { - found = 1; - } - else - { - ev2++; - } - } - - if (found == 1) - { - // It is after the event, and thus we would like to draw it. - // However, if there is another path along which we can get there, forget it - /** - * Note that this algorithm is similar to Floyd's algorithm for all shortest paths. - * The goal here is to select only the path with distance 1 (as viewed from the regular runs), - * so we can simplify stuff a bit. - * Nevertheless, using Floyd first would probably be faster. - */ - int other_route; - int run3; - int ev3; - - other_route = 0; - run3 = 0; - ev3 = 0; - while (other_route == 0 && run3 < sys->maxruns) - { - if (sys->runs[run3].protocol != INTRUDER) - { - ev3 = 0; - while (other_route == 0 && ev3 < sys->runs[run3].length) - { - if (graph - [graph_nodes - (nodes, run, ev, run3, ev3)] != 0 - && - graph[graph_nodes - (nodes, run3, ev3, run2, ev2)] != 0) - { - // other route found - other_route = 1; - } - ev3++; - } - } - run3++; - } - if (other_route == 0) - { - func (run2, ev2); - } - } - } - run2++; - } -} - //! Print the current semistate void printSemiState () @@ -1866,17 +1565,6 @@ bind_goal (const Binding b) } } -//! Count a false claim -/** - * Counts global attacks as well as claim instances. - */ -void -count_false () -{ - sys->attackid++; - sys->current_claim->failed = statesIncrease (sys->current_claim->failed); -} - //! Create a generic new term of the same type, with a new run identifier. /** * Output: the first element of the returned list. @@ -1917,6 +1605,10 @@ createNewTermGeneric (Termlist tl, Term t) //! Create a new term with incremented run rumber, starting at sys->maxruns. /** + * This is a rather intricate function that tries to generate new terms of a + * certain type. It first looks up things in the initial knowledge, checking + * whether they are used already. After that, new ones are generated. + * * Output: the first element of the returned list. */ Termlist @@ -1961,6 +1653,9 @@ createNewTerm (Termlist tl, Term t, int isagent) } //! Delete a term made in the previous constructions +/** + * \sa createNewTerm + */ void deleteNewTerm (Term t) { @@ -1974,6 +1669,12 @@ deleteNewTerm (Term t) } //! Make a trace concrete +/** + * People find reading variables in attack outputs difficult. + * Thus, we instantiate them in a sensible way to make things more readable. + * + * \sa makeTraceClass + */ Termlist makeTraceConcrete (const System sys) { @@ -2028,6 +1729,9 @@ makeTraceConcrete (const System sys) } //! Make a trace a class again +/** + * \sa makeTraceConcrete + */ void makeTraceClass (const System sys, Termlist varlist) { @@ -2136,43 +1840,6 @@ arachneOutputAttack () // Main logic core //------------------------------------------------------------------------ -//! Check properties -int -property_check () -{ - int flag; - int cost; - - flag = 1; - - /* Do we need any? */ - if (enoughAttacks (sys)) - return flag; - - /** - * By the way the claim is handled, this automatically means a flaw. - */ - count_false (); - if (switches.output == ATTACK) - { - arachneOutputAttack (); - } - // Store attack cost if cheaper - cost = attackCost (sys); - if (cost < attack_leastcost) - { - // Cheapest attack - attack_leastcost = cost; - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("New cheaper attack found with cost %i.\n", cost); - } - } - - return flag; -} - //! Selector to select the first tuple goal. /** @@ -2279,7 +1946,7 @@ iterate () sys->claims = statesIncrease (sys->claims); sys->current_claim->count = statesIncrease (sys->current_claim->count); - flag = property_check (); + flag = property_check (sys); } else { diff --git a/src/arachne.h b/src/arachne.h index ff5c29c..f6ae052 100644 --- a/src/arachne.h +++ b/src/arachne.h @@ -12,8 +12,14 @@ int isTriviallyKnownAtArachne (const System sys, const Term t, const int run, const int index); int isTriviallyKnownAfterArachne (const System sys, const Term t, const int run, const int index); -int ranks_to_lines (int *ranks, const int nodes); -void iterate_incoming_arrows (void (*func) (), const int run, const int ev); -void iterate_outgoing_arrows (void (*func) (), const int run, const int ev); + +struct goalstruct +{ + int run; + int index; + Roledef rd; +}; + +typedef struct goalstruct Goal; #endif diff --git a/src/claim.c b/src/claim.c index e56c5ab..a3157d6 100644 --- a/src/claim.c +++ b/src/claim.c @@ -17,6 +17,7 @@ #include "arachne.h" #include "specialterm.h" #include "switches.h" +#include "memory.h" #define MATCH_NONE 0 #define MATCH_ORDER 1 @@ -27,6 +28,7 @@ #define LABEL_TODO -2 extern int globalError; +extern int attack_leastcost; // Debugging the NI-SYNCH checks //#define OKIDEBUG @@ -772,3 +774,52 @@ add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd) } } } + +//! Count a false claim +/** + * Counts global attacks as well as claim instances. + */ +void +count_false_claim (const System sys) +{ + sys->attackid++; + sys->current_claim->failed = statesIncrease (sys->current_claim->failed); +} + + +//! Check properties +int +property_check (const System sys) +{ + int flag; + int cost; + + flag = 1; + + /* Do we need any? */ + if (enoughAttacks (sys)) + return flag; + + /** + * By the way the claim is handled, this automatically means a flaw. + */ + count_false_claim (sys); + if (switches.output == ATTACK) + { + arachneOutputAttack (); + } + // Store attack cost if cheaper + cost = attackCost (sys); + if (cost < attack_leastcost) + { + // Cheapest attack + attack_leastcost = cost; + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("New cheaper attack found with cost %i.\n", cost); + } + } + + return flag; +} diff --git a/src/claim.h b/src/claim.h index bf5ee71..26f2da2 100644 --- a/src/claim.h +++ b/src/claim.h @@ -11,5 +11,7 @@ int arachne_claim_nisynch (const System sys, const int claim_run, int prune_claim_specifics (const System sys); void add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd); +void count_false_claim (const System sys); +int property_check (const System sys); #endif diff --git a/src/dotout.c b/src/dotout.c index ce9b404..764041d 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -17,6 +17,171 @@ extern Role I_RRSD; #define isBound(rd) (rd->bound) #define length step +//! Iterate over all events that have an incoming arrow to the current one (forgetting the intruder for a moment) +void +iterate_incoming_arrows (const System sys, void (*func) (), const int run, + const int ev) +{ + /** + * Determine wheter to draw an incoming arrow to this event. + * We check all other runs, to see if they are ordered. + */ + int run2; + + run2 = 0; + while (run2 < sys->maxruns) + { + if (run2 != run && sys->runs[run2].protocol != INTRUDER) + { + // Is this run before the event? + int ev2; + int found; + + found = 0; + ev2 = sys->runs[run2].length; + while (found == 0 && ev2 > 0) + { + ev2--; + if (graph[graph_nodes (nodes, run2, ev2, run, ev)] != 0) + { + found = 1; + } + } + + if (found == 1) + { + // It is before the event, and thus we would like to draw it. + // However, if there is another path along which we can get here, forget it + /** + * Note that this algorithm is similar to Floyd's algorithm for all shortest paths. + * The goal here is to select only the path with distance 1 (as viewed from the regular runs), + * so we can simplify stuff a bit. + * Nevertheless, using Floyd first would probably be faster. + */ + int other_route; + int run3; + int ev3; + + other_route = 0; + run3 = 0; + ev3 = 0; + while (other_route == 0 && run3 < sys->maxruns) + { + if (sys->runs[run3].protocol != INTRUDER) + { + ev3 = 0; + while (other_route == 0 && ev3 < sys->runs[run3].length) + { + if (graph + [graph_nodes + (nodes, run2, ev2, run3, ev3)] != 0 + && + graph[graph_nodes + (nodes, run3, ev3, run, ev)] != 0) + { + // other route found + other_route = 1; + } + ev3++; + } + } + run3++; + } + if (other_route == 0) + { + func (run2, ev2); + } + + + } + } + run2++; + } +} + +//! Iterate over all events that have an outgoing arrow from the current one (forgetting the intruder for a moment) +void +iterate_outgoing_arrows (const System sys, void (*func) (), const int run, + const int ev) +{ + /** + * Determine wheter to draw an incoming arrow to this event. + * We check all other runs, to see if they are ordered. + */ + int run2; + + run2 = 0; + while (run2 < sys->maxruns) + { + if (run2 != run && sys->runs[run2].protocol != INTRUDER) + { + // Is this run after the event? + int ev2; + int found; + + found = 0; + ev2 = 0; + while (found == 0 && ev2 < sys->runs[run2].length) + { + if (graph[graph_nodes (nodes, run, ev, run2, ev2)] != 0) + { + found = 1; + } + else + { + ev2++; + } + } + + if (found == 1) + { + // It is after the event, and thus we would like to draw it. + // However, if there is another path along which we can get there, forget it + /** + * Note that this algorithm is similar to Floyd's algorithm for all shortest paths. + * The goal here is to select only the path with distance 1 (as viewed from the regular runs), + * so we can simplify stuff a bit. + * Nevertheless, using Floyd first would probably be faster. + */ + int other_route; + int run3; + int ev3; + + other_route = 0; + run3 = 0; + ev3 = 0; + while (other_route == 0 && run3 < sys->maxruns) + { + if (sys->runs[run3].protocol != INTRUDER) + { + ev3 = 0; + while (other_route == 0 && ev3 < sys->runs[run3].length) + { + if (graph + [graph_nodes + (nodes, run, ev, run3, ev3)] != 0 + && + graph[graph_nodes + (nodes, run3, ev3, run2, ev2)] != 0) + { + // other route found + other_route = 1; + } + ev3++; + } + } + run3++; + } + if (other_route == 0) + { + func (run2, ev2); + } + } + } + run2++; + } +} + //! Display the current semistate using dot output format. /** * This is not as nice as we would like it. Furthermore, the function is too big, and needs to be split into functional parts that @@ -326,7 +491,7 @@ dotSemiState (const System sys) } incoming_arrow_count = 0; - iterate_incoming_arrows (incoming_arrow, run, ev); + iterate_incoming_arrows (sys, incoming_arrow, run, ev); /* * Currently disabled: generates too much garbage */ diff --git a/src/prune_theorems.c b/src/prune_theorems.c index b419dd6..c51a56f 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -17,6 +17,38 @@ extern Protocol INTRUDER; extern int proofDepth; extern int max_encryption_level; +//! Check initiator roles +/** + * Returns false iff an agent type is wrong + */ +int +initiatorAgentsType (const System sys) +{ + int run; + + run = 0; + while (run < sys->maxruns) + { + // Only for initiators + if (sys->runs[run].role->initiator) + { + Termlist agents; + + agents = sys->runs[run].agents; + while (agents != NULL) + { + if (!goodAgentType (agents->term)) + { + return false; + } + agents = agents->next; + } + } + run++; + } + return true; // seems to be okay +} + //! Prune determination because of theorems /** * When something is pruned because of this function, the state space is still @@ -112,7 +144,7 @@ prune_theorems (const System sys) } // Prune wrong agents type for initators - if (!initiatorAgentsType ()) + if (!initiatorAgentsType (sys)) { if (switches.output == PROOF) { diff --git a/src/type.c b/src/type.c index 9212ec5..1e70dfe 100644 --- a/src/type.c +++ b/src/type.c @@ -444,3 +444,36 @@ checkAllSubstitutions (const System sys) termlistDelete (groundvars); return allvalid; } + +//! Check this variables whether it is a good agent type +/** + * Checks for leaf/etc and correct agent type + */ +int +goodAgentType (Term agent) +{ + agent = deVar (agent); + + if (!realTermLeaf (agent)) + { // not a leaf + return false; + } + else + { // real leaf + if (isTermVariable (agent)) + { + // Variable: check type consistency (should have a solution) + // Not yet: depends on matching mode also + } + else + { + // Constant: allow only exact type + if (!inTermlist (agent->stype, TERM_Agent)) + { + return false; + } + } + } + + return true; +} diff --git a/src/type.h b/src/type.h index 91a5929..88ee607 100644 --- a/src/type.h +++ b/src/type.h @@ -10,5 +10,6 @@ int checkTypeLocals (const System sys); Termlist typelistConjunct (Termlist typelist1, Termlist Typelist2); int checkAllSubstitutions (const System sys); int isAgentType (Termlist typelist); +int goodAgentType (Term agent); #endif