BUGFIX: Partial implementation of chosen name attacks could yield false type flaw attacks.
For the typed model, this was not an issue.
This commit is contained in:
parent
b7ab9aefeb
commit
5f7138c300
@ -113,6 +113,32 @@ correctLocalOrder (const System sys)
|
||||
return flag;
|
||||
}
|
||||
|
||||
//! Check all runs
|
||||
/**
|
||||
* Returns false iff an agent type is wrong
|
||||
*/
|
||||
int
|
||||
allAgentsType (const System sys)
|
||||
{
|
||||
int run;
|
||||
|
||||
for (run = 0; run < sys->maxruns; run++)
|
||||
{
|
||||
Termlist agents;
|
||||
|
||||
agents = sys->runs[run].rho;
|
||||
while (agents != NULL)
|
||||
{
|
||||
if (!goodAgentType (agents->term))
|
||||
{
|
||||
return false;
|
||||
}
|
||||
agents = agents->next;
|
||||
}
|
||||
}
|
||||
return true; // seems to be okay
|
||||
}
|
||||
|
||||
//! Check initiator roles
|
||||
/**
|
||||
* Returns false iff an agent type is wrong
|
||||
@ -170,30 +196,6 @@ prune_theorems (const System sys)
|
||||
return true;
|
||||
}
|
||||
|
||||
// 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 true;
|
||||
}
|
||||
}
|
||||
run++;
|
||||
}
|
||||
|
||||
// Prune if any initiator run talks to itself
|
||||
/**
|
||||
* This effectively disallows Alice from talking to Alice, for all
|
||||
@ -224,16 +226,65 @@ prune_theorems (const System sys)
|
||||
}
|
||||
}
|
||||
|
||||
// Prune wrong agents type for initators
|
||||
if (!initiatorAgentsType (sys))
|
||||
/*
|
||||
The semantics imply that create event chose agent names, i.e., the range of rho is a subset of Agent.
|
||||
|
||||
For chosen name attacks we may want to loosen that. However, this requires inserting receive events for the non-actor role variables of responders, and we don't have that yet,
|
||||
so technically this is a bug. Don't use.
|
||||
*/
|
||||
if (switches.chosenName)
|
||||
{
|
||||
if (switches.output == PROOF)
|
||||
// Check if all actors are agents for responders (initiators come next)
|
||||
run = 0;
|
||||
while (run < sys->maxruns)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf
|
||||
("Pruned: an initiator role does not have the correct type for one of its agents.\n");
|
||||
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 true;
|
||||
}
|
||||
}
|
||||
run++;
|
||||
}
|
||||
|
||||
// Prune wrong agents type for initators
|
||||
if (!initiatorAgentsType (sys))
|
||||
{
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf
|
||||
("Pruned: an initiator role does not have the correct type for one of its agents.\n");
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
}
|
||||
else
|
||||
{
|
||||
// Prune wrong agents type for runs
|
||||
if (!allAgentsType (sys))
|
||||
{
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf
|
||||
("Pruned: some run does not have the correct type for one of its agents.\n");
|
||||
}
|
||||
return true;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
// Check if the actors of all other runs are not untrusted
|
||||
|
@ -79,6 +79,7 @@ switchesInit (int argc, char **argv)
|
||||
switches.initUnique = false; // default allows initiator rho to contain duplicate terms
|
||||
switches.respUnique = false; // default allows responder rho to contain duplicate terms
|
||||
switches.intruder = true; // default allows an intruder
|
||||
switches.chosenName = false; // default no chosen name attacks
|
||||
switches.agentUnfold = 0; // default not to unfold agents
|
||||
switches.abstractionMethod = 0; // default no abstraction used
|
||||
switches.useAttackBuffer = false; // don't use by default as it does not work properly under windows vista yet
|
||||
@ -1064,6 +1065,22 @@ switcher (const int process, int index, int commandline)
|
||||
}
|
||||
}
|
||||
|
||||
if (detect (' ', "chosen-name", 0))
|
||||
{
|
||||
if (!process)
|
||||
{
|
||||
/* discourage: hide
|
||||
*
|
||||
* Check for chosen-name attacks. Currently buggy: see prune_theorems.c for more details.
|
||||
*/
|
||||
}
|
||||
else
|
||||
{
|
||||
switches.chosenName = true;
|
||||
return index;
|
||||
}
|
||||
}
|
||||
|
||||
if (detect (' ', "extend-trivial", 0))
|
||||
{
|
||||
if (!process)
|
||||
|
@ -55,6 +55,7 @@ struct switchdata
|
||||
int initUnique; //!< Default allows duplicate terms in rho (init)
|
||||
int respUnique; //!< Default allows duplicate terms in rho (resp)
|
||||
int intruder; //!< Enable intruder actions (default)
|
||||
int chosenName; //!< Check for chosen name attacks
|
||||
int agentUnfold; //!< Explicitly unfold for N honest agents and 1 compromised iff > 0
|
||||
int abstractionMethod; //!< 0 means none, others are specific modes
|
||||
int useAttackBuffer; //!< Use temporary file for attack storage
|
||||
|
Loading…
Reference in New Issue
Block a user