From b49d13b6eecff70cba1af8f3a495463227346b6d Mon Sep 17 00:00:00 2001 From: ccremers Date: Mon, 27 Feb 2006 16:08:17 +0000 Subject: [PATCH] - [[[ Broken commit. ]]] Stuff seems to be working again, slightly less efficient though (count states). --- src/arachne.c | 661 ++++++++++++++++++------------------------- src/claim.c | 23 +- src/claim.h | 4 +- src/compiler.c | 13 +- src/depend.c | 94 ++++-- src/mgu.c | 116 ++++++-- src/mgu.h | 6 +- src/prune_theorems.c | 52 ++++ src/system.c | 140 +++++++++ src/system.h | 11 + src/term.c | 33 ++- src/term.h | 15 +- 12 files changed, 714 insertions(+), 454 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 92098e6..43a76d7 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -378,41 +378,48 @@ fixAgentKeylevels (void) int add_read_goals (const int run, const int old, const int new) { - int count; - int i; - Roledef rd; + if (new <= sys->runs[run].height) + { + return 0; + } + else + { + int count; + int i; + Roledef rd; - sys->runs[run].height = new; - i = old; - rd = roledef_shift (sys->runs[run].start, i); - count = 0; - while (i < new && rd != NULL) - { - if (rd->type == READ) + sys->runs[run].height = new; + i = old; + rd = roledef_shift (sys->runs[run].start, i); + count = 0; + while (i < new && rd != NULL) { - if (switches.output == PROOF) + if (rd->type == READ) { - if (count == 0) + if (switches.output == PROOF) { - indentPrint (); - eprintf ("Thus, we must also produce "); + if (count == 0) + { + indentPrint (); + eprintf ("Thus, we must also produce "); + } + else + { + eprintf (", "); + } + termPrint (rd->message); } - else - { - eprintf (", "); - } - termPrint (rd->message); + count = count + goal_add (rd->message, run, i, 0); } - count = count + goal_add (rd->message, run, i, 0); + rd = rd->next; + i++; } - rd = rd->next; - i++; + if ((count > 0) && switches.output == PROOF) + { + eprintf ("\n"); + } + return count; } - if ((count > 0) && switches.output == PROOF) - { - eprintf ("\n"); - } - return count; } //! Determine the run that follows from a substitution. @@ -756,114 +763,75 @@ getPriorityOfNeededKey (const System sys, const Term keyneeded) return prioritylevel; } -//! Try to bind a specific existing run to a goal. + +//! Make a decryption chain from a binding to some run,index using the key list, and callback if this works. /** - * The idea is that we try to bind it this specific run and index. If this - * requires keys, then we should add such goals as well with the required - * decryptor things. - * - * The key goals are bound to the goal. Iterates on success. + * Callback return value is int, but is effectively ignored. */ void -bind_existing_to_goal (const Binding b, const int run, const int index) +createDecryptionChain (const Binding b, const int run, const int index, + Termlist keylist, int (*callback) (void)) { - int old_length; - int newgoals; - Term goalterm; - - int subterm_unification_needs (Term tbig, const int r, const int e) - { - Term t; - - void bind_iterate (Termlist tl) + if (keylist == NULL) { - if (goal_bind (b, r, e)) + // Immediate binding, no key needed. + if (goal_bind (b, run, index)) { - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Iterating for "); - termPrint (b->term); - eprintf (" to occur first in "); - termPrint (roledef_shift (sys->runs[run].start, index)-> - message); - eprintf ("\n"); - } - iterate (); + callback (); goal_unbind (b); + return; } } + else + { + Term tdecr, tkey; + int smallrun; - t = deVar (b->term); - tbig = deVar (tbig); + // Some decryptor is needed for the term in the list - // First check whether it unifies in a simple way - unify (t, tbig, NULL, bind_iterate); + indentDepth++; - // The other options are unification on subparts - if (realTermTuple (tbig)) + tdecr = keylist->term; + tkey = inverseKey (sys->know->inverses, TermKey (tdecr)); + smallrun = create_decryptor (tdecr, tkey); { - // Either one will do - subterm_unification_needs (TermOp1 (tbig), r, e); - subterm_unification_needs (TermOp1 (tbig), r, e); - } - if (realTermEncrypt (tbig)) - { - Term keyneeded; Roledef rddecrypt; - int smallrun; - int prioritylevel; - int newgoals; Binding bnew; + int newgoals; + int prioritylevel; + + /* + * 2. Add goal bindings + */ - indentDepth++; - // Maybe we can bind to the inner thing. Try. - // Add decryptor run - keyneeded = inverseKey (sys->know->inverses, TermKey (tbig)); - prioritylevel = getPriorityOfNeededKey (sys, keyneeded); - smallrun = create_decryptor (tbig, keyneeded); rddecrypt = sys->runs[smallrun].start; + // Add goal for tdecr copy + newgoals = goal_add (rddecrypt->message, smallrun, 0, 0); + if (newgoals != 1) + { + error + ("Added %i goals (instead of one) for decryptor goal 1, weird.", + newgoals); + } + + // This is the unique new goal + bnew = (Binding) sys->bindings->data; + + // Add goal for needed key copy + prioritylevel = getPriorityOfNeededKey (sys, tkey); + newgoals += goal_add (rddecrypt->next->message, smallrun, 1, + prioritylevel); if (switches.output == PROOF) { indentPrint (); eprintf ("This introduces the obligation to decrypt the following subterm: "); - termPrint (tbig); + termPrint (tdecr); eprintf (" to be decrypted using "); - termPrint (keyneeded); + termPrint (tkey); eprintf ("\n"); - } - /* - * 2. Add goal bindings - */ - - newgoals = goal_add (rddecrypt->message, smallrun, 0, 0); - if (newgoals >= 0) - { - if (newgoals > 1) - { - error - ("Added more than one goal for decryptor goal 1, weird."); - } - else - { - // This is the unique new goal then - bnew = (Binding) sys->bindings->data; - } - } - else - { - error ("No new binding added for inner message."); - // No new binding? Weird, but fair enough - bnew = NULL; - } - - newgoals += goal_add (rddecrypt->next->message, smallrun, 1, - prioritylevel); - if (switches.output == PROOF) - { indentPrint (); eprintf ("To this end, we added two new goals and one new send: "); @@ -878,257 +846,122 @@ bind_existing_to_goal (const Binding b, const int run, const int index) /* * 3. Bind open goal to decryptor? */ - if (goal_bind (bnew, r, e)) + if (goal_bind (b, smallrun, 2)) { if (switches.output == PROOF) { indentPrint (); - eprintf ("Bound: trying new subterm_unfication_needs.\n"); + eprintf ("Bound: trying new createDecryptionChain.\n"); } - subterm_unification_needs (TermOp (tbig), smallrun, 2); - goal_unbind (bnew); + + // Iterate with the new goal + createDecryptionChain (bnew, run, index, keylist->next, callback); + goal_unbind (b); } /* * clean up */ - termDelete (keyneeded); goal_remove_last (newgoals); - semiRunDestroy (); - indentDepth--; } - } + semiRunDestroy (); + termDelete (tkey); - old_length = sys->runs[run].height; - if (index >= old_length) - { - newgoals = add_read_goals (run, old_length, index + 1); + indentDepth--; } - else - { - newgoals = 0; - } - goalterm = roledef_shift (sys->runs[run].start, index)->message; - subterm_unification_needs (goalterm, run, index); - if (newgoals > 0) - { - goal_remove_last (newgoals); - } - sys->runs[run].height = old_length; } + //! Try to bind a specific existing run to a goal. /** - * The key goals are bound to the goal. + * The idea is that we try to bind it this specific run and index. If this + * requires keys, then we should add such goals as well with the required + * decryptor things. * - *@todo This is currently NOT correct. The point is that the key chain - * cannot uniquely define a path through a term in general, and - * a rewrite of termMguSubterm is needed. It should not yield the - * needed keys, but simply the path throught the term. This would enable - * reconstruction of the keys anyway. TODO - * - *@param b binding to fix (bind), destination filled in - *@param run run of binding start - *@param index index in run of binding start + * The key goals are bound to the goal. Iterates on success. */ -int -bind_existing_to_goal_old (const Binding b, const int run, const int index) +void +bind_existing_to_goal (const Binding b, const int run, const int index) { - Roledef rd; - int flag; - int old_length; - int newgoals; - int found; + Term bigterm; - int subterm_iterate (Termlist substlist, Termlist cryptlist) + int unifiesWithKeys (Termlist substlist, Termlist keylist) { - int flag; - - found++; - flag = 1; - /** - * Now create the new bindings - */ + int old_length; int newgoals; - int newruns; - int stillvalid; - Binding smalltermbinding; + // We need some adapting because the height would increase; we therefore + // have to add read goals before we know whether it unifies. + old_length = sys->runs[run].height; + newgoals = add_read_goals (run, old_length, index + 1); - stillvalid = true; // New stuff is valid (no cycles) - newgoals = 0; // No new goals introduced (yet) - newruns = 0; // New runs introduced - smalltermbinding = b; // Start off with destination binding + { + // wrap substitution lists - indentDepth++; -#ifdef DEBUG - if (DEBUGL (4)) + void wrapSubst (Termlist sl) { - eprintf ("Trying to bind the small term "); - termPrint (b->term); - eprintf (" as coming from the big send "); - termPrint (rd->message); - eprintf (" , binding "); - termPrint (b->term); - eprintf ("\nCrypted list needed: "); - termlistPrint (cryptlist); - eprintf ("\n"); - } -#endif - if (cryptlist != NULL && switches.output == PROOF) - { - indentPrint (); - eprintf - ("This introduces the obligation to decrypt the following encrypted subterms: "); - termlistPrint (cryptlist); - eprintf ("\n"); - } - - /* The order of the cryptlist is inner -> outer */ - while (stillvalid && cryptlist != NULL && smalltermbinding != NULL) - { - /* - * Invariants: - * - * smalltermbinding binding to be satisfied next (and for which a decryptor is needed) - */ - Term keyneeded; - int prioritylevel; - int smallrun; - int count; - Roledef rddecrypt; - Binding bnew; - int res; - - /* - * 1. Add decryptor - */ - - keyneeded = - inverseKey (sys->know->inverses, TermKey (cryptlist->term)); - prioritylevel = getPriorityOfNeededKey (sys, keyneeded); - smallrun = create_decryptor (cryptlist->term, keyneeded); - rddecrypt = sys->runs[smallrun].start; - termDelete (keyneeded); - newruns++; - - /* - * 2. Add goal bindings - */ - - count = goal_add (rddecrypt->message, smallrun, 0, 0); - newgoals = newgoals + count; - if (count >= 0) + if (sl == NULL) { - if (count > 1) - { - error - ("Added more than one goal for decryptor goal 1, weird."); - } - else - { - // This is the unique new goal then - bnew = (Binding) sys->bindings->data; - } + // new create key goals, bind etc. + createDecryptionChain (b, run, index, keylist, iterate); } else { - // No new binding? Weird, but fair enough - bnew = NULL; - } - newgoals = - newgoals + goal_add (rddecrypt->next->message, smallrun, 1, - prioritylevel); + int neworders; + int allgood; - /* - * 3. Bind open goal to decryptor - */ + // the idea is, that a substitution in run x with + // something containing should be wrapped; this + // occurs for all subterms of other runs. + int makeDepend (Term t) + { + int r1, e1; - res = goal_bind (smalltermbinding, smallrun, 2); // returns 0 iff invalid - if (res != 0) - { - // Allright, good binding, proceed with next - smalltermbinding = bnew; - } - else - { - stillvalid = false; - } + r1 = TermRunid (t); + e1 = firstOccurrence (sys, r1, t, SEND); + if (dependPushEvent (r1, e1, run, index)) + { + neworders++; + return true; + } + else + { + allgood = false; + return false; + } + } - /* progression */ - cryptlist = cryptlist->next; - } + neworders = 0; + allgood = true; + iterateTermOther (run, sl->term, makeDepend); - /* - * Decryptors for any nested keys have been added. Now we can fill the - * final binding. - */ - - if (stillvalid) - { - if (goal_bind (smalltermbinding, run, index)) - { - proof_suppose_binding (b); -#ifdef DEBUG - if (DEBUGL (4)) + if (allgood) { - indentPrint (); - eprintf ("Added %i new goals, iterating.\n", newgoals); + wrapSubst (sl->next); + } + while (neworders > 0) + { + neworders--; + dependPopEvent (); } -#endif - /* Iterate process */ - indentDepth++; - flag = flag && iterate (); - indentDepth--; - - goal_unbind (b); - } - else - { - proof_cannot_bind (b, run, index); } } + wrapSubst (substlist); + } + + // undo goal_remove_last (newgoals); - while (newruns > 0) - { - semiRunDestroy (); - newruns--; - } - - indentDepth--; - return flag; + sys->runs[run].height = old_length; + return true; } - //---------------------------- - // Roledef entry - rd = roledef_shift (sys->runs[run].start, index); - - // Fix length - old_length = sys->runs[run].height; - if ((index + 1) > old_length) - newgoals = add_read_goals (run, old_length, index + 1); - else - newgoals = 0; - - // Bind to existing run - found = 0; - flag = termMguSubTerm (b->term, rd->message, - subterm_iterate, sys->know->inverses, NULL); - // Did it work? - if (found == 0 && switches.output == PROOF) - { - indentPrint (); - eprintf ("Cannot bind "); - termPrint (b->term); - eprintf (" to run %i, index %i because it does not subterm-unify.\n", - run, index); - } - // Reset length - goal_remove_last (newgoals); - sys->runs[run].height = old_length; - return flag; + bigterm = roledef_shift (sys->runs[run].start, index)->message; + subtermUnify (bigterm, b->term, NULL, NULL, unifiesWithKeys); } + + + //! Bind a goal to an existing regular run, if possible int bind_existing_run (const Binding b, const Protocol p, const Role r, @@ -1181,11 +1014,12 @@ bind_new_run (const Binding b, const Protocol p, const Role r, const int index) { int run; - int newgoals; run = semiRunCreate (p, r); proof_suppose_run (run, 0, index + 1); { + int newgoals; + newgoals = add_read_goals (run, 0, index + 1); indentDepth++; bind_existing_to_goal (b, run, index); @@ -1269,6 +1103,9 @@ printSemiState () } //! Check if a binding duplicates an old one: if so, simply connect +/** + * If it returns true, it has bound the b_new binding, which we must unbind later. + */ int bind_old_goal (const Binding b_new) { @@ -1339,7 +1176,36 @@ bind_goal_new_m0 (const Binding b) termPrint (b->term); eprintf (" from the initial knowledge.\n"); } - flag = flag && iterate (); + + { + // Now we also want to add bindings to have this run before all other runs + void wrapRunOrders (const int otherrun) + { + if (otherrun < 0) + { + // No more runs to do + flag = flag && iterate (); + } + else + { + if (otherrun != run) + { + if (dependPushEvent (run, 0, otherrun, 0)) + { + wrapRunOrders (otherrun - 1); + dependPopEvent (); + } + } + else + { + wrapRunOrders (otherrun - 1); + } + } + } + + wrapRunOrders (sys->maxruns - 1); + } + goal_unbind (b); } else @@ -1389,10 +1255,6 @@ bind_goal_new_encrypt (const Binding b) if (!realTermLeaf (term)) { - int run; - int index; - int newgoals; - Roledef rd; Term t1, t2; if (!realTermEncrypt (term)) @@ -1407,40 +1269,53 @@ bind_goal_new_encrypt (const Binding b) if (t2 != TERM_Hidden) { + int run; + can_be_encrypted = 1; run = semiRunCreate (INTRUDER, I_RRS); - rd = sys->runs[run].start; - rd->message = termDuplicateUV (t1); - rd->next->message = termDuplicateUV (t2); - rd->next->next->message = termDuplicateUV (term); - index = 2; - proof_suppose_run (run, 0, index + 1); - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("* Encrypting "); - termPrint (term); - eprintf (" using term "); - termPrint (t1); - eprintf (" and key "); - termPrint (t2); - eprintf ("\n"); - } - newgoals = add_read_goals (run, 0, index + 1); + { + int index; + Roledef rd; + + rd = sys->runs[run].start; + rd->message = termDuplicateUV (t1); + rd->next->message = termDuplicateUV (t2); + rd->next->next->message = termDuplicateUV (term); + index = 2; + proof_suppose_run (run, 0, index + 1); + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("* Encrypting "); + termPrint (term); + eprintf (" using term "); + termPrint (t1); + eprintf (" and key "); + termPrint (t2); + eprintf ("\n"); + } - indentDepth++; - if (goal_bind (b, run, index)) { - proof_suppose_binding (b); - flag = flag && iterate (); - goal_unbind (b); + int newgoals; + newgoals = add_read_goals (run, 0, index + 1); + { + + indentDepth++; + if (goal_bind (b, run, index)) + { + proof_suppose_binding (b); + flag = flag && iterate (); + goal_unbind (b); + } + else + { + proof_cannot_bind (b, run, index); + } + indentDepth--; + } + goal_remove_last (newgoals); } - else - { - proof_cannot_bind (b, run, index); - } - indentDepth--; - goal_remove_last (newgoals); + } semiRunDestroy (); } } @@ -1456,7 +1331,6 @@ bind_goal_new_encrypt (const Binding b) } } - return flag; } @@ -1637,7 +1511,7 @@ bind_goal_old_intruder_run (Binding b) //! Bind a goal in all possible ways int -bind_goal (const Binding b) +bind_goal_all_options (const Binding b) { if (b->blocked) { @@ -2091,26 +1965,28 @@ iterate () { if (!prune_bounds (sys)) { - Binding b; + Binding btup; // Are there any tuple goals? - b = select_tuple_goal (); - if (b != NULL) + btup = select_tuple_goal (); + if (btup != NULL) { // Expand tuple goal int count; // mark as blocked for iteration - binding_block (b); + binding_block (btup); // simply adding will detect the tuple and add the new subgoals - count = goal_add (b->term, b->run_to, b->ev_to, b->level); + count = + goal_add (btup->term, btup->run_to, btup->ev_to, + btup->level); // Show this in output if (switches.output == PROOF) { indentPrint (); eprintf ("Expanding tuple goal "); - termPrint (b->term); + termPrint (btup->term); eprintf (" into %i subgoals.\n", count); } @@ -2119,7 +1995,7 @@ iterate () // undo goal_remove_last (count); - binding_unblock (b); + binding_unblock (btup); } else { @@ -2159,7 +2035,7 @@ iterate () /* * bind this goal in all possible ways and iterate */ - flag = bind_goal (b); + flag = bind_goal_all_options (b); } } } @@ -2316,9 +2192,11 @@ arachne () { // 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; @@ -2338,34 +2216,57 @@ arachne () eprintf (" at index %i.\n", cl->ev); } indentDepth++; + run = semiRunCreate (p, r); - proof_suppose_run (run, 0, cl->ev + 1); - add_read_goals (run, 0, cl->ev + 1); - - /** - * Add specific goal info - */ - add_claim_specifics (sys, cl, - roledef_shift (sys->runs[run].start, - cl->ev)); + newruns++; + { + int newgoals; + int realStart (void) + { #ifdef DEBUG - if (DEBUGL (5)) - { - printSemiState (); - } + if (DEBUGL (5)) + { + printSemiState (); + } #endif - iterate_buffer_attacks (); - - //! Destroy - while (sys->bindings != NULL) - { - goal_remove_last (1); + return iterate_buffer_attacks (); } - while (sys->maxruns > 0) + + proof_suppose_run (run, 0, cl->ev + 1); + newgoals = add_read_goals (run, 0, cl->ev + 1); + + /** + * Add specific goal info and iterate + */ + add_claim_specifics (sys, cl, + roledef_shift (sys->runs[run].start, + cl->ev), realStart); + + + goal_remove_last (newgoals); + } + //! 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--; diff --git a/src/claim.c b/src/claim.c index b80f7d9..21d3dcf 100644 --- a/src/claim.c +++ b/src/claim.c @@ -739,12 +739,19 @@ prune_claim_specifics (const System sys) return 0; } -//! Setup system for specific claim test -void -add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd) +//! Setup system for specific claim test and iterate +int +add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd, + int (*callback) (void)) { + /* + * different cases + */ if (cl->type == CLAIM_Secret) { + int newgoals; + int flag; + /** * Secrecy claim */ @@ -764,7 +771,12 @@ add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd) * be reached (without reaching the attack). */ cl->count = statesIncrease (cl->count); - goal_add (rd->message, 0, cl->ev, 0); // Assumption that all claims are in run 0 + newgoals = goal_add (rd->message, 0, cl->ev, 0); // Assumption that all claims are in run 0 + + flag = callback (); + + goal_remove_last (newgoals); + return flag; } if (cl->type == CLAIM_Reachable) @@ -779,7 +791,10 @@ add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd) rolecount = termlistLength (protocol->rolenames); switches.runs = rolecount; } + return callback (); } + + return callback (); } //! Count a false claim diff --git a/src/claim.h b/src/claim.h index 26f2da2..d15798e 100644 --- a/src/claim.h +++ b/src/claim.h @@ -9,8 +9,8 @@ int arachne_claim_nisynch (const System sys, const int claim_run, const int claim_index); int prune_claim_specifics (const System sys); -void add_claim_specifics (const System sys, const Claimlist cl, const - Roledef rd); +int add_claim_specifics (const System sys, const Claimlist cl, const + Roledef rd, int (*callback) (void)); void count_false_claim (const System sys); int property_check (const System sys); diff --git a/src/compiler.c b/src/compiler.c index 7a88bec..1a5c4e5 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -1427,10 +1427,10 @@ compute_prec_sets (const System sys) r1 = 0; while (r1 < sys->rolecount) { - ev1 = 0; - while (ev1 < (sys->roleeventmax - 1)) + ev1 = 1; + while (ev1 < (sys->roleeventmax)) { - SETBIT (prec + rowsize * index (r1, ev1), index (r1, ev1 + 1)); + SETBIT (prec + rowsize * index (r1, ev1 - 1), index (r1, ev1)); ev1++; } r1++; @@ -1472,6 +1472,13 @@ compute_prec_sets (const System sys) r1++; } +#ifdef DEBUG + if (DEBUGL (5)) + { + show_matrix (); + } +#endif + /* * Compute transitive closure (Warshall). */ diff --git a/src/depend.c b/src/depend.c index 3878784..ea475e3 100644 --- a/src/depend.c +++ b/src/depend.c @@ -40,6 +40,14 @@ struct depeventgraph //! Pointer shorthard typedef struct depeventgraph *Depeventgraph; +/* + * External + * --------------------------------------------------------------- + */ + +extern Protocol INTRUDER; //!< The intruder protocol +extern Role I_M; //!< special role; precedes all other events always + /* * Globals * --------------------------------------------------------------- @@ -266,18 +274,12 @@ dependPopGeneric (void) currentdepgraph = dgprev; } -//! Construct graph dependencies from sys -/** - * uses currentdepgraph->sys - */ +// Dependencies from role order void -dependFromSys (void) +dependDefaultRoleOrder (void) { int r; - List bl; - // There are two types of orderings. - // 1. Role orderings (within runs) for (r = 0; r < currentdepgraph->sys->maxruns; r++) { int e; @@ -287,10 +289,14 @@ dependFromSys (void) setDependEvent (r, e - 1, r, e); } } +} + +// Dependencies fro bindings order +void +dependDefaultBindingOrder (void) +{ + List bl; - // 2. Binding orderings - // We implicitly assume these cause no cycles (by construction this is - // correct) for (bl = currentdepgraph->sys->bindings; bl != NULL; bl = bl->next) { Binding b; @@ -313,6 +319,17 @@ dependFromSys (void) } } +//! Construct graph dependencies from sys +/** + * uses currentdepgraph->sys + */ +void +dependFromSys (void) +{ + dependDefaultRoleOrder (); + dependDefaultBindingOrder (); +} + //! Detect whether the graph has a cycle. If so, a node can get to itself (through the cycle) int hasCycle () @@ -386,6 +403,9 @@ isDependEvent (const int r1, const int e1, const int r2, const int e2) void dependPushRun (const System sys) { +#ifdef DEBUG + debug (5, "Push dependGraph for new run\n"); +#endif dependPushGeneric (dependCreate (sys)); dependFromSys (); } @@ -401,6 +421,9 @@ dependPopRun (void) globalError--; error ("Trying to pop graph created for new binding."); } +#ifdef DEBUG + debug (5, "Pop dependGraph for new run\n"); +#endif dependPopGeneric (); } @@ -432,12 +455,21 @@ dependPushEvent (const int r1, const int e1, const int r2, const int e2) else { // No immediate cycle: new graph, return true TODO disabled - if ((1 == 0) && ((r1 == r2) && (e1 == e2)) - || isDependEvent (r1, e1, r2, e2)) + if ((1 == 1) && (((r1 == r2) && (e1 == e2)) + || isDependEvent (r1, e1, r2, e2))) { // if n->n or the binding already existed, no changes // no change: add zombie currentdepgraph->zombie += 1; +#ifdef DEBUG + debug (5, "Push dependGraph for new event (zombie push)\n"); + if (DEBUGL (5)) + { + globalError++; + eprintf ("r%ii%i --> r%ii%i\n", r1, e1, r2, e2); + globalError--; + } +#endif } else { @@ -455,6 +487,15 @@ dependPushEvent (const int r1, const int e1, const int r2, const int e2) dependPopEvent (); return false; } +#ifdef DEBUG + debug (5, "Push dependGraph for new event (real push)\n"); + if (DEBUGL (5)) + { + globalError++; + eprintf ("r%ii%i --> r%ii%i\n", r1, e1, r2, e2); + globalError--; + } +#endif } return true; } @@ -464,22 +505,31 @@ dependPushEvent (const int r1, const int e1, const int r2, const int e2) void dependPopEvent (void) { - if (currentdepgraph->fornewrun) - { - globalError++; - dependPrint (); - globalError--; - error ("Trying to pop graph created for new run."); - } if (currentdepgraph->zombie > 0) { // zombie pushed +#ifdef DEBUG + debug (5, "Pop dependGraph for new event (zombie pop)\n"); +#endif currentdepgraph->zombie -= 1; } else { - // real graph - dependPopGeneric (); + if (currentdepgraph->fornewrun) + { + globalError++; + dependPrint (); + globalError--; + error ("Trying to pop graph created for new run."); + } + else + { + // real graph +#ifdef DEBUG + debug (5, "Pop dependGraph for new event (real pop)\n"); +#endif + dependPopGeneric (); + } } } diff --git a/src/mgu.c b/src/mgu.c index 10a5607..ad27d25 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -117,30 +117,36 @@ termlistSubstReset (Termlist tl) * The callback receives a list of variables, that were previously open, but are now closed * in such a way that the two terms unify. * + * The callback must return true for the iteration to proceed: if it returns false, a single call would abort the scan. + * The return value shows this: it is false if the scan was aborted, and true if not. */ -void -unify (Term t1, Term t2, Termlist tl, void (*callback) (Termlist)) +int +unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist)) { + int proceed; + + proceed = true; /* added for speed */ t1 = deVar (t1); t2 = deVar (t2); if (t1 == t2) { - callback (tl); - return; + return proceed && callback (tl); } int callsubst (Termlist tl, Term t, Term tsubst) { + int proceed; + t->subst = tsubst; #ifdef DEBUG showSubst (t); #endif tl = termlistAdd (tl, t); - callback (tl); + proceed = callback (tl); tl = termlistDelTerm (tl); t->subst = NULL; - return; + return proceed; } if (!(hasTermVariable (t1) || hasTermVariable (t2))) @@ -149,13 +155,12 @@ unify (Term t1, Term t2, Termlist tl, void (*callback) (Termlist)) if (isTermEqual (t1, t2)) { // Equal! - callback (tl); - return; + return proceed && callback (tl); } else { // Can never be fixed, no variables - return; + return proceed; } } @@ -183,8 +188,7 @@ unify (Term t1, Term t2, Termlist tl, void (*callback) (Termlist)) t1 = t2; t2 = t3; } - callsubst (tl, t1, t2); - return; + return proceed && callsubst (tl, t1, t2); } /* symmetrical tests for single variable. @@ -193,61 +197,115 @@ unify (Term t1, Term t2, Termlist tl, void (*callback) (Termlist)) if (realTermVariable (t2)) { if (termSubTerm (t1, t2) || !goodsubst (t2, t1)) - return; + return proceed; else { - callsubst (tl, t2, t1); - return; + return proceed && callsubst (tl, t2, t1); } } if (realTermVariable (t1)) { if (termSubTerm (t2, t1) || !goodsubst (t1, t2)) - return; + return proceed; else { - callsubst (tl, t1, t2); - return; + return proceed && callsubst (tl, t1, t2); } } /* left & right are compounds with variables */ if (t1->type != t2->type) - return; + return proceed; /* identical compound types */ /* encryption first */ if (realTermEncrypt (t1)) { - void unify_combined_enc (Termlist tl) + int unify_combined_enc (Termlist tl) { // now the keys are unified (subst in this tl) // and we try the inner terms - unify (TermOp (t1), TermOp (t2), tl, callback); - return; + return unify (TermOp (t1), TermOp (t2), tl, callback); } - unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc); - return; + return proceed + && unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc); } /* tupling second non-associative version ! TODO other version */ if (isTermTuple (t1)) { - void unify_combined_tup (Termlist tl) + int unify_combined_tup (Termlist tl) { // now the keys are unified (subst in this tl) // and we try the inner terms - unify (TermOp2 (t1), TermOp2 (t2), tl, callback); - return; + return unify (TermOp2 (t1), TermOp2 (t2), tl, callback); } - unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup); - return; + return proceed + && unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup); } - return; + return proceed; +} + + +//! Subterm unification +/** + * Try to unify (a subterm of) tbig with tsmall. + * + * Callback is called with a list of substitutions, and a list of terms that + * need to be decrypted in order for this to work. + * + * E.g. subtermUnify ( {{m}k1}k2, m ) yields a list : {{m}k1}k2, {m}k1 (where + * the {m}k1 is the last added node to the list) + * + * The callback should return true for the iteration to proceed, or false to abort. + * The final result is this flag. + */ +int +subtermUnify (Term tbig, Term tsmall, Termlist tl, Termlist keylist, + int (*callback) (Termlist, Termlist)) +{ + int proceed; + + int keycallback (Termlist tl) + { + return callback (tl, keylist); + } + + proceed = true; + + // Devar + tbig = deVar (tbig); + tsmall = deVar (tsmall); + + // Three options: + // 1. simple unification + proceed = proceed && unify (tbig, tsmall, tl, keycallback); + + // [2/3]: complex + // 2. interm unification + if (realTermTuple (tbig)) + { + proceed = proceed + && subtermUnify (TermOp1 (tbig), tsmall, tl, keylist, callback); + proceed = proceed + && subtermUnify (TermOp2 (tbig), tsmall, tl, keylist, callback); + } + + // 3. unification with encryption needed + if (realTermEncrypt (tbig)) + { + // extend the keylist + keylist = termlistAdd (keylist, tbig); + proceed = proceed + && subtermUnify (TermOp (tbig), tsmall, tl, keylist, callback); + // remove last item again + keylist = termlistDelTerm (keylist); + } + return proceed; } diff --git a/src/mgu.h b/src/mgu.h index afd5e8d..ded4e12 100644 --- a/src/mgu.h +++ b/src/mgu.h @@ -20,6 +20,10 @@ int termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist)); int termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist), Termlist inverses, Termlist keylist); void termlistSubstReset (Termlist tl); -void unify (Term t1, Term t2, Termlist tl, void (*callback) (Termlist)); +// The new iteration methods +int unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist)); +int +subtermUnify (Term tbig, Term tsmall, Termlist tl, Termlist keylist, + int (*callback) (Termlist, Termlist)); #endif diff --git a/src/prune_theorems.c b/src/prune_theorems.c index f9d9586..06845cc 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -17,6 +17,53 @@ extern Protocol INTRUDER; extern int proofDepth; extern int max_encryption_level; + +//! Check locals occurrence +/* + * Returns true if the order is correct + */ +int +correctLocalOrder (const System sys) +{ + int checkRun (int r1) + { + int checkTerm (Term t) + { + if (!isTermVariable (t)) + { + int r2; + int e1, e2; + + // t is a term from r2 that occurs in r1 + r2 = TermRunid (t); + e1 = firstOccurrence (sys, r1, t, READ); + e2 = firstOccurrence (sys, r2, t, SEND); + + // thus, it should not be the case that e1 occurs before e2 + if (isDependEvent (r1, e1, r2, e2)) + { + // That's not good! + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned because ordering for term "); + termPrint (t); + eprintf + (" cannot be correct: the first send r%ii%i occurs after the read r%ii%i.\n", + r2, e2, r1, e1); + } + return false; + } + } + return true; + + } + return iterateLocalToOther (sys, r1, checkTerm); + } + + return iterateRegularRuns (sys, checkRun); +} + //! Check initiator roles /** * Returns false iff an agent type is wrong @@ -232,6 +279,11 @@ prune_theorems (const System sys) } } + /* + * Check for correct orderings involving local constants + */ + correctLocalOrder (sys); + /** * Check whether the bindings are valid */ diff --git a/src/system.c b/src/system.c index 7a5fcfa..e451e25 100644 --- a/src/system.c +++ b/src/system.c @@ -30,6 +30,9 @@ int globalLatex; //! Global count of protocols int protocolCount; +//! External +extern Protocol INTRUDER; + //! Switch for indent or not. static int indentState = 0; //! Current indent depth. @@ -1513,3 +1516,140 @@ enoughAttacks (const System sys) } return 0; } + +//! Iterate over runs. +/** + * Callback should return true in order to continue. + */ +int +iterateRuns (const System sys, int (*callback) (int r)) +{ + int r; + + for (r = 0; r < sys->maxruns; r++) + { + if (!callback (r)) + { + return false; + } + } + return true; +} + +//! Iterate over non-intruder runs. +/** + * Callback should return true in order to continue. + */ +int +iterateRegularRuns (const System sys, int (*callback) (int r)) +{ + int regular (int r) + { + if (sys->runs[r].protocol != INTRUDER) + { + return callback (r); + } + return true; + } + + return iterateRuns (sys, regular); +} + +// Iterate over events in a certain run (increasing through role) +int +iterateEvents (const System sys, const int run, + int (*callback) (Roledef rd, int ev)) +{ + int e; + Roledef rd; + + rd = sys->runs[run].start; + for (e = 0; e < sys->runs[run].step; e++) + { + if (!callback (rd, e)) + { + return false; + } + rd = rd->next; + } + return true; +} + +// Iterate over event type in a certain run (increasing through role) +int +iterateEventsType (const System sys, const int run, const int evtype, + int (*callback) (Roledef rd, int ev)) +{ + int selectEvent (Roledef rd, int e) + { + if (rd->type == evtype) + { + return callback (rd, e); + } + return true; + } + + return iterateEvents (sys, run, selectEvent); +} + +// Iterate over all 'others': local variables of a run that are instantiated and contain some term of another run. +int +iterateLocalToOther (const System sys, const int myrun, + int (*callback) (Term t)) +{ + Termlist tlo, tls; + + int addOther (Term t) + { + tlo = termlistAddNew (tlo, t); + return true; + } + + tlo = NULL; + // construct all others occuring in the reads + for (tls = sys->runs[myrun].locals; tls != NULL; tls = tls->next) + { + iterateTermOther (myrun, tls->term, addOther); + } + // now iterate over all of them + for (tls = tlo; tls != NULL; tls = tls->next) + { + if (!callback (tls->term)) + { + return false; + } + } + + // clean up + termlistDelete (tlo); + return true; +} + +//! Get first read/send occurrence (event index) of term t in run r +int +firstOccurrence (const System sys, const int r, Term t, int evtype) +{ + int firste; + + int checkOccurs (Roledef rd, int e) + { + if (termSubTerm (rd->message, t) || termSubTerm (rd->from, t) + || termSubTerm (rd->to, t)) + { + firste = e; + return false; + } + return true; + } + + if (iterateEventsType (sys, r, evtype, checkOccurs)) + { + globalError++; + eprintf ("Desired term "); + termPrint (t); + eprintf (" does not occur.\n"); + globalError--; + error ("(in run %i in event type %i.)", r, evtype); + } + return firste; +} diff --git a/src/system.h b/src/system.h index 4d5db0a..eeeb491 100644 --- a/src/system.h +++ b/src/system.h @@ -224,6 +224,17 @@ int isAgentTrusted (const System sys, Term agent); int isAgentlistTrusted (const System sys, Termlist agents); int isRunTrusted (const System sys, const int run); +int iterateRuns (const System sys, int (*callback) (int r)); +int iterateRegularRuns (const System sys, int (*callback) (int r)); +int iterateEvents (const System sys, const int run, + int (*callback) (Roledef rd, int ev)); +int iterateEventsType (const System sys, const int run, const int evtype, + int (*callback) (Roledef rd, int ev)); +int iterateLocalToOther (const System sys, const int myrun, + int (*callback) (Term t)); +int firstOccurrence (const System sys, const int r, Term t, int evtype); + + //! Equality for run structure naming /** * For the modelchecker, there was an index called step. In Strand Space diff --git a/src/term.c b/src/term.c index 1dd133e..6ef95bb 100644 --- a/src/term.c +++ b/src/term.c @@ -925,8 +925,8 @@ termOrder (Term t1, Term t2) //! Generic term iteration int -term_iterate (const Term term, int (*leaf) (), int (*nodel) (), - int (*nodem) (), int (*noder) ()) +term_iterate (const Term term, int (*leaf) (Term t), int (*nodel) (Term t), + int (*nodem) (Term t), int (*noder) (Term t)) { if (term != NULL) { @@ -977,8 +977,8 @@ term_iterate (const Term term, int (*leaf) (), int (*nodel) (), //! Generic term iteration int -term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (), - int (*nodem) (), int (*noder) ()) +term_iterate_deVar (Term term, int (*leaf) (Term t), int (*nodel) (Term t), + int (*nodem) (Term t), int (*noder) (Term t)) { term = deVar (term); if (term != NULL) @@ -1045,7 +1045,7 @@ term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (), * well. It is up to func to decide wether or not to recurse. */ int -term_iterate_leaves (const Term term, int (*func) ()) +term_iterate_leaves (const Term term, int (*func) (Term t)) { if (term != NULL) { @@ -1069,13 +1069,13 @@ term_iterate_leaves (const Term term, int (*func) ()) //! Iterate over open leaves (i.e. respect variable closure) int -term_iterate_open_leaves (const Term term, int (*func) ()) +term_iterate_open_leaves (const Term term, int (*func) (Term t)) { int testleaf (const Term t) { if (substVar (t)) { - return term_iterate_open_leaves (t, func); + return term_iterate_open_leaves (t->subst, func); } else { @@ -1427,3 +1427,22 @@ termHidelevel (const Term tsmall, Term tbig) } } } + +// Iterate over subterm constants of other runs in a term +// Callback should return true to progress. This is reported in the final thing. +int +iterateTermOther (const int myrun, Term t, int (*callback) (Term t)) +{ + int testOther (Term t) + { + int run; + + run = TermRunid (t); + if (run >= 0 && run != myrun) + { + return callback (t); + } + return true; + } + return term_iterate_deVar (t, testOther, NULL, NULL, NULL); +} diff --git a/src/term.h b/src/term.h index 6d47f01..2849eae 100644 --- a/src/term.h +++ b/src/term.h @@ -186,12 +186,14 @@ Term tupleProject (Term tt, int n); int termSize (Term t); float termDistance (Term t1, Term t2); int termOrder (Term t1, Term t2); -int term_iterate (const Term term, int (*leaf) (), int (*nodel) (), - int (*nodem) (), int (*noder) ()); -int term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (), - int (*nodem) (), int (*noder) ()); -int term_iterate_leaves (const Term t, int (*func) ()); -int term_iterate_open_leaves (const Term term, int (*func) ()); +int term_iterate (const Term term, int (*leaf) (Term t), + int (*nodel) (Term t), int (*nodem) (Term t), + int (*noder) (Term t)); +int term_iterate_deVar (Term term, int (*leaf) (Term t), + int (*nodel) (Term t), int (*nodem) (Term t), + int (*noder) (Term t)); +int term_iterate_leaves (const Term t, int (*func) (Term t)); +int term_iterate_open_leaves (const Term term, int (*func) (Term t)); void term_rolelocals_are_variables (); int term_encryption_level (const Term term); float term_constrain_level (const Term term); @@ -203,5 +205,6 @@ int isTermFunctionName (Term t); Term getTermFunction (Term t); unsigned int termHidelevel (const Term tsmall, Term tbig); +int iterateTermOther (const int myrun, Term t, int (*callback) (Term t)); #endif