- Refactoring code: splitting stuff out of arachne.c
This commit is contained in:
ccremers
parent
4023ef237e
commit
e592a0a432
470
src/arachne.c
470
src/arachne.c
@ -35,27 +35,31 @@
|
|||||||
#include "specialterm.h"
|
#include "specialterm.h"
|
||||||
#include "cost.h"
|
#include "cost.h"
|
||||||
#include "dotout.h"
|
#include "dotout.h"
|
||||||
|
#include "prune_bounds.h"
|
||||||
|
#include "prune_theorems.h"
|
||||||
|
|
||||||
extern int *graph;
|
extern int *graph;
|
||||||
extern int nodes;
|
extern int nodes;
|
||||||
extern int graph_uordblks;
|
extern int graph_uordblks;
|
||||||
|
|
||||||
static System sys;
|
static System sys;
|
||||||
static int attack_length;
|
|
||||||
static int attack_leastcost;
|
int attack_length;
|
||||||
|
int attack_leastcost;
|
||||||
|
|
||||||
Protocol INTRUDER; // Pointers, to be set by the Init
|
Protocol INTRUDER; // Pointers, to be set by the Init
|
||||||
Role I_M; // Same here.
|
Role I_M; // Same here.
|
||||||
Role I_RRS;
|
Role I_RRS;
|
||||||
Role I_RRSD;
|
Role I_RRSD;
|
||||||
|
|
||||||
|
int proofDepth;
|
||||||
|
int max_encryption_level;
|
||||||
|
int num_regular_runs;
|
||||||
|
int num_intruder_runs;
|
||||||
|
|
||||||
static int indentDepth;
|
static int indentDepth;
|
||||||
static int prevIndentDepth;
|
static int prevIndentDepth;
|
||||||
static int indentDepthChanges;
|
static int indentDepthChanges;
|
||||||
static int proofDepth;
|
|
||||||
static int max_encryption_level;
|
|
||||||
static int num_regular_runs;
|
|
||||||
static int num_intruder_runs;
|
|
||||||
static FILE *attack_stream;
|
static FILE *attack_stream;
|
||||||
|
|
||||||
struct goalstruct
|
struct goalstruct
|
||||||
@ -2481,456 +2485,6 @@ bind_goal (const Binding b)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
//! Prune determination because of theorems
|
|
||||||
/**
|
|
||||||
* When something is pruned because of this function, the state space is still
|
|
||||||
* considered to be complete.
|
|
||||||
*
|
|
||||||
*@returns true iff this state is invalid because of a theorem
|
|
||||||
*/
|
|
||||||
int
|
|
||||||
prune_theorems ()
|
|
||||||
{
|
|
||||||
Termlist tl;
|
|
||||||
List bl;
|
|
||||||
int run;
|
|
||||||
|
|
||||||
// Check all types of the local agents according to the matching type
|
|
||||||
if (!checkAllSubstitutions (sys))
|
|
||||||
{
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf
|
|
||||||
("Pruned because some local variable was incorrectly subsituted.\n");
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
// Check if all actors are agents for responders (initiators come next)
|
|
||||||
run = 0;
|
|
||||||
while (run < sys->maxruns)
|
|
||||||
{
|
|
||||||
if (!sys->runs[run].role->initiator)
|
|
||||||
{
|
|
||||||
Term actor;
|
|
||||||
|
|
||||||
actor = agentOfRun (sys, run);
|
|
||||||
if (!goodAgentType (actor))
|
|
||||||
{
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf ("Pruned because the actor ");
|
|
||||||
termPrint (actor);
|
|
||||||
eprintf (" of run %i is not of a compatible type.\n", run);
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
run++;
|
|
||||||
}
|
|
||||||
|
|
||||||
// Prune if any initiator run talks to itself
|
|
||||||
/**
|
|
||||||
* This effectively disallows Alice from talking to Alice, for all
|
|
||||||
* initiators. We still allow it for responder runs, because we assume the
|
|
||||||
* responder is not checking this.
|
|
||||||
*/
|
|
||||||
if (switches.extravert)
|
|
||||||
{
|
|
||||||
int run;
|
|
||||||
|
|
||||||
run = 0;
|
|
||||||
while (run < sys->maxruns)
|
|
||||||
{
|
|
||||||
// Check this run only if it is an initiator role
|
|
||||||
if (sys->runs[run].role->initiator)
|
|
||||||
{
|
|
||||||
// Check this initiator run
|
|
||||||
Termlist tl;
|
|
||||||
|
|
||||||
tl = sys->runs[run].agents;
|
|
||||||
while (tl != NULL)
|
|
||||||
{
|
|
||||||
Termlist tlscan;
|
|
||||||
|
|
||||||
tlscan = tl->next;
|
|
||||||
while (tlscan != NULL)
|
|
||||||
{
|
|
||||||
if (isTermEqual (tl->term, tlscan->term))
|
|
||||||
{
|
|
||||||
// XXX TODO
|
|
||||||
// Still need to fix proof output for this
|
|
||||||
//
|
|
||||||
// Pruning because some agents are equal for this role.
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
tlscan = tlscan->next;
|
|
||||||
}
|
|
||||||
tl = tl->next;
|
|
||||||
}
|
|
||||||
run++;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
// Prune wrong agents type for initators
|
|
||||||
if (!initiatorAgentsType ())
|
|
||||||
{
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf
|
|
||||||
("Pruned: an initiator role does not have the correct type for one of its agents.\n");
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
// Check if all agents of the main run are valid
|
|
||||||
if (!isRunTrusted (sys, 0))
|
|
||||||
{
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf
|
|
||||||
("Pruned because all agents of the claim run must be trusted.\n");
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
// Check if the actors of all other runs are not untrusted
|
|
||||||
if (sys->untrusted != NULL)
|
|
||||||
{
|
|
||||||
int run;
|
|
||||||
|
|
||||||
run = 1;
|
|
||||||
while (run < sys->maxruns)
|
|
||||||
{
|
|
||||||
if (sys->runs[run].protocol != INTRUDER)
|
|
||||||
{
|
|
||||||
if (sys->runs[run].agents != NULL)
|
|
||||||
{
|
|
||||||
Term actor;
|
|
||||||
|
|
||||||
actor = agentOfRun (sys, run);
|
|
||||||
if (actor == NULL)
|
|
||||||
{
|
|
||||||
error ("Agent of run %i is NULL", run);
|
|
||||||
}
|
|
||||||
if (!isAgentTrusted (sys, actor))
|
|
||||||
{
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf
|
|
||||||
("Pruned because the actor of run %i is untrusted.\n",
|
|
||||||
run);
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
Protocol p;
|
|
||||||
|
|
||||||
globalError++;
|
|
||||||
eprintf ("Run %i: ", run);
|
|
||||||
role_name_print (run);
|
|
||||||
eprintf (" has an empty agents list.\n");
|
|
||||||
eprintf ("protocol->rolenames: ");
|
|
||||||
p = (Protocol) sys->runs[run].protocol;
|
|
||||||
termlistPrint (p->rolenames);
|
|
||||||
eprintf ("\n");
|
|
||||||
error ("Aborting.");
|
|
||||||
globalError--;
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
run++;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
// Check for c-minimality
|
|
||||||
{
|
|
||||||
if (!bindings_c_minimal ())
|
|
||||||
{
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf ("Pruned because this is not <=c-minimal.\n");
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
|
||||||
* Check whether the bindings are valid
|
|
||||||
*/
|
|
||||||
bl = sys->bindings;
|
|
||||||
while (bl != NULL)
|
|
||||||
{
|
|
||||||
Binding b;
|
|
||||||
|
|
||||||
b = bl->data;
|
|
||||||
|
|
||||||
// Check for "Hidden" interm goals
|
|
||||||
if (termInTerm (b->term, TERM_Hidden))
|
|
||||||
{
|
|
||||||
// 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;
|
|
||||||
}
|
|
||||||
|
|
||||||
// Check for encryption levels
|
|
||||||
/*
|
|
||||||
* if (switches.match < 2
|
|
||||||
*/
|
|
||||||
if (term_encryption_level (b->term) > max_encryption_level)
|
|
||||||
{
|
|
||||||
// Prune: we do not need to construct such terms
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf ("Pruned because the encryption level of ");
|
|
||||||
termPrint (b->term);
|
|
||||||
eprintf (" is too high.\n");
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
// 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.
|
|
||||||
if (isTermFunctionName (b->term))
|
|
||||||
{
|
|
||||||
if (!inKnowledge (sys->know, b->term))
|
|
||||||
{
|
|
||||||
// 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;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
bl = bl->next;
|
|
||||||
}
|
|
||||||
|
|
||||||
/* check for singular roles */
|
|
||||||
run = 0;
|
|
||||||
while (run < sys->maxruns)
|
|
||||||
{
|
|
||||||
if (sys->runs[run].role->singular)
|
|
||||||
{
|
|
||||||
// This is a singular role: it therefore should not occur later on again.
|
|
||||||
int run2;
|
|
||||||
Term rolename;
|
|
||||||
|
|
||||||
rolename = sys->runs[run].role->nameterm;
|
|
||||||
run2 = run + 1;
|
|
||||||
while (run2 < sys->maxruns)
|
|
||||||
{
|
|
||||||
Term rolename2;
|
|
||||||
|
|
||||||
rolename2 = sys->runs[run2].role->nameterm;
|
|
||||||
if (isTermEqual (rolename, rolename2))
|
|
||||||
{
|
|
||||||
// This is not allowed: the singular role occurs twice in the semitrace.
|
|
||||||
// Thus we prune.
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf ("Pruned because the singular role ");
|
|
||||||
termPrint (rolename);
|
|
||||||
eprintf (" occurs more than once in the semitrace.\n");
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
run2++;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
run++;
|
|
||||||
}
|
|
||||||
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
//! Prune determination for bounds
|
|
||||||
/**
|
|
||||||
* When something is pruned here, the state space is not complete anymore.
|
|
||||||
*
|
|
||||||
*@returns true iff this state is invalid for some reason
|
|
||||||
*/
|
|
||||||
int
|
|
||||||
prune_bounds ()
|
|
||||||
{
|
|
||||||
Termlist tl;
|
|
||||||
List bl;
|
|
||||||
|
|
||||||
/* prune for time */
|
|
||||||
if (passed_time_limit ())
|
|
||||||
{
|
|
||||||
// Oh no, we ran out of time!
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf ("Pruned: ran out of allowed time (-T %i switch)\n",
|
|
||||||
get_time_limit ());
|
|
||||||
}
|
|
||||||
// Pruned because of time bound!
|
|
||||||
sys->current_claim->timebound = 1;
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
/* prune for proof depth */
|
|
||||||
if (proofDepth > switches.maxproofdepth)
|
|
||||||
{
|
|
||||||
// Hardcoded limit on proof tree depth
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf ("Pruned: proof tree too deep: %i (-d %i switch)\n",
|
|
||||||
proofDepth, switches.maxproofdepth);
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
/* prune for trace length */
|
|
||||||
if (switches.maxtracelength < INT_MAX)
|
|
||||||
{
|
|
||||||
int tracelength;
|
|
||||||
int run;
|
|
||||||
|
|
||||||
/* compute trace length of current semistate */
|
|
||||||
tracelength = 0;
|
|
||||||
run = 0;
|
|
||||||
while (run < sys->maxruns)
|
|
||||||
{
|
|
||||||
/* ignore intruder actions */
|
|
||||||
if (sys->runs[run].protocol != INTRUDER)
|
|
||||||
{
|
|
||||||
tracelength = tracelength + sys->runs[run].step;
|
|
||||||
}
|
|
||||||
run++;
|
|
||||||
}
|
|
||||||
/* test */
|
|
||||||
if (tracelength > switches.maxtracelength)
|
|
||||||
{
|
|
||||||
// Hardcoded limit on proof tree depth
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf ("Pruned: trace too long: %i (-l %i switch)\n",
|
|
||||||
tracelength, switches.maxtracelength);
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
if (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);
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
// This needs some foundation. Probably * 2^max_encryption_level
|
|
||||||
//!@todo Fix this bound
|
|
||||||
if ((switches.match < 2)
|
|
||||||
&& (num_intruder_runs >
|
|
||||||
((double) switches.runs * max_encryption_level * 8)))
|
|
||||||
{
|
|
||||||
// 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;
|
|
||||||
}
|
|
||||||
|
|
||||||
// Limit on exceeding any attack length
|
|
||||||
if (get_semitrace_length () >= attack_length)
|
|
||||||
{
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf ("Pruned: attack length %i.\n", attack_length);
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
/* prune for cheaper */
|
|
||||||
if (switches.prune == 2 && attack_leastcost <= attackCost (sys))
|
|
||||||
{
|
|
||||||
// We already had an attack at least this cheap.
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf
|
|
||||||
("Pruned: attack cost exceeds a previously found attack.\n");
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
// Limit on attack count
|
|
||||||
if (enoughAttacks (sys))
|
|
||||||
return 1;
|
|
||||||
|
|
||||||
// Pruning involving the number of intruder actions
|
|
||||||
{
|
|
||||||
// Count intruder actions
|
|
||||||
int actioncount;
|
|
||||||
|
|
||||||
actioncount = countIntruderActions ();
|
|
||||||
|
|
||||||
// Limit intruder actions in any case
|
|
||||||
if (!(switches.intruder) && actioncount > 0)
|
|
||||||
{
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf
|
|
||||||
("Pruned: no intruder allowed.\n", switches.maxIntruderActions);
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
// Limit on intruder events count
|
|
||||||
if (actioncount > switches.maxIntruderActions)
|
|
||||||
{
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf
|
|
||||||
("Pruned: more than %i encrypt/decrypt events in the semitrace.\n",
|
|
||||||
switches.maxIntruderActions);
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
// No pruning because of bounds
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
//! Prune determination for specific properties
|
//! 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.
|
* 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.
|
||||||
@ -3337,11 +2891,11 @@ iterate ()
|
|||||||
|
|
||||||
|
|
||||||
flag = 1;
|
flag = 1;
|
||||||
if (!prune_theorems ())
|
if (!prune_theorems (sys))
|
||||||
{
|
{
|
||||||
if (!prune_claim_specifics ())
|
if (!prune_claim_specifics ())
|
||||||
{
|
{
|
||||||
if (!prune_bounds ())
|
if (!prune_bounds (sys))
|
||||||
{
|
{
|
||||||
Binding b;
|
Binding b;
|
||||||
|
|
||||||
|
|||||||
186
src/prune_bounds.c
Normal file
186
src/prune_bounds.c
Normal file
@ -0,0 +1,186 @@
|
|||||||
|
/**
|
||||||
|
*
|
||||||
|
*@file prune_bounds.c
|
||||||
|
*
|
||||||
|
* Prune stuff based on bounds
|
||||||
|
*
|
||||||
|
*/
|
||||||
|
|
||||||
|
#include <limits.h>
|
||||||
|
|
||||||
|
#include "termlist.h"
|
||||||
|
#include "list.h"
|
||||||
|
#include "switches.h"
|
||||||
|
|
||||||
|
extern int attack_length;
|
||||||
|
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
|
||||||
|
/**
|
||||||
|
* When something is pruned here, the state space is not complete anymore.
|
||||||
|
*
|
||||||
|
*@returns true iff this state is invalid for some reason
|
||||||
|
*/
|
||||||
|
int
|
||||||
|
prune_bounds (const System sys)
|
||||||
|
{
|
||||||
|
Termlist tl;
|
||||||
|
List bl;
|
||||||
|
|
||||||
|
/* prune for time */
|
||||||
|
if (passed_time_limit ())
|
||||||
|
{
|
||||||
|
// Oh no, we ran out of time!
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf ("Pruned: ran out of allowed time (-T %i switch)\n",
|
||||||
|
get_time_limit ());
|
||||||
|
}
|
||||||
|
// Pruned because of time bound!
|
||||||
|
sys->current_claim->timebound = 1;
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
/* prune for proof depth */
|
||||||
|
if (proofDepth > switches.maxproofdepth)
|
||||||
|
{
|
||||||
|
// Hardcoded limit on proof tree depth
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf ("Pruned: proof tree too deep: %i (-d %i switch)\n",
|
||||||
|
proofDepth, switches.maxproofdepth);
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
/* prune for trace length */
|
||||||
|
if (switches.maxtracelength < INT_MAX)
|
||||||
|
{
|
||||||
|
int tracelength;
|
||||||
|
int run;
|
||||||
|
|
||||||
|
/* compute trace length of current semistate */
|
||||||
|
tracelength = 0;
|
||||||
|
run = 0;
|
||||||
|
while (run < sys->maxruns)
|
||||||
|
{
|
||||||
|
/* ignore intruder actions */
|
||||||
|
if (sys->runs[run].protocol != INTRUDER)
|
||||||
|
{
|
||||||
|
tracelength = tracelength + sys->runs[run].step;
|
||||||
|
}
|
||||||
|
run++;
|
||||||
|
}
|
||||||
|
/* test */
|
||||||
|
if (tracelength > switches.maxtracelength)
|
||||||
|
{
|
||||||
|
// Hardcoded limit on proof tree depth
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf ("Pruned: trace too long: %i (-l %i switch)\n",
|
||||||
|
tracelength, switches.maxtracelength);
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
if (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);
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
// This needs some foundation. Probably * 2^max_encryption_level
|
||||||
|
//!@todo Fix this bound
|
||||||
|
if ((switches.match < 2)
|
||||||
|
&& (num_intruder_runs >
|
||||||
|
((double) switches.runs * max_encryption_level * 8)))
|
||||||
|
{
|
||||||
|
// 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;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Limit on exceeding any attack length
|
||||||
|
if (get_semitrace_length () >= attack_length)
|
||||||
|
{
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf ("Pruned: attack length %i.\n", attack_length);
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
/* prune for cheaper */
|
||||||
|
if (switches.prune == 2 && attack_leastcost <= attackCost (sys))
|
||||||
|
{
|
||||||
|
// We already had an attack at least this cheap.
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf
|
||||||
|
("Pruned: attack cost exceeds a previously found attack.\n");
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Limit on attack count
|
||||||
|
if (enoughAttacks (sys))
|
||||||
|
return 1;
|
||||||
|
|
||||||
|
// Pruning involving the number of intruder actions
|
||||||
|
{
|
||||||
|
// Count intruder actions
|
||||||
|
int actioncount;
|
||||||
|
|
||||||
|
actioncount = countIntruderActions ();
|
||||||
|
|
||||||
|
// Limit intruder actions in any case
|
||||||
|
if (!(switches.intruder) && actioncount > 0)
|
||||||
|
{
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf
|
||||||
|
("Pruned: no intruder allowed.\n", switches.maxIntruderActions);
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Limit on intruder events count
|
||||||
|
if (actioncount > switches.maxIntruderActions)
|
||||||
|
{
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf
|
||||||
|
("Pruned: more than %i encrypt/decrypt events in the semitrace.\n",
|
||||||
|
switches.maxIntruderActions);
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// No pruning because of bounds
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
6
src/prune_bounds.h
Normal file
6
src/prune_bounds.h
Normal file
@ -0,0 +1,6 @@
|
|||||||
|
#ifndef PRUNEBOUNDS
|
||||||
|
#define PRUNEBOUNDS
|
||||||
|
|
||||||
|
int prune_bounds (const System sys);
|
||||||
|
|
||||||
|
#endif
|
||||||
303
src/prune_theorems.c
Normal file
303
src/prune_theorems.c
Normal file
@ -0,0 +1,303 @@
|
|||||||
|
/**
|
||||||
|
*
|
||||||
|
*@file prune_theorems.c
|
||||||
|
*
|
||||||
|
* Prune stuff based on theorems.
|
||||||
|
* Pruning leaves complete results.
|
||||||
|
*
|
||||||
|
*/
|
||||||
|
|
||||||
|
#include "system.h"
|
||||||
|
#include "list.h"
|
||||||
|
#include "switches.h"
|
||||||
|
#include "binding.h"
|
||||||
|
#include "specialterm.h"
|
||||||
|
|
||||||
|
extern Protocol INTRUDER;
|
||||||
|
extern int proofDepth;
|
||||||
|
extern int max_encryption_level;
|
||||||
|
|
||||||
|
//! Prune determination because of theorems
|
||||||
|
/**
|
||||||
|
* When something is pruned because of this function, the state space is still
|
||||||
|
* considered to be complete.
|
||||||
|
*
|
||||||
|
*@returns true iff this state is invalid because of a theorem
|
||||||
|
*/
|
||||||
|
int
|
||||||
|
prune_theorems (const System sys)
|
||||||
|
{
|
||||||
|
Termlist tl;
|
||||||
|
List bl;
|
||||||
|
int run;
|
||||||
|
|
||||||
|
// Check all types of the local agents according to the matching type
|
||||||
|
if (!checkAllSubstitutions (sys))
|
||||||
|
{
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf
|
||||||
|
("Pruned because some local variable was incorrectly subsituted.\n");
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Check if all actors are agents for responders (initiators come next)
|
||||||
|
run = 0;
|
||||||
|
while (run < sys->maxruns)
|
||||||
|
{
|
||||||
|
if (!sys->runs[run].role->initiator)
|
||||||
|
{
|
||||||
|
Term actor;
|
||||||
|
|
||||||
|
actor = agentOfRun (sys, run);
|
||||||
|
if (!goodAgentType (actor))
|
||||||
|
{
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf ("Pruned because the actor ");
|
||||||
|
termPrint (actor);
|
||||||
|
eprintf (" of run %i is not of a compatible type.\n", run);
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
run++;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Prune if any initiator run talks to itself
|
||||||
|
/**
|
||||||
|
* This effectively disallows Alice from talking to Alice, for all
|
||||||
|
* initiators. We still allow it for responder runs, because we assume the
|
||||||
|
* responder is not checking this.
|
||||||
|
*/
|
||||||
|
if (switches.extravert)
|
||||||
|
{
|
||||||
|
int run;
|
||||||
|
|
||||||
|
run = 0;
|
||||||
|
while (run < sys->maxruns)
|
||||||
|
{
|
||||||
|
// Check this run only if it is an initiator role
|
||||||
|
if (sys->runs[run].role->initiator)
|
||||||
|
{
|
||||||
|
// Check this initiator run
|
||||||
|
Termlist tl;
|
||||||
|
|
||||||
|
tl = sys->runs[run].agents;
|
||||||
|
while (tl != NULL)
|
||||||
|
{
|
||||||
|
Termlist tlscan;
|
||||||
|
|
||||||
|
tlscan = tl->next;
|
||||||
|
while (tlscan != NULL)
|
||||||
|
{
|
||||||
|
if (isTermEqual (tl->term, tlscan->term))
|
||||||
|
{
|
||||||
|
// XXX TODO
|
||||||
|
// Still need to fix proof output for this
|
||||||
|
//
|
||||||
|
// Pruning because some agents are equal for this role.
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
tlscan = tlscan->next;
|
||||||
|
}
|
||||||
|
tl = tl->next;
|
||||||
|
}
|
||||||
|
run++;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// Prune wrong agents type for initators
|
||||||
|
if (!initiatorAgentsType ())
|
||||||
|
{
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf
|
||||||
|
("Pruned: an initiator role does not have the correct type for one of its agents.\n");
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Check if all agents of the main run are valid
|
||||||
|
if (!isRunTrusted (sys, 0))
|
||||||
|
{
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf
|
||||||
|
("Pruned because all agents of the claim run must be trusted.\n");
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Check if the actors of all other runs are not untrusted
|
||||||
|
if (sys->untrusted != NULL)
|
||||||
|
{
|
||||||
|
int run;
|
||||||
|
|
||||||
|
run = 1;
|
||||||
|
while (run < sys->maxruns)
|
||||||
|
{
|
||||||
|
if (sys->runs[run].protocol != INTRUDER)
|
||||||
|
{
|
||||||
|
if (sys->runs[run].agents != NULL)
|
||||||
|
{
|
||||||
|
Term actor;
|
||||||
|
|
||||||
|
actor = agentOfRun (sys, run);
|
||||||
|
if (actor == NULL)
|
||||||
|
{
|
||||||
|
error ("Agent of run %i is NULL", run);
|
||||||
|
}
|
||||||
|
if (!isAgentTrusted (sys, actor))
|
||||||
|
{
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf
|
||||||
|
("Pruned because the actor of run %i is untrusted.\n",
|
||||||
|
run);
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
Protocol p;
|
||||||
|
|
||||||
|
globalError++;
|
||||||
|
eprintf ("Run %i: ", run);
|
||||||
|
role_name_print (run);
|
||||||
|
eprintf (" has an empty agents list.\n");
|
||||||
|
eprintf ("protocol->rolenames: ");
|
||||||
|
p = (Protocol) sys->runs[run].protocol;
|
||||||
|
termlistPrint (p->rolenames);
|
||||||
|
eprintf ("\n");
|
||||||
|
error ("Aborting.");
|
||||||
|
globalError--;
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
run++;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// Check for c-minimality
|
||||||
|
{
|
||||||
|
if (!bindings_c_minimal ())
|
||||||
|
{
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf ("Pruned because this is not <=c-minimal.\n");
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Check whether the bindings are valid
|
||||||
|
*/
|
||||||
|
bl = sys->bindings;
|
||||||
|
while (bl != NULL)
|
||||||
|
{
|
||||||
|
Binding b;
|
||||||
|
|
||||||
|
b = bl->data;
|
||||||
|
|
||||||
|
// Check for "Hidden" interm goals
|
||||||
|
if (termInTerm (b->term, TERM_Hidden))
|
||||||
|
{
|
||||||
|
// 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;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Check for encryption levels
|
||||||
|
/*
|
||||||
|
* if (switches.match < 2
|
||||||
|
*/
|
||||||
|
if (term_encryption_level (b->term) > max_encryption_level)
|
||||||
|
{
|
||||||
|
// Prune: we do not need to construct such terms
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf ("Pruned because the encryption level of ");
|
||||||
|
termPrint (b->term);
|
||||||
|
eprintf (" is too high.\n");
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
// 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.
|
||||||
|
if (isTermFunctionName (b->term))
|
||||||
|
{
|
||||||
|
if (!inKnowledge (sys->know, b->term))
|
||||||
|
{
|
||||||
|
// 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;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
bl = bl->next;
|
||||||
|
}
|
||||||
|
|
||||||
|
/* check for singular roles */
|
||||||
|
run = 0;
|
||||||
|
while (run < sys->maxruns)
|
||||||
|
{
|
||||||
|
if (sys->runs[run].role->singular)
|
||||||
|
{
|
||||||
|
// This is a singular role: it therefore should not occur later on again.
|
||||||
|
int run2;
|
||||||
|
Term rolename;
|
||||||
|
|
||||||
|
rolename = sys->runs[run].role->nameterm;
|
||||||
|
run2 = run + 1;
|
||||||
|
while (run2 < sys->maxruns)
|
||||||
|
{
|
||||||
|
Term rolename2;
|
||||||
|
|
||||||
|
rolename2 = sys->runs[run2].role->nameterm;
|
||||||
|
if (isTermEqual (rolename, rolename2))
|
||||||
|
{
|
||||||
|
// This is not allowed: the singular role occurs twice in the semitrace.
|
||||||
|
// Thus we prune.
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf ("Pruned because the singular role ");
|
||||||
|
termPrint (rolename);
|
||||||
|
eprintf (" occurs more than once in the semitrace.\n");
|
||||||
|
}
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
run2++;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
run++;
|
||||||
|
}
|
||||||
|
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
6
src/prune_theorems.h
Normal file
6
src/prune_theorems.h
Normal file
@ -0,0 +1,6 @@
|
|||||||
|
#ifndef PRUNETHEOREMS
|
||||||
|
#define PRUNETHEOREMS
|
||||||
|
|
||||||
|
int prune_theorems (const System sys);
|
||||||
|
|
||||||
|
#endif
|
||||||
Loading…
Reference in New Issue
Block a user