From 5c15c21832caa14d5e171631a421c9c821ed896e Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 19 Aug 2004 13:09:35 +0000 Subject: [PATCH] - Reports on completeness of proofs. --- src/arachne.c | 160 +++++++++++++++++++++++++++++-------------------- src/compiler.c | 1 + src/main.c | 15 ++++- src/role.h | 3 + 4 files changed, 112 insertions(+), 67 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 28cac63..67d0ada 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -167,31 +167,33 @@ binding_indent_print (Binding b, int flag) /** *@return Returns the run number */ -int semiRunCreate (const Protocol p, const Role r) +int +semiRunCreate (const Protocol p, const Role r) { int run; run = sys->maxruns; if (p == INTRUDER) - num_intruder_runs++; + num_intruder_runs++; else - num_regular_runs++; + num_regular_runs++; roleInstance (sys, p, r, NULL, NULL); sys->runs[run].length = 0; return run; } //! Wrapper for roleDestroy -void semiRunDestroy () +void +semiRunDestroy () { Protocol p; - p = sys->runs[sys->maxruns-1].protocol; + p = sys->runs[sys->maxruns - 1].protocol; roleInstanceDestroy (sys); if (p == INTRUDER) - num_intruder_runs--; + num_intruder_runs--; else - num_regular_runs--; + num_regular_runs--; } //! After a role instance, or an extension of a run, we might need to add some goals @@ -528,7 +530,8 @@ bind_existing_to_goal (const Binding b, const int run, const int index) indentPrint (); eprintf ("Cannot bind "); termPrint (b->term); - eprintf (" to run %i, index %i because it does not subterm-unify.\n", run, index); + eprintf (" to run %i, index %i because it does not subterm-unify.\n", + run, index); } // Reset length remove_read_goals (newgoals); @@ -931,7 +934,8 @@ bind_goal_regular_run (const Binding b) indentPrint (); eprintf ("The term ", found); termPrint (b->term); - eprintf (" matches patterns from the role definitions. Investigate.\n"); + eprintf + (" matches patterns from the role definitions. Investigate.\n"); } if (sys->output == PROOF) { @@ -999,11 +1003,12 @@ bind_goal_old_intruder_run (Binding b) if (sys->output == PROOF && found == 1) { indentPrint (); - eprintf ("Suppose it is from an existing intruder run.\n"); + eprintf + ("Suppose it is from an existing intruder run.\n"); } - indentDepth++; + indentDepth++; flag = flag && bind_existing_to_goal (b, run, ev); - indentDepth--; + indentDepth--; } rd = rd->next; ev++; @@ -1040,37 +1045,16 @@ bind_goal (const Binding b) } } -//! Prune determination +//! Prune determination because of theorems /** - *@returns true iff this state is invalid for some reason + *@returns true iff this state is invalid because of a theorem */ int -prune () +prune_theorems () { Termlist tl; List bl; - if (indentDepth > 20) - { - // Hardcoded limit on iterations - if (sys->output == PROOF) - { - indentPrint (); - eprintf ("Pruned because too many iteration levels.\n"); - } - return 1; - } - if (sys->maxruns > sys->switchRuns) - { - // Hardcoded limit on runs - if (sys->output == PROOF) - { - indentPrint (); - eprintf ("Pruned because too many runs.\n"); - } - return 1; - } - // Check if all agents are valid tl = sys->runs[0].agents; while (tl != NULL) @@ -1145,6 +1129,39 @@ prune () return 0; } +//! Prune determination for bounds +/** + *@returns true iff this state is invalid for some reason + */ +int +prune_bounds () +{ + Termlist tl; + List bl; + + if (indentDepth > 20) + { + // Hardcoded limit on iterations + if (sys->output == PROOF) + { + indentPrint (); + eprintf ("Pruned because too many iteration levels.\n"); + } + return 1; + } + if (num_regular_runs > sys->switchRuns) + { + // Hardcoded limit on runs + if (sys->output == PROOF) + { + indentPrint (); + eprintf ("Pruned because too many regular runs.\n"); + } + return 1; + } + return 0; +} + //! Setup system for specific claim test add_claim_specifics (const Claimlist cl, const Roledef rd) { @@ -1163,6 +1180,12 @@ add_claim_specifics (const Claimlist cl, const Roledef rd) 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); // Assumption that all claims are in run 0 } } @@ -1205,41 +1228,49 @@ iterate () int flag; flag = 1; - if (!prune ()) + if (!prune_theorems ()) { - Binding b; - - /** - * Not pruned: count - */ - - sys->states = statesIncrease (sys->states); - - /** - * Check whether its a final state (i.e. all goals bound) - */ - - b = select_goal (); - if (b == NULL) + if (!prune_bounds ()) { - /* - * all goals bound, check for property + Binding b; + + /** + * Not pruned: count */ - if (sys->output == PROOF) + + sys->states = statesIncrease (sys->states); + + /** + * Check whether its a final state (i.e. all goals bound) + */ + + b = select_goal (); + if (b == NULL) { - indentPrint (); - eprintf ("All goals are now bound.\n"); + /* + * all goals bound, check for property + */ + if (sys->output == PROOF) + { + indentPrint (); + eprintf ("All goals are now bound.\n"); + } + sys->claims = statesIncrease (sys->claims); + current_claim->count = statesIncrease (current_claim->count); + flag = property_check (); + } + else + { + /* + * bind this goal in all possible ways and iterate + */ + flag = bind_goal (b); } - sys->claims = statesIncrease (sys->claims); - current_claim->count = statesIncrease (current_claim->count); - flag = flag && property_check (); } else { - /* - * bind this goal in all possible ways and iterate - */ - flag = bind_goal (b); + // Pruned because of bound! + current_claim->complete = 0; } } @@ -1324,6 +1355,7 @@ arachne () int run; current_claim = cl; + cl->complete = 1; p = (Protocol) cl->protocol; r = (Role) cl->role; @@ -1339,7 +1371,7 @@ arachne () eprintf (" at index %i.\n", cl->ev); } indentDepth++; - run = semiRunCreate (p,r); + run = semiRunCreate (p, r); proof_suppose_run (run, 0, cl->ev + 1); add_read_goals (run, 0, cl->ev + 1); diff --git a/src/compiler.c b/src/compiler.c index 8bdcaac..3ddd37a 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -477,6 +477,7 @@ commEvent (int event, Tac tc) cl->role = thisRole; cl->roledef = NULL; cl->count = 0; + cl->complete = 0; cl->failed = 0; cl->prec = NULL; cl->next = sys->claimlist; diff --git a/src/main.c b/src/main.c index b8e946b..b11296d 100644 --- a/src/main.c +++ b/src/main.c @@ -92,7 +92,8 @@ main (int argc, char **argv) "output file (default is stdout)"); struct arg_lit *switch_arachne = arg_lit0 ("a", "arachne", "use Arachne engine"); - struct arg_lit *switch_proof = arg_lit0 ("P", "proof", "generate proof output"); + struct arg_lit *switch_proof = + arg_lit0 ("P", "proof", "generate proof output"); struct arg_str *switch_check = arg_str0 (NULL, "check", "CLAIM", "claim type to check (default is all)"); struct arg_int *switch_scenario = arg_int0 ("s", "scenario", NULL, @@ -362,7 +363,7 @@ main (int argc, char **argv) } /* handle switches */ - + sys->switchRuns = switch_maximum_runs->ival[0]; /* maximum number of runs */ if (switch_implicit_choose->count > 0) /* allow implicit chooses */ @@ -389,7 +390,7 @@ main (int argc, char **argv) if (switch_summary->count > 0) sys->output = SUMMARY; /* report summary on stdout */ if (switch_proof->count > 0) - sys->output = PROOF; /* report proof on stdout (for arachne only) */ + sys->output = PROOF; /* report proof on stdout (for arachne only) */ /* * The scenario selector has an important side effect; when it is non-null, @@ -775,6 +776,14 @@ timersPrint (const System sys) eprintf ("failed:\t"); statesFormat (cl_scan->failed); } + else + { + eprintf ("\tcorrect: "); + if (cl_scan->complete) + eprintf ("complete proof"); + else + eprintf ("bounded proof"); + } } eprintf ("\n"); cl_scan = cl_scan->next; diff --git a/src/role.h b/src/role.h index 3a98388..bee51d8 100644 --- a/src/role.h +++ b/src/role.h @@ -30,6 +30,9 @@ struct claimlist states_t count; //! Number of occurrences that failed. states_t failed; + //! Whether the result is complete or not (failings always are!) + int complete; + int r; //!< role number for mapping int ev; //!< event index in role //! Preceding label list