From d2058d937b5623516199c7862034f5b261ad67b5 Mon Sep 17 00:00:00 2001 From: ccremers Date: Sun, 2 Apr 2006 12:29:02 +0000 Subject: [PATCH] - Revised cost heuristic. Trace length is no longer the real optimization. --- src/arachne.c | 18 ++++++++---------- src/binding.c | 20 ++++++++++++++++++++ src/binding.h | 1 + src/cost.c | 12 ++++++++---- src/prune_bounds.c | 11 +++++------ src/system.c | 2 ++ src/system.h | 2 ++ 7 files changed, 46 insertions(+), 20 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 2b8a00e..c504077 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -57,8 +57,6 @@ Role I_RRSD; //!< Decrypt role of the intruder int proofDepth; //!< Current depth of the proof int max_encryption_level; //!< Maximum encryption level of any term -int num_regular_runs; //!< Current number of regular runs -int num_intruder_runs; //!< Current number of intruder runs static int indentDepth; static int prevIndentDepth; @@ -132,8 +130,8 @@ arachneInit (const System mysys) add_event (SEND, NULL); I_RRSD = add_role ("I_D: Decrypt"); - num_regular_runs = 0; - num_intruder_runs = 0; + sys->num_regular_runs = 0; + sys->num_intruder_runs = 0; max_encryption_level = 0; indentDepth = 0; @@ -309,9 +307,9 @@ semiRunCreate (const Protocol p, const Role r) int run; if (p == INTRUDER) - num_intruder_runs++; + sys->num_intruder_runs++; else - num_regular_runs++; + sys->num_regular_runs++; #ifdef DEBUG if (DEBUGL (5)) { @@ -341,9 +339,9 @@ semiRunDestroy () p = sys->runs[sys->maxruns - 1].protocol; roleInstanceDestroy (sys); if (p == INTRUDER) - num_intruder_runs--; + sys->num_intruder_runs--; else - num_regular_runs--; + sys->num_regular_runs--; } } @@ -2277,8 +2275,8 @@ arachne () error ("Something is wrong, number of runs >0."); } - num_regular_runs = 0; - num_intruder_runs = 0; + sys->num_regular_runs = 0; + sys->num_intruder_runs = 0; max_encryption_level = 0; iterate_role_events (determine_encrypt_max); diff --git a/src/binding.c b/src/binding.c index 8302104..50f7226 100644 --- a/src/binding.c +++ b/src/binding.c @@ -588,3 +588,23 @@ bindings_c_minimal () } return true; } + +//! Count the number of bindings that are done. +int +countBindingsDone () +{ + int count; + + int countDone (Binding b) + { + if (b->done) + { + count++; + } + return true; + } + + count = 0; + iterate_bindings (countDone); + return count; +} diff --git a/src/binding.h b/src/binding.h index 0ff5d51..34bb8b8 100644 --- a/src/binding.h +++ b/src/binding.h @@ -48,5 +48,6 @@ int iterate_preceding_bindings (const int run, const int ev, int (*func) (Binding b)); int bindings_c_minimal (); +int countBindingsDone (); #endif diff --git a/src/cost.c b/src/cost.c index 38e6adf..48459ff 100644 --- a/src/cost.c +++ b/src/cost.c @@ -32,10 +32,14 @@ attackCost (const System sys) cost = 0; - cost += get_semitrace_length (); - cost += 8 * selfInitiators (sys); - cost += 4 * selfResponders (sys); - cost += 2 * countInitiators (sys); + //cost += get_semitrace_length (); + + cost += 10 * selfInitiators (sys); + cost += 7 * selfResponders (sys); + cost += 4 * sys->num_regular_runs; + cost += 3 * countInitiators (sys); + cost += 2 * countBindingsDone (); + cost += 1 * sys->num_intruder_runs; return cost; } diff --git a/src/prune_bounds.c b/src/prune_bounds.c index 4e56d59..4db30f5 100644 --- a/src/prune_bounds.c +++ b/src/prune_bounds.c @@ -17,8 +17,6 @@ extern int attack_leastcost; extern Protocol INTRUDER; extern int proofDepth; extern int max_encryption_level; -extern int num_regular_runs; -extern int num_intruder_runs; //! Prune determination for bounds /** @@ -92,13 +90,14 @@ prune_bounds (const System sys) } } - if (num_regular_runs > switches.runs) + if (sys->num_regular_runs > switches.runs) { // Hardcoded limit on runs if (switches.output == PROOF) { indentPrint (); - eprintf ("Pruned: too many regular runs (%i).\n", num_regular_runs); + eprintf ("Pruned: too many regular runs (%i).\n", + sys->num_regular_runs); } return 1; } @@ -111,7 +110,7 @@ prune_bounds (const System sys) if (switches.experimental & 1) { if ((switches.match < 2) - && (num_intruder_runs > + && (sys->num_intruder_runs > ((double) switches.runs * max_encryption_level * 8))) { // Hardcoded limit on iterations @@ -120,7 +119,7 @@ prune_bounds (const System sys) indentPrint (); eprintf ("Pruned: %i intruder runs is too much. (max encr. level %i)\n", - num_intruder_runs, max_encryption_level); + sys->num_intruder_runs, max_encryption_level); } return 1; } diff --git a/src/system.c b/src/system.c index 99fc117..b8c8897 100644 --- a/src/system.c +++ b/src/system.c @@ -107,6 +107,8 @@ systemReset (const System sys) termlistDestroy (sys->secrets); // remove old secrets list sys->secrets = NULL; // list of claimed secrets + sys->num_intruder_runs = 0; // number of intruder runs + sys->num_regular_runs = 0; // number of regular runs /* transfer switches */ sys->maxtracelength = switches.maxtracelength; diff --git a/src/system.h b/src/system.h index 1288711..0a0e1c6 100644 --- a/src/system.h +++ b/src/system.h @@ -121,6 +121,8 @@ struct system states_t failed; //!< Number of claims failed. int attackid; //!< Global counter of attacks (used for assigning identifiers) within this Scyther call. int countScenario; //!< Number of scenarios skipped. + int num_regular_runs; //!< Number of regular runs + int num_intruder_runs; //!< Number of intruder runs /* protocol definition */ Protocol protocols; //!< List of protocols in the system