diff --git a/src/cost.c b/src/cost.c index e2cf111..7e78a34 100644 --- a/src/cost.c +++ b/src/cost.c @@ -34,6 +34,7 @@ attackCost (const System sys) cost += get_semitrace_length (); cost += 8 * selfInitiators (sys); + cost += 4 * selfResponders (sys); return cost; } diff --git a/src/prune_theorems.c b/src/prune_theorems.c index df60af8..25b6df7 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -208,7 +208,7 @@ prune_theorems (const System sys) * initiators. We still allow it for responder runs, because we assume the * responder is not checking this. */ - if (switches.extravert) + if (switches.initUnique) { if (selfInitiators (sys) > 0) { @@ -220,6 +220,18 @@ prune_theorems (const System sys) } } + if (switches.respUnique) + { + if (selfResponders (sys) > 0) + { + // XXX TODO + // Still need to fix proof output for this + // + // Pruning because some agents are equal for this role. + return true; + } + } + // Prune wrong agents type for initators if (!initiatorAgentsType (sys)) { diff --git a/src/switches.c b/src/switches.c index 6ea6788..f881898 100644 --- a/src/switches.c +++ b/src/switches.c @@ -51,7 +51,8 @@ switchesInit (int argc, char **argv) switches.maxIntruderActions = INT_MAX; // max number of encrypt/decrypt events switches.agentTypecheck = 1; // default do check agent types switches.concrete = true; // default removes symbols, and makes traces concrete - switches.extravert = false; // default allows also initiator Alice to talk to Alice + 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 // Misc @@ -812,7 +813,40 @@ switcher (const int process, int index, int commandline) } else { - switches.extravert = true; + switches.initUnique = true; + switches.respUnique = true; + return index; + } + } + + if (detect (' ', "init-unique", 0)) + { + if (!process) + { + /* discourage: hide + * + * Finds only attacks which exclude initiator Alice talking to Alice + */ + } + else + { + switches.initUnique = true; + return index; + } + } + + if (detect (' ', "resp-unique", 0)) + { + if (!process) + { + /* discourage: hide + * + * Finds only attacks which exclude initiator Alice talking to Alice + */ + } + else + { + switches.respUnique = true; return index; } } diff --git a/src/switches.h b/src/switches.h index 520cb6e..babe7e5 100644 --- a/src/switches.h +++ b/src/switches.h @@ -31,7 +31,8 @@ struct switchdata int maxIntruderActions; //!< Maximum number of intruder actions in the semitrace (encrypt/decrypt) int agentTypecheck; //!< Check type of agent variables in all matching modes int concrete; //!< Swap out variables at the end. - int extravert; //!< Disallow Alice talking to Alice + int initUnique; //!< Default allows duplicate terms in rho (init) + int respUnique; //!< Default allows duplicate terms in rho (resp) int intruder; //!< Enable intruder actions (default) // Misc diff --git a/src/system.c b/src/system.c index 972e839..f72589e 100644 --- a/src/system.c +++ b/src/system.c @@ -1399,6 +1399,82 @@ eventRoledef (const System sys, const int run, const int ev) return roledef_shift (sys->runs[run].start, ev); } +//! determine whether a run talks to itself +int +selfSession (const System sys, const int run) +{ + int self_session; + Termlist agents; + Termlist seen; + + if (sys->runs[run].protocol == INTRUDER) + { + // Intruder has no self sessions + return false; + } + + self_session = false; + + agents = sys->runs[run].rho; + seen = NULL; + while (agents != NULL) + { + Term agent; + + agent = deVar (agents->term); + if (inTermlist (seen, agent)) + { + // This agent was already in the seen list + self_session = true; + } + else + { + seen = termlistAdd (seen, agent); + } + agents = agents->next; + } + termlistDelete (seen); + + return self_session; +} + +//! determine whether a run is a so-called self-responder +/** + * Alice starting a run with Bob, Charlie, Bob is also counted as self-response. + */ +int +selfResponder (const System sys, const int run) +{ + if (sys->runs[run].role->initiator) + { + return false; + } + else + { + return selfSession (sys, run); + } +} + +//! Count the number of any self-responders +int +selfResponders (const System sys) +{ + int count; + int run; + + count = 0; + run = 0; + while (run < sys->maxruns) + { + if (selfInitiator (sys, run)) + { + count++; + } + run++; + } + return count; +} + //! determine whether a run is a so-called self-initiator /** * Alice starting a run with Bob, Charlie, Bob is also counted as self-initiation. @@ -1406,36 +1482,14 @@ eventRoledef (const System sys, const int run, const int ev) int selfInitiator (const System sys, const int run) { - int self_initiator; - - self_initiator = false; if (sys->runs[run].role->initiator) { - // An initiator - Termlist agents; - Termlist seen; - - agents = sys->runs[run].rho; - seen = NULL; - while (agents != NULL) - { - Term agent; - - agent = agents->term; - if (inTermlist (seen, agent)) - { - // This agent was already in the seen list - self_initiator = true; - } - else - { - seen = termlistAdd (seen, agent); - } - agents = agents->next; - } - termlistDelete (seen); + return selfSession (sys, run); + } + else + { + return false; } - return self_initiator; } //! Count the number of any self-initiators diff --git a/src/system.h b/src/system.h index 520087d..968435f 100644 --- a/src/system.h +++ b/src/system.h @@ -201,6 +201,8 @@ int iterateLocalToOther (const System sys, const int myrun, int (*callback) (Term t)); int firstOccurrence (const System sys, const int r, Term t, int evtype); Roledef eventRoledef (const System sys, const int run, const int ev); +int selfResponder (const System sys, const int run); +int selfResponders (const System sys); int selfInitiator (const System sys, const int run); int selfInitiators (const System sys);