From 921c82876dcd9580799a033fc91ea1ac8dcc62ae Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 22 Feb 2006 09:53:50 +0000 Subject: [PATCH] - experimental=4 now disables some things. Weirdly enough, they don't seem to make much difference. --- src/arachne.c | 36 ++++++++++++++++-------------- src/prune_bounds.c | 23 +++++++++++--------- src/prune_theorems.c | 52 ++++++++++++++++++++++++-------------------- src/switches.c | 2 ++ 4 files changed, 64 insertions(+), 49 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 34b849e..3ceefe9 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -278,8 +278,9 @@ isKeylevelRight (Term t, const int kl) //! Keylevel tester: can this term ever be sent at this keylevel? /** - * Depends on the keylevel lemma (TODO) and the keylevel constructors in symbol.c - * The idea is that certain terms will never be sent. + * Depends on the keylevel lemma (so this will not be called when those lemmas + * are disabled) and the keylevel constructors in symbol.c The idea is that + * certain terms will never be sent. */ int isPossiblySent (Term t) @@ -1512,25 +1513,28 @@ bind_goal (const Binding b) } } - // Keylevel lemmas: improves on the previous one - if (!isPossiblySent (b->term)) + if (switches.experimental & 4 == 0) { - if (switches.output == PROOF) + // Keylevel lemmas: improves on the previous one + if (!isPossiblySent (b->term)) { - eprintf - ("Rejecting a term as a regular bind because key levels are off: "); - termPrint (b->term); - if (know_only) + if (switches.output == PROOF) { - eprintf (" [in accordance with function lemma]"); + eprintf + ("Rejecting a term as a regular bind because key levels are off: "); + termPrint (b->term); + if (know_only) + { + eprintf (" [in accordance with function lemma]"); + } + else + { + eprintf (" [stronger than function lemma]"); + } + eprintf ("\n"); } - else - { - eprintf (" [stronger than function lemma]"); - } - eprintf ("\n"); + know_only = 1; } - know_only = 1; } #ifdef DEBUG else diff --git a/src/prune_bounds.c b/src/prune_bounds.c index a56135e..2d669ca 100644 --- a/src/prune_bounds.c +++ b/src/prune_bounds.c @@ -108,19 +108,22 @@ prune_bounds (const System sys) /** * This should be removed once the hidelevel lemma works correctly */ - if ((switches.match < 2) - && (num_intruder_runs > - ((double) switches.runs * max_encryption_level * 8))) + if (switches.experimental & 4 == 0) { - // Hardcoded limit on iterations - if (switches.output == PROOF) + if ((switches.match < 2) + && (num_intruder_runs > + ((double) switches.runs * max_encryption_level * 8))) { - indentPrint (); - eprintf - ("Pruned: %i intruder runs is too much. (max encr. level %i)\n", - num_intruder_runs, max_encryption_level); + // Hardcoded limit on iterations + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned: %i intruder runs is too much. (max encr. level %i)\n", + num_intruder_runs, max_encryption_level); + } + return 1; } - return 1; } // Limit on exceeding any attack length diff --git a/src/prune_theorems.c b/src/prune_theorems.c index c07c71d..f9d9586 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -242,19 +242,22 @@ 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)) + if (switches.experimental & 4 == 0) { - // Prune the state: we can never meet this - if (switches.output == PROOF) + // 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)) { - indentPrint (); - eprintf ("Pruned because intruder can never construnct "); - termPrint (b->term); - eprintf ("\n"); + // Prune the state: we can never meet this + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned because intruder can never construnct "); + termPrint (b->term); + eprintf ("\n"); + } + return 1; } - return 1; } // Check for encryption levels @@ -281,23 +284,26 @@ 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 (switches.experimental & 4 == 0) { - if (!inKnowledge (sys->know, b->term)) + // 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)) { - // Not in initial knowledge of the intruder - if (switches.output == PROOF) + if (!inKnowledge (sys->know, b->term)) { - indentPrint (); - eprintf ("Pruned because the function "); - termPrint (b->term); - eprintf (" is not known initially to the intruder.\n"); + // Not in initial knowledge of the intruder + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Pruned because the function "); + termPrint (b->term); + eprintf (" is not known initially to the intruder.\n"); + } + return 1; } - return 1; } } diff --git a/src/switches.c b/src/switches.c index 309e2bf..b410161 100644 --- a/src/switches.c +++ b/src/switches.c @@ -942,6 +942,8 @@ switcher (const int process, int index, int commandline) else { switches.experimental = integer_argument (); + eprintf ("Set experimental switch to %i.\n", switches.experimental); + eprintf ("And 4 mask: %i.\n", switches.experimental & 4); return index; } }