From 881eccd6beb335e719b13bb16851c3535faac9b5 Mon Sep 17 00:00:00 2001 From: ccremers Date: Sun, 19 Mar 2006 12:59:26 +0000 Subject: [PATCH] - Fixed --disable-intruder: it now also uses no tupling shortcuts. --- src/arachne.c | 215 ++++++++++++++++++++++++++++---------------------- src/binding.c | 29 ++++++- src/mgu.c | 66 ++++++++-------- 3 files changed, 178 insertions(+), 132 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 28a5658..2fcdacd 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -1193,7 +1193,7 @@ bind_goal_new_m0 (const Binding b) Termlist subst; m0t = tl->term; - subst = termMguTerm (b->term, m0t); + subst = termMguTerm (b->term, m0t); //! @todo This needs to be replace by the iterator one, but works for now if (subst != MGUFAIL) { int run; @@ -1296,7 +1296,7 @@ bind_goal_new_encrypt (const Binding b) { Term t1, t2; - if (!realTermEncrypt (term)) + if (switches.intruder && (!realTermEncrypt (term))) { // tuple construction error ("Goal that is a tuple should not occur!"); @@ -1407,20 +1407,21 @@ bind_goal_regular_run (const Binding b) int flag; int found; - int test_sub_unification (Termlist substlist, Termlist keylist) - { - // A unification exists; return the signal - return 0; - } /* * This is a local function so we have access to goal */ int bind_this_role_send (Protocol p, Role r, Roledef rd, int index) { + int test_sub_unification (Termlist substlist, Termlist keylist) + { + // A unification exists; return the signal + return false; + } + if (p == INTRUDER) { // No intruder roles here - return 1; + return true; } // Test for interm unification @@ -1437,9 +1438,8 @@ bind_goal_regular_run (const Binding b) eprintf (", index %i\n", index); } #endif - if (!termMguSubTerm - (b->term, rd->message, test_sub_unification, sys->know->inverses, - NULL)) + if (!subtermUnify + (rd->message, b->term, NULL, NULL, test_sub_unification)) { int sflag; @@ -1482,7 +1482,7 @@ bind_goal_regular_run (const Binding b) } else { - return 1; + return true; } } @@ -2004,6 +2004,112 @@ select_tuple_goal () } +//! Iterate a binding +/** + * For DY model, we unfold any tuples first, otherwise we skip that. + */ +int +iterateOneBinding (void) +{ + Binding btup; + int flag; + + // marker + flag = true; + + // Are there any tuple goals? + if (switches.intruder) + { + // Maybe... (well, test) + btup = select_tuple_goal (); + } + else + { + // No, there are non that need to be expanded (no intruder) + btup = NULL; + } + if (btup != NULL) + { + /* Substitution or something resulted in a tuple goal: we immediately split them into compounds. + */ + Term tuple; + + tuple = deVar (btup->term); + if (realTermTuple (tuple)) + { + int count; + Term tupletermbuffer; + + tupletermbuffer = btup->term; + /* + * We solve this by replacing the tuple goal by the left term, and adding a goal for the right term. + */ + btup->term = TermOp1 (tuple); + count = + goal_add (TermOp2 (tuple), btup->run_to, + btup->ev_to, btup->level); + + // Show this in output + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Expanding tuple goal "); + termPrint (tupletermbuffer); + eprintf (" into %i subgoals.\n", count); + } + + // iterate + flag = iterate (); + + // undo + goal_remove_last (count); + btup->term = tupletermbuffer; + } + } + else + { + // No tuple goals; good + Binding b; + + /** + * Not pruned: count + */ + + sys->states = statesIncrease (sys->states); + sys->current_claim->states = + statesIncrease (sys->current_claim->states); + + /** + * Check whether its a final state (i.e. all goals bound) + */ + + b = (Binding) select_goal (sys); + if (b == NULL) + { + /* + * all goals bound, check for property + */ + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("All goals are now bound.\n"); + } + sys->claims = statesIncrease (sys->claims); + sys->current_claim->count = + statesIncrease (sys->current_claim->count); + flag = property_check (sys); + } + else + { + /* + * bind this goal in all possible ways and iterate + */ + flag = bind_goal_all_options (b); + } + } + return flag; +} + //! Main recursive procedure for Arachne int iterate () @@ -2018,89 +2124,8 @@ iterate () { if (!prune_bounds (sys)) { - Binding btup; - - // Are there any tuple goals? - btup = select_tuple_goal (); - if (btup != NULL) - { - /* Substitution or something resulted in a tuple goal: we immediately split them into compounds. - */ - Term tuple; - - tuple = deVar (btup->term); - if (realTermTuple (tuple)) - { - int count; - Term tupletermbuffer; - - tupletermbuffer = btup->term; - /* - * We solve this by replacing the tuple goal by the left term, and adding a goal for the right term. - */ - btup->term = TermOp1 (tuple); - count = - goal_add (TermOp2 (tuple), btup->run_to, - btup->ev_to, btup->level); - - // Show this in output - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Expanding tuple goal "); - termPrint (tupletermbuffer); - eprintf (" into %i subgoals.\n", count); - } - - // iterate - flag = iterate (); - - // undo - goal_remove_last (count); - btup->term = tupletermbuffer; - } - } - else - { - // No tuple goals; good - Binding b; - - /** - * Not pruned: count - */ - - sys->states = statesIncrease (sys->states); - sys->current_claim->states = - statesIncrease (sys->current_claim->states); - - /** - * Check whether its a final state (i.e. all goals bound) - */ - - b = (Binding) select_goal (sys); - if (b == NULL) - { - /* - * all goals bound, check for property - */ - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("All goals are now bound.\n"); - } - sys->claims = statesIncrease (sys->claims); - sys->current_claim->count = - statesIncrease (sys->current_claim->count); - flag = property_check (sys); - } - else - { - /* - * bind this goal in all possible ways and iterate - */ - flag = bind_goal_all_options (b); - } - } + // Go and pick a binding for iteration + flag = iterateOneBinding (); } else { diff --git a/src/binding.c b/src/binding.c index 6b3be70..8302104 100644 --- a/src/binding.c +++ b/src/binding.c @@ -234,8 +234,9 @@ goal_add (Term term, const int run, const int ev, const int level) error ("Trying to add a goal for an event that is not in the semistate yet."); #endif - if (realTermTuple (term)) + if (switches.intruder && realTermTuple (term)) { + // Only split if there is an intruder return goal_add (TermOp1 (term), run, ev, level) + goal_add (TermOp2 (term), run, ev, level); } @@ -459,7 +460,16 @@ unique_origination () { Termlist terms2, sharedterms; - terms2 = tuple_to_termlist (b2->term); + if (switches.intruder) + { + // For intruder we work with sets here + terms2 = tuple_to_termlist (b2->term); + } + else + { + // For regular agents we use terms + terms2 = termlistAdd (NULL, b2->term); + } sharedterms = termlistConjunct (terms, terms2); // Compare terms @@ -529,11 +539,22 @@ bindings_c_minimal () { // this node is *before* the from node Roledef rd; + int occursthere; rd = roledef_shift (sys->runs[run].start, ev); - if (termInTerm (rd->message, b->term)) + if (switches.intruder) { - // This term already occurs as interm in a previous node! + // intruder: interm bindings should cater for the first occurrence + occursthere = termInTerm (rd->message, b->term); + } + else + { + // no intruder, then simple test + occursthere = isTermEqual (rd->message, b->term); + } + if (occursthere) + { + // This term already occurs in a previous node! #ifdef DEBUG if (DEBUGL (4)) { diff --git a/src/mgu.c b/src/mgu.c index 318d06d..343afac 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -7,6 +7,7 @@ #include "type.h" #include "debug.h" #include "specialterm.h" +#include "switches.h" /* Most General Unifier @@ -123,15 +124,12 @@ termlistSubstReset (Termlist tl) 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) { - return proceed && callback (tl); + return callback (tl); } int callsubst (Termlist tl, Term t, Term tsubst) @@ -155,12 +153,12 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist)) if (isTermEqual (t1, t2)) { // Equal! - return proceed && callback (tl); + return callback (tl); } else { // Can never be fixed, no variables - return proceed; + return true; } } @@ -188,7 +186,7 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist)) t1 = t2; t2 = t3; } - return proceed && callsubst (tl, t1, t2); + return callsubst (tl, t1, t2); } /* symmetrical tests for single variable. @@ -197,25 +195,25 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist)) if (realTermVariable (t2)) { if (termSubTerm (t1, t2) || !goodsubst (t2, t1)) - return proceed; + return true; else { - return proceed && callsubst (tl, t2, t1); + return callsubst (tl, t2, t1); } } if (realTermVariable (t1)) { if (termSubTerm (t2, t1) || !goodsubst (t1, t2)) - return proceed; + return true; else { - return proceed && callsubst (tl, t1, t2); + return callsubst (tl, t1, t2); } } /* left & right are compounds with variables */ if (t1->type != t2->type) - return proceed; + return true; /* identical compound types */ @@ -229,8 +227,7 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist)) return unify (TermOp (t1), TermOp (t2), tl, callback); } - return proceed - && unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc); + return unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc); } /* tupling second @@ -243,11 +240,10 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist)) // and we try the inner terms return unify (TermOp2 (t1), TermOp2 (t2), tl, callback); } - return proceed - && unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup); + return unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup); } - return proceed; + return true; } @@ -286,24 +282,28 @@ subtermUnify (Term tbig, Term tsmall, Termlist tl, Termlist keylist, proceed = proceed && unify (tbig, tsmall, tl, keycallback); // [2/3]: complex - // 2. interm unification - if (realTermTuple (tbig)) + if (switches.intruder) { - proceed = proceed - && subtermUnify (TermOp1 (tbig), tsmall, tl, keylist, callback); - proceed = proceed - && subtermUnify (TermOp2 (tbig), tsmall, tl, keylist, callback); - } + // 2. interm unification + // Only if there is an intruder + 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); + // 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; }