- New attack attribute.
This commit is contained in:
parent
86b1a8295c
commit
164e325659
@ -2724,23 +2724,15 @@ prune_theorems ()
|
||||
}
|
||||
|
||||
// Check if all agents of the main run are valid
|
||||
tl = sys->runs[0].agents;
|
||||
while (tl != NULL)
|
||||
if (!isRunTrusted (sys,0))
|
||||
{
|
||||
Term agent;
|
||||
|
||||
agent = deVar (tl->term);
|
||||
if (!realTermVariable (agent) && inTermlist (sys->untrusted, agent))
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf
|
||||
("Pruned because all agents of the claim run must be trusted.\n");
|
||||
}
|
||||
return 1;
|
||||
indentPrint ();
|
||||
eprintf
|
||||
("Pruned because all agents of the claim run must be trusted.\n");
|
||||
}
|
||||
tl = tl->next;
|
||||
return 1;
|
||||
}
|
||||
|
||||
// Check if the actors of all other runs are not untrusted
|
||||
@ -2762,7 +2754,7 @@ prune_theorems ()
|
||||
{
|
||||
error ("Agent of run %i is NULL", run);
|
||||
}
|
||||
if (inTermlist (sys->untrusted, actor))
|
||||
if (!isAgentTrusted (sys, actor))
|
||||
{
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
|
@ -719,7 +719,7 @@ runInstanceCreate (Tac tc)
|
||||
/* first: determine whether the run is untrusted,
|
||||
* by checking whether one of the untrusted agents occurs
|
||||
* in the run instance */
|
||||
if (untrustedAgent (sys, instParams))
|
||||
if (!isAgentlistTrusted (sys, instParams))
|
||||
{
|
||||
/* nothing yet */
|
||||
/* claims handle this themselves */
|
||||
|
@ -260,7 +260,7 @@ removeDangling (Roledef rd, const int killclaims)
|
||||
Roledef
|
||||
removeIrrelevant (const System sys, const int run, Roledef rd)
|
||||
{
|
||||
if (untrustedAgent (sys, sys->runs[run].agents))
|
||||
if (!isRunTrusted (sys,run))
|
||||
{
|
||||
// untrusted, so also remove claims
|
||||
return removeDangling (rd, 1);
|
||||
@ -384,7 +384,7 @@ explorify (const System sys, const int run)
|
||||
while (rid < sys->maxruns)
|
||||
{
|
||||
/* are claims in this run evaluated anyway? */
|
||||
if (!untrustedAgent (sys, sys->runs[rid].agents))
|
||||
if (isRunTrusted(sys, rid))
|
||||
{ /* possibly claims to be checked in this run */
|
||||
rdscan = runPointerGet (sys, rid);
|
||||
while (rdscan != NULL)
|
||||
@ -465,7 +465,7 @@ explorify (const System sys, const int run)
|
||||
rid = 0;
|
||||
while (rid < sys->maxruns)
|
||||
{
|
||||
if (!untrustedAgent (sys, sys->runs[rid].agents))
|
||||
if (!isRunTrusted (sys, rid))
|
||||
{
|
||||
}
|
||||
rid++;
|
||||
@ -1207,7 +1207,7 @@ claimViolationDetails (const System sys, const int run, const Roledef rd,
|
||||
{
|
||||
/* secrecy claim */
|
||||
|
||||
if (untrustedAgent (sys, sys->runs[run].agents))
|
||||
if (!isRunTrusted (sys,run))
|
||||
{
|
||||
/* claim was skipped */
|
||||
return (Termlist) - 1;
|
||||
@ -1328,7 +1328,7 @@ executeTry (const System sys, int run)
|
||||
if (runPoint->type == CLAIM)
|
||||
{
|
||||
/* first we might dynamically determine whether the claim is valid */
|
||||
if (untrustedAgent (sys, sys->runs[run].agents))
|
||||
if (!isRunTrusted (sys,run))
|
||||
{
|
||||
/* for untrusted agents we check no claim violations at all
|
||||
* so: we know it's okay. */
|
||||
|
@ -609,7 +609,7 @@ graphNode (const System sys)
|
||||
// Print step
|
||||
printf ("%i:", sys->runs[run].step - 1);
|
||||
|
||||
if (rd->type == CLAIM && untrustedAgent (sys, sys->runs[run].agents))
|
||||
if (rd->type == CLAIM && (!isRunTrusted(sys,run)))
|
||||
{
|
||||
printf ("Skip claim in #%i\"", run);
|
||||
}
|
||||
|
61
src/system.c
61
src/system.c
@ -1212,39 +1212,55 @@ protocolsPrint (Protocol p)
|
||||
}
|
||||
}
|
||||
|
||||
//! Determine whether an agent term is trusted
|
||||
/**
|
||||
* 1 (True) means trusted, 0 is untrusted
|
||||
*/
|
||||
int
|
||||
isAgentTrusted (const System sys, Term agent)
|
||||
{
|
||||
agent = deVar (agent);
|
||||
if (!realTermVariable (agent) && inTermlist (sys->untrusted, agent))
|
||||
{
|
||||
// Untrusted agent in the list
|
||||
return 0;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
//! Determine whether there is an untrusted agent.
|
||||
/**
|
||||
*@param sys The system, containing system::untrusted.
|
||||
*@param agents A list of agents to be verified.
|
||||
*@return True iff any agent in the list is untrusted.
|
||||
*@return True iff all agent in the list are trusted.
|
||||
*/
|
||||
int
|
||||
untrustedAgent (const System sys, Termlist agents)
|
||||
isAgentlistTrusted (const System sys, Termlist agents)
|
||||
{
|
||||
while (agents != NULL)
|
||||
{
|
||||
if (isTermVariable (agents->term))
|
||||
if (!isAgentTrusted (sys, agents->term))
|
||||
{
|
||||
if (switches.clp)
|
||||
{
|
||||
/* clp: variables are difficult */
|
||||
/* TODO Add as constraint that they're
|
||||
* trusted */
|
||||
/* However, that is a branch as well :(
|
||||
*/
|
||||
/* claim secret is _really_ a instant-multiple
|
||||
* read. If it is succesful, we sound
|
||||
* the alert */
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
if (inTermlist (sys->untrusted, agents->term))
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
agents = agents->next;
|
||||
}
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
|
||||
//! Determine whether all agents of a run are trusted
|
||||
/**
|
||||
* Returns 0 (False) if they are not trusted, otherwise 1 (True)
|
||||
*/
|
||||
int
|
||||
isRunTrusted (const System sys, const int run)
|
||||
{
|
||||
if (run >= 0 && run < sys->maxruns)
|
||||
{
|
||||
if (!isAgentlistTrusted (sys, sys->runs[run].agents))
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
//! Yield the maximum length of a trace by analysing the runs in the system.
|
||||
@ -1446,3 +1462,4 @@ system_iterate_roles (const System sys, int (*func) ())
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
@ -203,5 +203,8 @@ int compute_roleeventmax (const System sys);
|
||||
|
||||
void scenarioPrint (const System sys);
|
||||
int system_iterate_roles (const System sys, int (*func) ());
|
||||
int isAgentTrusted (const System sys, Term agent);
|
||||
int isAgentlistTrusted (const System sys, Termlist agents);
|
||||
int isRunTrusted (const System sys, const int run);
|
||||
|
||||
#endif
|
||||
|
@ -672,6 +672,14 @@ xmlRunInfo (const System sys, const int run)
|
||||
{
|
||||
printf (" intruder=\"true\"");
|
||||
}
|
||||
else
|
||||
{
|
||||
// Non-intruder run, check whether communicates with untrusted agents
|
||||
if (!isRunTrusted (sys, run))
|
||||
{
|
||||
printf(" untrustedrun=\"true\"");
|
||||
}
|
||||
}
|
||||
printf (">");
|
||||
xmlTermPrint (sys->runs[run].protocol->nameterm);
|
||||
printf ("</protocol>\n");
|
||||
|
Loading…
Reference in New Issue
Block a user