diff --git a/src/arachne.c b/src/arachne.c index f925a2a..6fe2612 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -35,27 +35,31 @@ #include "specialterm.h" #include "cost.h" #include "dotout.h" +#include "prune_bounds.h" +#include "prune_theorems.h" extern int *graph; extern int nodes; extern int graph_uordblks; static System sys; -static int attack_length; -static int attack_leastcost; + +int attack_length; +int attack_leastcost; Protocol INTRUDER; // Pointers, to be set by the Init Role I_M; // Same here. Role I_RRS; Role I_RRSD; +int proofDepth; +int max_encryption_level; +int num_regular_runs; +int num_intruder_runs; + static int indentDepth; static int prevIndentDepth; static int indentDepthChanges; -static int proofDepth; -static int max_encryption_level; -static int num_regular_runs; -static int num_intruder_runs; static FILE *attack_stream; struct goalstruct @@ -2481,456 +2485,6 @@ bind_goal (const Binding b) } } -//! Prune determination because of theorems -/** - * When something is pruned because of this function, the state space is still - * considered to be complete. - * - *@returns true iff this state is invalid because of a theorem - */ -int -prune_theorems () -{ - Termlist tl; - List bl; - int run; - - // Check all types of the local agents according to the matching type - if (!checkAllSubstitutions (sys)) - { - if (switches.output == PROOF) - { - indentPrint (); - eprintf - ("Pruned because some local variable was incorrectly subsituted.\n"); - } - return 1; - } - - // Check if all actors are agents for responders (initiators come next) - run = 0; - while (run < sys->maxruns) - { - if (!sys->runs[run].role->initiator) - { - Term actor; - - actor = agentOfRun (sys, run); - if (!goodAgentType (actor)) - { - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Pruned because the actor "); - termPrint (actor); - eprintf (" of run %i is not of a compatible type.\n", run); - } - return 1; - } - } - run++; - } - - // Prune if any initiator run talks to itself - /** - * This effectively disallows Alice from talking to Alice, for all - * initiators. We still allow it for responder runs, because we assume the - * responder is not checking this. - */ - if (switches.extravert) - { - int run; - - run = 0; - while (run < sys->maxruns) - { - // Check this run only if it is an initiator role - if (sys->runs[run].role->initiator) - { - // Check this initiator run - Termlist tl; - - tl = sys->runs[run].agents; - while (tl != NULL) - { - Termlist tlscan; - - tlscan = tl->next; - while (tlscan != NULL) - { - if (isTermEqual (tl->term, tlscan->term)) - { - // XXX TODO - // Still need to fix proof output for this - // - // Pruning because some agents are equal for this role. - return 1; - } - tlscan = tlscan->next; - } - tl = tl->next; - } - run++; - } - } - } - - // Prune wrong agents type for initators - if (!initiatorAgentsType ()) - { - if (switches.output == PROOF) - { - indentPrint (); - eprintf - ("Pruned: an initiator role does not have the correct type for one of its agents.\n"); - } - return 1; - } - - // Check if all agents of the main run are valid - if (!isRunTrusted (sys, 0)) - { - if (switches.output == PROOF) - { - indentPrint (); - eprintf - ("Pruned because all agents of the claim run must be trusted.\n"); - } - return 1; - } - - // Check if the actors of all other runs are not untrusted - if (sys->untrusted != NULL) - { - int run; - - run = 1; - while (run < sys->maxruns) - { - if (sys->runs[run].protocol != INTRUDER) - { - if (sys->runs[run].agents != NULL) - { - Term actor; - - actor = agentOfRun (sys, run); - if (actor == NULL) - { - error ("Agent of run %i is NULL", run); - } - if (!isAgentTrusted (sys, actor)) - { - if (switches.output == PROOF) - { - indentPrint (); - eprintf - ("Pruned because the actor of run %i is untrusted.\n", - run); - } - return 1; - } - } - else - { - Protocol p; - - globalError++; - eprintf ("Run %i: ", run); - role_name_print (run); - eprintf (" has an empty agents list.\n"); - eprintf ("protocol->rolenames: "); - p = (Protocol) sys->runs[run].protocol; - termlistPrint (p->rolenames); - eprintf ("\n"); - error ("Aborting."); - globalError--; - return 1; - } - } - run++; - } - } - - // Check for c-minimality - { - if (!bindings_c_minimal ()) - { - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Pruned because this is not <=c-minimal.\n"); - } - return 1; - } - } - - /** - * Check whether the bindings are valid - */ - bl = sys->bindings; - while (bl != NULL) - { - Binding b; - - b = bl->data; - - // Check for "Hidden" interm goals - if (termInTerm (b->term, TERM_Hidden)) - { - // Prune the state: we can never meet this - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Pruned because intruder can never construnct "); - termPrint (b->term); - eprintf ("\n"); - } - return 1; - } - - // Check for encryption levels - /* - * if (switches.match < 2 - */ - if (term_encryption_level (b->term) > max_encryption_level) - { - // Prune: we do not need to construct such terms - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Pruned because the encryption level of "); - termPrint (b->term); - eprintf (" is too high.\n"); - } - return 1; - } - - // Check for SK-type function occurrences - //!@todo Needs a LEMMA, although this seems to be quite straightforward to prove. - // The idea is that functions are never sent as a whole, but only used in applications. - if (isTermFunctionName (b->term)) - { - if (!inKnowledge (sys->know, b->term)) - { - // Not in initial knowledge of the intruder - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Pruned because the function "); - termPrint (b->term); - eprintf (" is not known initially to the intruder.\n"); - } - return 1; - } - } - - bl = bl->next; - } - - /* check for singular roles */ - run = 0; - while (run < sys->maxruns) - { - if (sys->runs[run].role->singular) - { - // This is a singular role: it therefore should not occur later on again. - int run2; - Term rolename; - - rolename = sys->runs[run].role->nameterm; - run2 = run + 1; - while (run2 < sys->maxruns) - { - Term rolename2; - - rolename2 = sys->runs[run2].role->nameterm; - if (isTermEqual (rolename, rolename2)) - { - // This is not allowed: the singular role occurs twice in the semitrace. - // Thus we prune. - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Pruned because the singular role "); - termPrint (rolename); - eprintf (" occurs more than once in the semitrace.\n"); - } - return 1; - } - run2++; - } - } - run++; - } - - return 0; -} - -//! Prune determination for bounds -/** - * When something is pruned here, the state space is not complete anymore. - * - *@returns true iff this state is invalid for some reason - */ -int -prune_bounds () -{ - Termlist tl; - List bl; - - /* prune for time */ - if (passed_time_limit ()) - { - // Oh no, we ran out of time! - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Pruned: ran out of allowed time (-T %i switch)\n", - get_time_limit ()); - } - // Pruned because of time bound! - sys->current_claim->timebound = 1; - return 1; - } - - /* prune for proof depth */ - if (proofDepth > switches.maxproofdepth) - { - // Hardcoded limit on proof tree depth - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Pruned: proof tree too deep: %i (-d %i switch)\n", - proofDepth, switches.maxproofdepth); - } - return 1; - } - - /* prune for trace length */ - if (switches.maxtracelength < INT_MAX) - { - int tracelength; - int run; - - /* compute trace length of current semistate */ - tracelength = 0; - run = 0; - while (run < sys->maxruns) - { - /* ignore intruder actions */ - if (sys->runs[run].protocol != INTRUDER) - { - tracelength = tracelength + sys->runs[run].step; - } - run++; - } - /* test */ - if (tracelength > switches.maxtracelength) - { - // Hardcoded limit on proof tree depth - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Pruned: trace too long: %i (-l %i switch)\n", - tracelength, switches.maxtracelength); - } - return 1; - } - } - - if (num_regular_runs > switches.runs) - { - // Hardcoded limit on runs - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Pruned: too many regular runs (%i).\n", num_regular_runs); - } - return 1; - } - - // This needs some foundation. Probably * 2^max_encryption_level - //!@todo Fix this bound - if ((switches.match < 2) - && (num_intruder_runs > - ((double) switches.runs * max_encryption_level * 8))) - { - // Hardcoded limit on iterations - if (switches.output == PROOF) - { - indentPrint (); - eprintf - ("Pruned: %i intruder runs is too much. (max encr. level %i)\n", - num_intruder_runs, max_encryption_level); - } - return 1; - } - - // Limit on exceeding any 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: attack cost exceeds a previously found attack.\n"); - } - return 1; - } - - // Limit on attack count - if (enoughAttacks (sys)) - return 1; - - // Pruning involving the number of intruder actions - { - // Count intruder actions - int actioncount; - - actioncount = countIntruderActions (); - - // Limit intruder actions in any case - if (!(switches.intruder) && actioncount > 0) - { - if (switches.output == PROOF) - { - indentPrint (); - eprintf - ("Pruned: no intruder allowed.\n", switches.maxIntruderActions); - } - return 1; - } - - // Limit on intruder events count - if (actioncount > switches.maxIntruderActions) - { - if (switches.output == PROOF) - { - indentPrint (); - eprintf - ("Pruned: more than %i encrypt/decrypt events in the semitrace.\n", - switches.maxIntruderActions); - } - return 1; - } - } - - // No pruning because of bounds - return 0; -} - //! Prune determination for specific properties /** * Sometimes, a property holds in part of the tree. Thus, we don't need to explore that part further if we want to find an attack. @@ -3337,11 +2891,11 @@ iterate () flag = 1; - if (!prune_theorems ()) + if (!prune_theorems (sys)) { if (!prune_claim_specifics ()) { - if (!prune_bounds ()) + if (!prune_bounds (sys)) { Binding b; diff --git a/src/prune_bounds.c b/src/prune_bounds.c new file mode 100644 index 0000000..d725fab --- /dev/null +++ b/src/prune_bounds.c @@ -0,0 +1,186 @@ +/** + * + *@file prune_bounds.c + * + * Prune stuff based on bounds + * + */ + +#include + +#include "termlist.h" +#include "list.h" +#include "switches.h" + +extern int attack_length; +extern int attack_leastcost; +extern Protocol INTRUDER; +extern int proofDepth; +extern int max_encryption_level; +extern int num_regular_runs; +extern int num_intruder_runs; + +//! Prune determination for bounds +/** + * When something is pruned here, the state space is not complete anymore. + * + *@returns true iff this state is invalid for some reason + */ +int +prune_bounds (const System sys) +{ + Termlist tl; + List bl; + + /* prune for time */ + if (passed_time_limit ()) + { + // Oh no, we ran out of time! + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned: ran out of allowed time (-T %i switch)\n", + get_time_limit ()); + } + // Pruned because of time bound! + sys->current_claim->timebound = 1; + return 1; + } + + /* prune for proof depth */ + if (proofDepth > switches.maxproofdepth) + { + // Hardcoded limit on proof tree depth + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned: proof tree too deep: %i (-d %i switch)\n", + proofDepth, switches.maxproofdepth); + } + return 1; + } + + /* prune for trace length */ + if (switches.maxtracelength < INT_MAX) + { + int tracelength; + int run; + + /* compute trace length of current semistate */ + tracelength = 0; + run = 0; + while (run < sys->maxruns) + { + /* ignore intruder actions */ + if (sys->runs[run].protocol != INTRUDER) + { + tracelength = tracelength + sys->runs[run].step; + } + run++; + } + /* test */ + if (tracelength > switches.maxtracelength) + { + // Hardcoded limit on proof tree depth + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned: trace too long: %i (-l %i switch)\n", + tracelength, switches.maxtracelength); + } + return 1; + } + } + + if (num_regular_runs > switches.runs) + { + // Hardcoded limit on runs + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned: too many regular runs (%i).\n", num_regular_runs); + } + return 1; + } + + // This needs some foundation. Probably * 2^max_encryption_level + //!@todo Fix this bound + if ((switches.match < 2) + && (num_intruder_runs > + ((double) switches.runs * max_encryption_level * 8))) + { + // Hardcoded limit on iterations + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned: %i intruder runs is too much. (max encr. level %i)\n", + num_intruder_runs, max_encryption_level); + } + return 1; + } + + // Limit on exceeding any 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: attack cost exceeds a previously found attack.\n"); + } + return 1; + } + + // Limit on attack count + if (enoughAttacks (sys)) + return 1; + + // Pruning involving the number of intruder actions + { + // Count intruder actions + int actioncount; + + actioncount = countIntruderActions (); + + // Limit intruder actions in any case + if (!(switches.intruder) && actioncount > 0) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned: no intruder allowed.\n", switches.maxIntruderActions); + } + return 1; + } + + // Limit on intruder events count + if (actioncount > switches.maxIntruderActions) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned: more than %i encrypt/decrypt events in the semitrace.\n", + switches.maxIntruderActions); + } + return 1; + } + } + + // No pruning because of bounds + return 0; +} diff --git a/src/prune_bounds.h b/src/prune_bounds.h new file mode 100644 index 0000000..ded64f4 --- /dev/null +++ b/src/prune_bounds.h @@ -0,0 +1,6 @@ +#ifndef PRUNEBOUNDS +#define PRUNEBOUNDS + +int prune_bounds (const System sys); + +#endif diff --git a/src/prune_theorems.c b/src/prune_theorems.c new file mode 100644 index 0000000..b419dd6 --- /dev/null +++ b/src/prune_theorems.c @@ -0,0 +1,303 @@ +/** + * + *@file prune_theorems.c + * + * Prune stuff based on theorems. + * Pruning leaves complete results. + * + */ + +#include "system.h" +#include "list.h" +#include "switches.h" +#include "binding.h" +#include "specialterm.h" + +extern Protocol INTRUDER; +extern int proofDepth; +extern int max_encryption_level; + +//! Prune determination because of theorems +/** + * When something is pruned because of this function, the state space is still + * considered to be complete. + * + *@returns true iff this state is invalid because of a theorem + */ +int +prune_theorems (const System sys) +{ + Termlist tl; + List bl; + int run; + + // Check all types of the local agents according to the matching type + if (!checkAllSubstitutions (sys)) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned because some local variable was incorrectly subsituted.\n"); + } + return 1; + } + + // Check if all actors are agents for responders (initiators come next) + run = 0; + while (run < sys->maxruns) + { + if (!sys->runs[run].role->initiator) + { + Term actor; + + actor = agentOfRun (sys, run); + if (!goodAgentType (actor)) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned because the actor "); + termPrint (actor); + eprintf (" of run %i is not of a compatible type.\n", run); + } + return 1; + } + } + run++; + } + + // Prune if any initiator run talks to itself + /** + * This effectively disallows Alice from talking to Alice, for all + * initiators. We still allow it for responder runs, because we assume the + * responder is not checking this. + */ + if (switches.extravert) + { + int run; + + run = 0; + while (run < sys->maxruns) + { + // Check this run only if it is an initiator role + if (sys->runs[run].role->initiator) + { + // Check this initiator run + Termlist tl; + + tl = sys->runs[run].agents; + while (tl != NULL) + { + Termlist tlscan; + + tlscan = tl->next; + while (tlscan != NULL) + { + if (isTermEqual (tl->term, tlscan->term)) + { + // XXX TODO + // Still need to fix proof output for this + // + // Pruning because some agents are equal for this role. + return 1; + } + tlscan = tlscan->next; + } + tl = tl->next; + } + run++; + } + } + } + + // Prune wrong agents type for initators + if (!initiatorAgentsType ()) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned: an initiator role does not have the correct type for one of its agents.\n"); + } + return 1; + } + + // Check if all agents of the main run are valid + if (!isRunTrusted (sys, 0)) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned because all agents of the claim run must be trusted.\n"); + } + return 1; + } + + // Check if the actors of all other runs are not untrusted + if (sys->untrusted != NULL) + { + int run; + + run = 1; + while (run < sys->maxruns) + { + if (sys->runs[run].protocol != INTRUDER) + { + if (sys->runs[run].agents != NULL) + { + Term actor; + + actor = agentOfRun (sys, run); + if (actor == NULL) + { + error ("Agent of run %i is NULL", run); + } + if (!isAgentTrusted (sys, actor)) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned because the actor of run %i is untrusted.\n", + run); + } + return 1; + } + } + else + { + Protocol p; + + globalError++; + eprintf ("Run %i: ", run); + role_name_print (run); + eprintf (" has an empty agents list.\n"); + eprintf ("protocol->rolenames: "); + p = (Protocol) sys->runs[run].protocol; + termlistPrint (p->rolenames); + eprintf ("\n"); + error ("Aborting."); + globalError--; + return 1; + } + } + run++; + } + } + + // Check for c-minimality + { + if (!bindings_c_minimal ()) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned because this is not <=c-minimal.\n"); + } + return 1; + } + } + + /** + * Check whether the bindings are valid + */ + bl = sys->bindings; + while (bl != NULL) + { + Binding b; + + b = bl->data; + + // Check for "Hidden" interm goals + if (termInTerm (b->term, TERM_Hidden)) + { + // Prune the state: we can never meet this + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned because intruder can never construnct "); + termPrint (b->term); + eprintf ("\n"); + } + return 1; + } + + // Check for encryption levels + /* + * if (switches.match < 2 + */ + if (term_encryption_level (b->term) > max_encryption_level) + { + // Prune: we do not need to construct such terms + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned because the encryption level of "); + termPrint (b->term); + eprintf (" is too high.\n"); + } + return 1; + } + + // Check for SK-type function occurrences + //!@todo Needs a LEMMA, although this seems to be quite straightforward to prove. + // The idea is that functions are never sent as a whole, but only used in applications. + if (isTermFunctionName (b->term)) + { + if (!inKnowledge (sys->know, b->term)) + { + // Not in initial knowledge of the intruder + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned because the function "); + termPrint (b->term); + eprintf (" is not known initially to the intruder.\n"); + } + return 1; + } + } + + bl = bl->next; + } + + /* check for singular roles */ + run = 0; + while (run < sys->maxruns) + { + if (sys->runs[run].role->singular) + { + // This is a singular role: it therefore should not occur later on again. + int run2; + Term rolename; + + rolename = sys->runs[run].role->nameterm; + run2 = run + 1; + while (run2 < sys->maxruns) + { + Term rolename2; + + rolename2 = sys->runs[run2].role->nameterm; + if (isTermEqual (rolename, rolename2)) + { + // This is not allowed: the singular role occurs twice in the semitrace. + // Thus we prune. + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned because the singular role "); + termPrint (rolename); + eprintf (" occurs more than once in the semitrace.\n"); + } + return 1; + } + run2++; + } + } + run++; + } + + return 0; +} diff --git a/src/prune_theorems.h b/src/prune_theorems.h new file mode 100644 index 0000000..ce9c06c --- /dev/null +++ b/src/prune_theorems.h @@ -0,0 +1,6 @@ +#ifndef PRUNETHEOREMS +#define PRUNETHEOREMS + +int prune_theorems (const System sys); + +#endif