From b2e40e07f35f7dc0752f185215bb42e9e2235f17 Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 22 Feb 2006 08:24:29 +0000 Subject: [PATCH] - Some more work on hidelevel backbone. - Added '--count-states' switch for the Arachne engine. --- src/arachne.c | 3 +++ src/compiler.c | 1 + src/hidelevel.c | 60 ++++++++++++++++++++++++++++++++++++++++++++ src/hidelevel.h | 11 ++++++++ src/main.c | 10 ++++++++ src/prune_bounds.c | 5 +++- src/prune_theorems.c | 4 ++- src/role.h | 5 ++++ src/switches.c | 16 ++++++++++++ src/switches.h | 1 + 10 files changed, 114 insertions(+), 2 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 9b7e012..34b849e 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -38,6 +38,7 @@ #include "prune_bounds.h" #include "prune_theorems.h" #include "arachne.h" +#include "hidelevel.h" extern int *graph; extern int nodes; @@ -1934,6 +1935,8 @@ iterate () */ 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) diff --git a/src/compiler.c b/src/compiler.c index 9e8941b..571ce11 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -449,6 +449,7 @@ claimCreate (const System sys, const Protocol protocol, const Role role, cl->complete = 0; cl->timebound = 0; cl->failed = 0; + cl->states = 0; cl->prec = NULL; cl->roles = NULL; cl->alwaystrue = false; diff --git a/src/hidelevel.c b/src/hidelevel.c index 8b04a61..d27c4e2 100644 --- a/src/hidelevel.c +++ b/src/hidelevel.c @@ -123,6 +123,40 @@ hidelevelCompute (const System sys) } } +//! Determine flag from parameters +unsigned int +hidelevelParamFlag (unsigned int l, unsigned int lmin, unsigned int lprot, + unsigned int lknow) +{ + // Given the parameters, determine where the term with hidelevel l could be generated from. + if (l < lmin) + { + return HLFLAG_NONE; + } + else + { + // One should work (at least) + if (l < lprot) + { + // Know should be possible + return HLFLAG_KNOW; + } + else + { + // Prot can, know also? + if (l < lknow) + { + // Nope, just prot + return HLFLAG_PROT; + } + else + { + // Both + return HLFLAG_BOTH; + } + } + } +} //! Given a term, iterate over all factors int @@ -185,3 +219,29 @@ hidelevelImpossible (const System sys, const Term goalterm) return !iterate_interesting (sys, goalterm, possible); } + +//! Return flag on the basis of the Hidelevel lemma +int +hidelevelFlag (const System sys, const Term goalterm) +{ + unsigned int flag; + + int getflag (unsigned int l, unsigned int lmin, unsigned int lprot, + unsigned int lknow) + { + // Determine new flag + flag = flag | hidelevelParamFlag (l, lmin, lprot, lknow); + + // Should we proceed? + if (flag == HLFLAG_NONE) + { + // abort iteration: it cannot get worse + return false; + } + return true; + } + + flag = HLFLAG_BOTH; + iterate_interesting (sys, goalterm, getflag); + return flag; +} diff --git a/src/hidelevel.h b/src/hidelevel.h index 40c61bc..b24d0a7 100644 --- a/src/hidelevel.h +++ b/src/hidelevel.h @@ -4,6 +4,17 @@ #include "term.h" #include "system.h" +/* + * Flags for hidelevel lemma + * + * Use binary or (|) to compose results: by default, a term can be satisfied by + * both the protocol and the initial knowledge. + */ +#define HLFLAG_BOTH 0 +#define HLFLAG_KNOW 1 +#define HLFLAG_PROT 2 +#define HLFLAG_NONE 3 + /* * The structure hiddenterm/Hiddenterm is defined in system.h */ diff --git a/src/main.c b/src/main.c index 7902cf9..a2098a1 100644 --- a/src/main.c +++ b/src/main.c @@ -559,6 +559,16 @@ timersPrint (const System sys) } } + /* states (if asked) */ + if (switches.engine == ARACHNE_ENGINE) + { + if (switches.countStates) + { + eprintf ("\tstates="); + statesFormat (cl_scan->states); + } + } + /* any warnings */ if (cl_scan->warnings) { diff --git a/src/prune_bounds.c b/src/prune_bounds.c index d725fab..a56135e 100644 --- a/src/prune_bounds.c +++ b/src/prune_bounds.c @@ -104,7 +104,10 @@ prune_bounds (const System sys) } // This needs some foundation. Probably * 2^max_encryption_level - //!@todo Fix this bound + //!@todo Remove later + /** + * This should be removed once the hidelevel lemma works correctly + */ if ((switches.match < 2) && (num_intruder_runs > ((double) switches.runs * max_encryption_level * 8))) diff --git a/src/prune_theorems.c b/src/prune_theorems.c index bce56c4..e2335bd 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -243,6 +243,7 @@ prune_theorems (const System sys) b = bl->data; // Check for "Hidden" interm goals + //!@TODO in the future, this can be subsumed by adding TERM_Hidden to the hidelevel constructs if (termInTerm (b->term, TERM_Hidden)) { // Prune the state: we can never meet this @@ -259,7 +260,7 @@ prune_theorems (const System sys) // Check for encryption levels /* * if (switches.match < 2 - *!@todo Doesn't work yet as desired for Tickets. Prove lemma first. + *!@TODO Doesn't work yet as desired for Tickets. Prove lemma first. */ if (switches.experimental) { @@ -283,6 +284,7 @@ prune_theorems (const System sys) // Check for SK-type function occurrences //!@todo Needs a LEMMA, although this seems to be quite straightforward to prove. // The idea is that functions are never sent as a whole, but only used in applications. + //!@TODO Subsumed by hidelevel lemma later if (isTermFunctionName (b->term)) { if (!inKnowledge (sys->know, b->term)) diff --git a/src/role.h b/src/role.h index cb7b25e..79ad2b7 100644 --- a/src/role.h +++ b/src/role.h @@ -12,6 +12,9 @@ enum eventtype { READ, SEND, CLAIM }; //! The container for the claim info list +/** + * Defaults are set in compiler.c (claimCreate) + */ struct claimlist { //! The type of claim @@ -33,6 +36,8 @@ struct claimlist states_t count; //! Number of occurrences that failed. states_t failed; + //! Number of iterations traversed for this claim. + states_t states; //! Whether the result is complete or not (failings always are!) int complete; //! If we ran into the time bound (incomplete, and bad for results) diff --git a/src/switches.c b/src/switches.c index 3080d06..91e8463 100644 --- a/src/switches.c +++ b/src/switches.c @@ -89,6 +89,7 @@ switchesInit (int argc, char **argv) switches.reportMemory = 0; switches.reportTime = 0; switches.reportStates = 0; + switches.countStates = false; // default off switches.extendNonReads = 0; // default off switches.extendTrivial = 0; // default off switches.plain = false; // default colors @@ -940,6 +941,21 @@ switcher (const int process, int index, int commandline) /* ================== * External options */ + if (detect (' ', "count-states", 0)) + { + if (!process) + { + /* not very important + helptext (" --count-states", "report on states (per claim)"); + */ + } + else + { + switches.countStates = true; + return index; + } + } + if (!process) printf ("Misc. switches:\n"); diff --git a/src/switches.h b/src/switches.h index 53e93d6..b4bcc4f 100644 --- a/src/switches.h +++ b/src/switches.h @@ -67,6 +67,7 @@ struct switchdata int reportMemory; //!< Memory display switch. int reportTime; //!< Time display switch. int reportStates; //!< Progress display switch. (traversed states) + int countStates; //!< Count states int extendNonReads; //!< Show further events in arachne xml output. int extendTrivial; //!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension) int plain; //!< Disable color output