From e6505a72a3b1ae65976e6805192081826acdfd19 Mon Sep 17 00:00:00 2001 From: ccremers Date: Mon, 2 Jan 2006 19:55:34 +0000 Subject: [PATCH] - Further refactoring. - Some cleanup. --- src/arachne.c | 114 +----------------------------------------------- src/claim.c | 97 ++++++++++++++++++++++++++++++++++++++++ src/claim.h | 4 ++ src/heuristic.c | 1 + src/symbol.c | 2 +- src/term.c | 26 +++++++++++ src/term.h | 3 ++ 7 files changed, 134 insertions(+), 113 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 16cec02..25fef0d 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -235,32 +235,6 @@ binding_indent_print (const Binding b, const int flag) eprintf ("\n"); } -//! Determine whether a term is a functor -int -isTermFunctionName (Term t) -{ - t = deVar (t); - if (t != NULL && isTermLeaf (t) && t->stype != NULL - && inTermlist (t->stype, TERM_Function)) - return 1; - return 0; -} - -//! Determine whether a term is a function application. Returns the function term. -Term -getTermFunction (Term t) -{ - t = deVar (t); - if (t != NULL) - { - if (realTermEncrypt (t) && isTermFunctionName (TermKey (t))) - { - return TermKey (t); - } - } - return NULL; -} - //! Keylevel tester: can this term ever be sent at this keylevel? int isKeylevelRight (Term t, const int kl) @@ -1892,90 +1866,6 @@ bind_goal (const Binding b) } } -//! 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. - * - *@returns true iff this state is invalid for some reason - */ -int -prune_claim_specifics () -{ - if (sys->current_claim->type == CLAIM_Niagree) - { - if (arachne_claim_niagree (sys, 0, sys->current_claim->ev)) - { - sys->current_claim->count = - statesIncrease (sys->current_claim->count); - if (switches.output == PROOF) - { - indentPrint (); - eprintf - ("Pruned: niagree holds in this part of the proof tree.\n"); - } - return 1; - } - } - if (sys->current_claim->type == CLAIM_Nisynch) - { - if (arachne_claim_nisynch (sys, 0, sys->current_claim->ev)) - { - sys->current_claim->count = - statesIncrease (sys->current_claim->count); - if (switches.output == PROOF) - { - indentPrint (); - eprintf - ("Pruned: nisynch holds in this part of the proof tree.\n"); - } - return 1; - } - } - return 0; -} - -//! Setup system for specific claim test -add_claim_specifics (const Claimlist cl, const Roledef rd) -{ - if (cl->type == CLAIM_Secret) - { - /** - * Secrecy claim - */ - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("* To verify the secrecy claim, we add the term "); - termPrint (rd->message); - eprintf (" as a goal.\n"); - indentPrint (); - eprintf - ("* If all goals can be bound, this constitutes an attack.\n"); - } - - /** - * We say that a state exists for secrecy, but we don't really test wheter the claim can - * 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 - } - - if (cl->type == CLAIM_Reachable) - { - if (switches.check) - { - // For reachability claims in check mode, we restrict the number of runs to the number of roles of this protocol - Protocol protocol; - int rolecount; - - protocol = (Protocol) cl->protocol; - rolecount = termlistLength (protocol->rolenames); - switches.runs = rolecount; - } - } -} - //! Count a false claim /** * Counts global attacks as well as claim instances. @@ -2326,7 +2216,7 @@ iterate () flag = 1; if (!prune_theorems (sys)) { - if (!prune_claim_specifics ()) + if (!prune_claim_specifics (sys)) { if (!prune_bounds (sys)) { @@ -2582,7 +2472,7 @@ arachne () /** * Add specific goal info */ - add_claim_specifics (cl, + add_claim_specifics (sys, cl, roledef_shift (sys->runs[run].start, cl->ev)); diff --git a/src/claim.c b/src/claim.c index 2a41cd5..e56c5ab 100644 --- a/src/claim.c +++ b/src/claim.c @@ -1,10 +1,22 @@ +/** + * + *@file claim.c + * + * Claim handling for the Arachne engine. + * + */ + #include + #include "termmap.h" #include "system.h" #include "label.h" #include "error.h" #include "debug.h" #include "binding.h" +#include "arachne.h" +#include "specialterm.h" +#include "switches.h" #define MATCH_NONE 0 #define MATCH_ORDER 1 @@ -675,3 +687,88 @@ arachne_claim_nisynch (const System sys, const int claim_run, { return arachne_claim_authentications (sys, claim_run, claim_index, 1); } + +//! 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. + * + *@returns true iff this state is invalid for some reason + */ +int +prune_claim_specifics (const System sys) +{ + if (sys->current_claim->type == CLAIM_Niagree) + { + if (arachne_claim_niagree (sys, 0, sys->current_claim->ev)) + { + sys->current_claim->count = + statesIncrease (sys->current_claim->count); + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned: niagree holds in this part of the proof tree.\n"); + } + return 1; + } + } + if (sys->current_claim->type == CLAIM_Nisynch) + { + if (arachne_claim_nisynch (sys, 0, sys->current_claim->ev)) + { + sys->current_claim->count = + statesIncrease (sys->current_claim->count); + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned: nisynch holds in this part of the proof tree.\n"); + } + return 1; + } + } + return 0; +} + +//! Setup system for specific claim test +void +add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd) +{ + if (cl->type == CLAIM_Secret) + { + /** + * Secrecy claim + */ + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("* To verify the secrecy claim, we add the term "); + termPrint (rd->message); + eprintf (" as a goal.\n"); + indentPrint (); + eprintf + ("* If all goals can be bound, this constitutes an attack.\n"); + } + + /** + * We say that a state exists for secrecy, but we don't really test wheter the claim can + * 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 + } + + if (cl->type == CLAIM_Reachable) + { + if (switches.check) + { + // For reachability claims in check mode, we restrict the number of runs to the number of roles of this protocol + Protocol protocol; + int rolecount; + + protocol = (Protocol) cl->protocol; + rolecount = termlistLength (protocol->rolenames); + switches.runs = rolecount; + } + } +} diff --git a/src/claim.h b/src/claim.h index c1c0f94..bf5ee71 100644 --- a/src/claim.h +++ b/src/claim.h @@ -8,4 +8,8 @@ int arachne_claim_niagree (const System sys, const int claim_run, 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); + #endif diff --git a/src/heuristic.c b/src/heuristic.c index d18d3e0..b5172eb 100644 --- a/src/heuristic.c +++ b/src/heuristic.c @@ -416,4 +416,5 @@ select_goal (const System sys) } error ("Unknown value (<0) for --goal-select."); } + return NULL; } diff --git a/src/symbol.c b/src/symbol.c index c12cbdb..08954a1 100644 --- a/src/symbol.c +++ b/src/symbol.c @@ -46,7 +46,7 @@ symbolsInit (void) symb_list = NULL; symb_alloc = NULL; globalError = 0; - globalStream = stdout; + globalStream = (char *) stdout; } //! Close symbols code. diff --git a/src/term.c b/src/term.c index c170358..cb77890 100644 --- a/src/term.c +++ b/src/term.c @@ -1352,3 +1352,29 @@ freshTermPrefix (Term prefixterm) freshsymbol = symbolNextFree (prefixsymbol); return makeTermType (GLOBAL, freshsymbol, -1); } + +//! Determine whether a term is a functor +int +isTermFunctionName (Term t) +{ + t = deVar (t); + if (t != NULL && isTermLeaf (t) && t->stype != NULL + && inTermlist (t->stype, TERM_Function)) + return 1; + return 0; +} + +//! Determine whether a term is a function application. Returns the function term. +Term +getTermFunction (Term t) +{ + t = deVar (t); + if (t != NULL) + { + if (realTermEncrypt (t) && isTermFunctionName (TermKey (t))) + { + return TermKey (t); + } + } + return NULL; +} diff --git a/src/term.h b/src/term.h index f12fcb2..0428ba1 100644 --- a/src/term.h +++ b/src/term.h @@ -197,5 +197,8 @@ void term_set_keylevels (const Term term); void termPrintDiff (Term t1, Term t2); int isLeafNameEqual (Term t1, Term t2); Term freshTermPrefix (Term prefixterm); +int isTermFunctionName (Term t); +Term getTermFunction (Term t); + #endif