From 95df010a5483fe1c0f889ac1bc9810489238f115 Mon Sep 17 00:00:00 2001 From: ccremers Date: Sun, 26 Feb 2006 17:18:59 +0000 Subject: [PATCH] - [[[ Broken commit ]]] More intermediate work. --- src/arachne.c | 169 ++++++++++++++++++++++++++++++++++++++++++++++++- src/binding.c | 13 +++- src/mgu.c | 128 +++++++++++++++++++++++++++++++++++++ src/mgu.h | 1 + src/system.c | 5 ++ src/termlist.c | 23 +++++++ src/termlist.h | 1 + 7 files changed, 338 insertions(+), 2 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 9a37f14..e15b55c 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -302,6 +302,18 @@ semiRunCreate (const Protocol p, const Role r) num_intruder_runs++; else num_regular_runs++; +#ifdef DEBUG + if (DEBUGL (5)) + { + globalError++; + eprintf ("Adding a run %i with semiRunCreate, ", sys->maxruns); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf ("\n"); + globalError--; + } +#endif roleInstance (sys, p, r, NULL, NULL); run = sys->maxruns - 1; sys->runs[run].height = 0; @@ -688,6 +700,19 @@ create_decryptor (const Term term, const Term key) Term tempkey; int run; +#ifdef DEBUG + if (DEBUGL (5)) + { + globalError++; + eprintf ("Creating decryptor for term "); + termPrint (term); + eprintf (" and key "); + termPrint (key); + eprintf ("\n"); + globalError--; + } +#endif + run = semiRunCreate (INTRUDER, I_RRSD); rd = sys->runs[run].start; rd->message = termDuplicateUV (term); @@ -731,6 +756,142 @@ getPriorityOfNeededKey (const System sys, const Term keyneeded) return prioritylevel; } +//! Try to bind a specific existing run to a 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. + * + * The key goals are bound to the goal. Iterates on success. + */ +int +bind_existing_to_goal (const Binding b, const int run, const int index) +{ + int old_length; + int flag; + int newgoals; + + int subterm_unification_needs (const Binding bt, Term tbig) + { + Term t; + int flag; + + int bind_iterate (Termlist tl) + { + if (goal_bind (bt, run, index)) + { + int flag; + + flag = iterate (); + goal_unbind (bt); + return flag; + } + return false; + } + + if (bt == NULL) + { + return false; + } + flag = false; + t = deVar (bt->term); + tbig = deVar (tbig); + + // First check whether it unifies in a simple way + flag = flag || unify (t, tbig, NULL, bind_iterate); + + // The other options are unification on subparts + if (realTermTuple (tbig)) + { + // Either one will do + return (subterm_unification_needs (bt, TermOp1 (tbig)) || + subterm_unification_needs (bt, TermOp1 (tbig))); + } + if (realTermEncrypt (tbig)) + { + Term keyneeded; + Roledef rddecrypt; + int smallrun; + int prioritylevel; + int newgoals; + Binding bnew; + + // 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; + + /* + * 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); + /* + * 3. Bind open goal to decryptor + */ + if (goal_bind (bt, smallrun, 2)) + { + // Allright, good binding, proceed with next + flag = flag || subterm_unification_needs (bnew, TermOp (tbig)); + goal_unbind (bt); + } + /* + * clean up + */ + termDelete (keyneeded); + goal_remove_last (newgoals); + semiRunDestroy (); + + return flag; + } + return false; + } + + old_length = sys->runs[run].height; + if ((index + 1) > old_length) + { + newgoals = add_read_goals (run, old_length, index + 1); + } + else + { + newgoals = 0; + } + flag = + subterm_unification_needs (b, + roledef_shift (sys->runs[run].start, + index)->message); + if (newgoals > 0) + { + goal_remove_last (newgoals); + } + sys->runs[run].height = old_length; + return flag; +} + //! Try to bind a specific existing run to a goal. /** * The key goals are bound to the goal. @@ -746,7 +907,7 @@ getPriorityOfNeededKey (const System sys, const Term keyneeded) *@param index index in run of binding start */ int -bind_existing_to_goal (const Binding b, const int run, const int index) +bind_existing_to_goal_old (const Binding b, const int run, const int index) { Roledef rd; int flag; @@ -1370,8 +1531,14 @@ bind_goal_regular_run (const Binding b) indentDepth++; // Bind to existing run +#ifdef DEBUG + debug (5, "Trying to bind to existing run."); +#endif sflag = bind_existing_run (b, p, r, index); // bind to new run +#ifdef DEBUG + debug (5, "Trying to bind to new run."); +#endif sflag = sflag && bind_new_run (b, p, r, index); indentDepth--; diff --git a/src/binding.c b/src/binding.c index 7ca250e..24e68f3 100644 --- a/src/binding.c +++ b/src/binding.c @@ -123,7 +123,18 @@ goal_bind (const Binding b, const int run, const int ev) { #ifdef DEBUG if (run >= sys->maxruns || sys->runs[run].step <= ev) - error ("Trying to bind to something not yet in the semistate."); + { + globalError++; + eprintf ("For term: "); + termPrint (b->term); + eprintf (" needed for r%ii%i.\n", b->run_to, b->ev_to); + eprintf ("Current limits: %i runs, %i events for this run.\n", + sys->maxruns, sys->runs[run].step); + globalError--; + error + ("trying to bind to something not yet in the semistate: r%ii%i.", + run, ev); + } #endif b->run_from = run; b->ev_from = ev; diff --git a/src/mgu.c b/src/mgu.c index a057455..5d30c0c 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -110,6 +110,134 @@ termlistSubstReset (Termlist tl) } } +//! Most general unifier iteration +/** + * Try to determine the most general unifier of two terms, if so calls function. + * + * The callback receives a list of variables, that were previously open, but are now closed + * in such a way that the two terms unify. Returns result of iteration, or false if not. + */ +int +unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist)) +{ + /* added for speed */ + t1 = deVar (t1); + t2 = deVar (t2); + if (t1 == t2) + return callback (tl); + + int callsubst (Termlist tl, Term t, Term tsubst) + { + int flag; + + t->subst = tsubst; +#ifdef DEBUG + showSubst (t); +#endif + tl = termlistAdd (tl, t); + flag = callback (tl); + tl = termlistDelTerm (tl); + t->subst = NULL; + return flag; + } + + if (!(hasTermVariable (t1) || hasTermVariable (t2))) + { + if (isTermEqual (t1, t2)) + { + return callback (tl); + } + else + { + return false; + } + } + + /* + * Distinguish a special case where both are unbound variables that will be + * connected, and I want to give one priority over the other for readability. + * + * Because t1 and t2 have been deVar'd means that if they are variables, they + * are also unbound. + */ + + if (realTermVariable (t1) && realTermVariable (t2) && goodsubst (t1, t2)) + { + /* Both are unbound variables. Decide. + * + * The plan: t1->subst will point to t2. But maybe we prefer the other + * way around? + */ + if (preferSubstitutionOrder (t2, t1)) + { + Term t3; + + // Swappy. + t3 = t1; + t1 = t2; + t2 = t3; + } + return callsubst (tl, t1, t2); + } + + /* symmetrical tests for single variable. + */ + + if (realTermVariable (t2)) + { + if (termSubTerm (t1, t2) || !goodsubst (t2, t1)) + return false; + else + { + return callsubst (tl, t2, t1); + } + } + if (realTermVariable (t1)) + { + if (termSubTerm (t2, t1) || !goodsubst (t1, t2)) + return false; + else + { + return callsubst (tl, t1, t2); + } + } + + /* left & right are compounds with variables */ + if (t1->type != t2->type) + return false; + + /* identical compound types */ + + /* encryption first */ + if (realTermEncrypt (t1)) + { + int unify_combined_enc (Termlist tl) + { + // now the keys are unified (subst in this tl) + // and we try the inner terms + return unify (TermOp (t1), TermOp (t2), tl, callback); + } + + return unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc); + } + + /* tupling second + non-associative version ! TODO other version */ + if (isTermTuple (t1)) + { + int unify_combined_tup (Termlist tl) + { + // now the keys are unified (subst in this tl) + // and we try the inner terms + return unify (TermOp2 (t1), TermOp2 (t2), tl, callback); + } + + return unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup); + } + return false; +} + + //! Most general unifier. /** * Try to determine the most general unifier of two terms. diff --git a/src/mgu.h b/src/mgu.h index 62ab659..93b0f6b 100644 --- a/src/mgu.h +++ b/src/mgu.h @@ -20,5 +20,6 @@ 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); +int unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist)); #endif diff --git a/src/system.c b/src/system.c index 30f17e3..7a5fcfa 100644 --- a/src/system.c +++ b/src/system.c @@ -823,6 +823,11 @@ roleInstanceArachne (const System sys, const Protocol protocol, /* length */ runs[rid].rolelength = roledef_length (runs[rid].start); + /* [[[ Hack ]]] this length is minimally 3 (to help the construction of the encryptors/decryptors from bare roledefs */ + if (runs[rid].rolelength < 3) + { + runs[rid].rolelength = 3; + } /* new graph to create */ dependPushRun (sys); diff --git a/src/termlist.c b/src/termlist.c index b10b574..6699fec 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -295,6 +295,29 @@ termlistConcat (Termlist tl1, Termlist tl2) return tl1; } +//! Concatenates two termlists. +/** + * Creates a completely new list that can be deleted. + * + * Note that the order is not preserved currently. + */ +Termlist +termlistConcatStatic (Termlist tl1, Termlist tl2) +{ + Termlist tl, tls; + + tl = NULL; + for (tls = tl1; tls != NULL; tls = tls->next) + { + tl = termlistAdd (tl, tls->term); + } + for (tls = tl2; tls != NULL; tls = tls->next) + { + tl = termlistAdd (tl, tls->term); + } + return tl; +} + //! Remove the pointed at element from the termlist. /** * Easier because of the double linked list. Note: does not do termDelete on the term. diff --git a/src/termlist.h b/src/termlist.h index 0df189e..ebbce82 100644 --- a/src/termlist.h +++ b/src/termlist.h @@ -36,6 +36,7 @@ Termlist termlistAdd (Termlist tl, Term term); Termlist termlistAppend (const Termlist tl, const Term term); Termlist termlistAddNew (const Termlist tl, const Term t); Termlist termlistConcat (Termlist tl1, Termlist tl2); +Termlist termlistConcatStatic (Termlist tl1, Termlist tl2); Termlist termlistDelTerm (Termlist tl); Termlist termlistConjunct (Termlist tl1, Termlist tl2); Termlist termlistConjunctType (Termlist tl1, Termlist tl2, int termtype);