diff --git a/gui/Changelog.txt b/gui/Changelog.txt index cbe0c85..a431b8e 100644 --- a/gui/Changelog.txt +++ b/gui/Changelog.txt @@ -6,6 +6,11 @@ Scyther 1.0-beta6 * Added Mac support (added universal binary) * Fixed bug in scripting backend (e.g. with mpa.py) + * Added claim parameter for Reachable claim; Reachable,R means + that role R should be trusted (as well as the actor), but not + any other claim. This can be useful for showing stronger + authentication properties of protocols with more than two + parties. Scyther 1.0-beta5 diff --git a/gui/Scyther/Bin/scyther-linux b/gui/Scyther/Bin/scyther-linux index 2b15c84..65e7e3e 100755 Binary files a/gui/Scyther/Bin/scyther-linux and b/gui/Scyther/Bin/scyther-linux differ diff --git a/src/claim.c b/src/claim.c index de2bcf6..982029a 100644 --- a/src/claim.c +++ b/src/claim.c @@ -707,6 +707,29 @@ arachne_claim_nisynch (const System sys, const int claim_run, return arachne_claim_authentications (sys, claim_run, claim_index, 1); } +//! Are all agents trusted of the claim run (as required by the property?) +int +pruneClaimRunTrusted (const System sys) +{ + if (sys->trustedRoles == NULL) + { + // all agents need to be trusted + if (!isRunTrusted (sys, 0)) + { + return true; + } + } + else + { + // a subset is trusted + if (!isAgentlistTrusted (sys, sys->trustedRoles)) + { + return true; + } + } + return false; +} + //! 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. @@ -716,6 +739,19 @@ arachne_claim_nisynch (const System sys, const int claim_run, int prune_claim_specifics (const System sys) { + // generic status of (all) roles trusted or not + if (pruneClaimRunTrusted (sys)) + { + if (switches.output == PROOF) + { + indentPrint (); + eprintf + ("Pruned because all agents of the claim run must be trusted.\n"); + } + return true; + } + + // specific claims if (sys->current_claim->type == CLAIM_Niagree) { if (arachne_claim_niagree (sys, 0, sys->current_claim->ev)) @@ -757,6 +793,10 @@ add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd, /* * different cases */ + + // per default, all agents are trusted + sys->trustedRoles = NULL; + if (cl->type == CLAIM_Secret) { int newgoals; @@ -791,6 +831,8 @@ add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd, if (cl->type == CLAIM_Reachable) { + int flag; + if (switches.check) { // For reachability claims in check mode, we restrict the number of runs to the number of roles of this protocol @@ -801,7 +843,28 @@ add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd, rolecount = termlistLength (protocol->rolenames); switches.runs = rolecount; } - return callback (); + if (rd->message != NULL) + { + sys->trustedRoles = tuple_to_termlist (rd->message); + +#ifdef DEBUG + if (DEBUGL (2)) + { + eprintf ("Trusted roles : "); + termlistPrint (sys->trustedRoles); + eprintf ("\n"); + } +#endif + } + + flag = callback (); + + if (rd->message != NULL) + { + termlistDelete (sys->trustedRoles); + sys->trustedRoles = NULL; + } + return flag; } return callback (); diff --git a/src/compiler.c b/src/compiler.c index 4baaa73..e0e2ee4 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -998,22 +998,7 @@ runInstanceCreate (Tac tc) roleInstance (sys, p, r, instParams, NULL); // technically, we don't need to do this for Arachne [fix later] /* after creation analysis */ - /* AC1: untrusted agents */ - /* first: determine whether the run is untrusted, - * by checking whether one of the untrusted agents occurs - * in the run instance */ - if (!isAgentlistTrusted (sys, instParams)) - { - /* nothing yet */ - /* claims handle this themselves */ - - /* some reduction might be possible, by cutting of the last few actions - * of such an untrusted run */ - - /* but most of it might be handled dynamically */ - } - - /* AC2: originator assumption for CLP ? */ + /* originator assumption for CLP ? */ /* TODO */ } diff --git a/src/dotout.c b/src/dotout.c index 0ec1ead..6ec5373 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -1673,61 +1673,61 @@ dotSemiState (const System mysys) maxrank = graph_ranks (ranks, nodes); // determine ranks #ifdef DEBUG - if (DEBUGL(1)) - { - // For debugging purposes, we also display an ASCII version of some stuff in the comments - printSemiState (); - // Even draw all dependencies for non-intruder runs - // Real nice debugging :( - int run; + if (DEBUGL (1)) + { + // For debugging purposes, we also display an ASCII version of some stuff in the comments + printSemiState (); + // Even draw all dependencies for non-intruder runs + // Real nice debugging :( + int run; - run = 0; - while (run < sys->maxruns) - { - int ev; + run = 0; + while (run < sys->maxruns) + { + int ev; - ev = 0; - while (ev < sys->runs[run].length) - { - int run2; - int notfirstrun; + ev = 0; + while (ev < sys->runs[run].length) + { + int run2; + int notfirstrun; - eprintf ("// precedence: r%ii%i <- ", run, ev); - run2 = 0; - notfirstrun = 0; - while (run2 < sys->maxruns) - { - int notfirstev; - int ev2; + eprintf ("// precedence: r%ii%i <- ", run, ev); + run2 = 0; + notfirstrun = 0; + while (run2 < sys->maxruns) + { + int notfirstev; + int ev2; - notfirstev = 0; - ev2 = 0; - while (ev2 < sys->runs[run2].length) - { - if (isDependEvent (run2, ev2, run, ev)) - { - if (notfirstev) - eprintf (","); - else - { - if (notfirstrun) - eprintf (" "); - eprintf ("r%i:", run2); - } - eprintf ("%i", ev2); - notfirstrun = 1; - notfirstev = 1; - } - ev2++; - } - run2++; - } - eprintf ("\n"); - ev++; - } - run++; - } - } + notfirstev = 0; + ev2 = 0; + while (ev2 < sys->runs[run2].length) + { + if (isDependEvent (run2, ev2, run, ev)) + { + if (notfirstev) + eprintf (","); + else + { + if (notfirstrun) + eprintf (" "); + eprintf ("r%i:", run2); + } + eprintf ("%i", ev2); + notfirstrun = 1; + notfirstev = 1; + } + ev2++; + } + run2++; + } + eprintf ("\n"); + ev++; + } + run++; + } + } #endif // First, runs diff --git a/src/prune_theorems.c b/src/prune_theorems.c index 9acbbbf..ed5b38c 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -246,18 +246,6 @@ prune_theorems (const System sys) return true; } - // 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 true; - } - // Check if the actors of all other runs are not untrusted if (sys->untrusted != NULL) { diff --git a/src/system.c b/src/system.c index 099981b..12f7681 100644 --- a/src/system.c +++ b/src/system.c @@ -74,9 +74,11 @@ systemInit () sys->knowledgedefined = false; // currently, we have backwards compatibility for empty role knowledge defs (disabling well-formedness rules) sys->attackid = 0; // First attack will have id 1, because the counter is increased before any attacks are displayed. + /* arachne assist */ bindingInit (sys); sys->bindings = NULL; sys->current_claim = NULL; + sys->trustedRoles = NULL; /* reset global counters */ systemReset (sys); diff --git a/src/system.h b/src/system.h index 7ee3ac3..7879fc8 100644 --- a/src/system.h +++ b/src/system.h @@ -150,6 +150,7 @@ struct system /* Arachne assistance */ List bindings; //!< List of bindings Claimlist current_claim; //!< The claim under current investigation + Termlist trustedRoles; //!< Roles that should be trusted for this claim (the default, NULL, means all) }; typedef struct system *System;