diff --git a/src/arachne.c b/src/arachne.c index d726552..7399ce2 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -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) { diff --git a/src/compiler.c b/src/compiler.c index deffb1c..7643859 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -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 */ diff --git a/src/modelchecker.c b/src/modelchecker.c index 158b71e..612f61c 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -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. */ diff --git a/src/output.c b/src/output.c index 45003b4..df41006 100644 --- a/src/output.c +++ b/src/output.c @@ -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); } diff --git a/src/system.c b/src/system.c index d7e87d9..0bda593 100644 --- a/src/system.c +++ b/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; } + diff --git a/src/system.h b/src/system.h index 1908d0d..f81d04e 100644 --- a/src/system.h +++ b/src/system.h @@ -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 diff --git a/src/xmlout.c b/src/xmlout.c index dbd86ff..9f75e21 100644 --- a/src/xmlout.c +++ b/src/xmlout.c @@ -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 ("\n");