[cap-talk] Partial authority

[Toby Murray]

On Tue, 2007-05-08 at 15:06 +0100, David Hopwood wrote:
> Toby Murray wrote:
> > The above conclusion presumes that that s, s'_a, s'_b and s'_d are valid
> > traces of the system, if I follow you.
> > 
> > If we remove all "david" events from either s'_a or s'_b, then e
> > certainly can't follow. Hence, one cannot conclude from this example
> > that david does not have authority to cause e.
> 
> The definition asks that we remove "david" events from s, not from s'_a
> or s'_b:
> 
>   i.e. if we remove all of [o = david]'s events from s (to produce some
>   sequence [s' = s'_d]), and if e can't follow [s'_d], then we conclude
>   that [david] causes this occurrence of e and hence, that [david]
>   has the authority to cause e to occur.

Have a look at the paper. The part that relates to our current
discussion is the definition of the predicate TC, which is defined as:

TC(A,e) = \exists s . s ^ <e> \in traces(S) \land (s \hide A) ^ <e> \nin
traces(S)

ie. if there exists some trace s where e can follow s and if we remove
all A events from s and e can't follow s, then TC(A,e) holds; that is,
an object with alphabet A *can* cause e to occur.

Therefore, given that you say that e can follow s'_a and s'_b, there
certainly exists some s (say s = s'_a) whereby the above holds.

We only require one such s for the definition to hold. 

> 
> Presumably, this is also intended to imply the converse -- i.e. if
> e can follow s' then o does not have the authority to cause e. 

If no such trace s exists that satisfies the defn of TC, (and the system
is totally deterministic -- see the paper) then we can conclude that the
object with alphabet A cannot cause e to occur.


> (The
> definition doesn't strictly speaking say that, but if it only covers
> *some* of the cases where o has authority to cause e, then it is much
> less useful.)

Why is it less useful if it only covers some cases? The fact that o can
cause e at all is in itself very interesting. If you want to narrow the
cases down to find all of the ways in which o can cause e then this is
possible by considering subsets of traces(S) (where traces(S) is the
total set of traces for the system S). However I'm yet to explore this
too deeply.

> 
> You seem to be saying that we first have to remove all of the events due
> to other subjects that might have been involved in causing e. In general,
> how do we know which subjects those are?

Not necessarily. I'm just saying if there is one such trace s that
satisfies TC, then you can conclude that o *can* cause e to occur.

> 
> 
> Perhaps we can get further by considering groups of subjects rather than
> individual subjects to be the possible agents of causation. (For simplicity,
> let's restrict to groups whose membership does not change during the
> execution, i.e. sets of subjects.)
> 
> First attempt: a subject group G has authority to cause an event e in a
> trace s iff e cannot follow s \ e \ {events(o) : o in G}.

I see where the disconnect might be now. Yes I agree that deciding
whether o has caused e to occur *in a particular trace s* when other
subjects are involved in s is tricky. But this isn't what the defn is
about. TC covers the entire set of traces for a system -- it considers
all s, not just one.

I hope that clears up the misunderstanding. 

I also hope to get your insights on the usefulness of the clarified defn
that ranges over all traces s.


> 
> I think that this is still not the definition we want for most purposes.
> In the second example it would give the following conclusions:
> 
>   {alice, david}      has authority to cause e
>   {bob, david}        has authority to cause e
>   {alice, bob, david} has authority to cause e
>   {alice}             does not have authority to cause e
>   {bob}               does not have authority to cause e
>   {david}             does not have authority to cause e
> 
> but note that if we introduce a dummy object zebedee, which does nothing,
> then we also have:
> 
>   {alice, david, zebedee}      has authority to cause e
>   {bob, david, zebedee}        has authority to cause e
>   {alice, bob, david, zebedee} has authority to cause e
> 
> I don't know how to interpret these results.
> 

> 
> (Note that it is not true in general that adding an subject to the group
> preserves "has authority to cause", i.e. if G' is a superset of G, then
> (G has authority to cause e) does not in general imply
> (G' has authority to cause e), by the above definition. It's easy to
> construct counterexamples involving revokers. However, this is always
> true when G' \ G contains only dummy subjects.)
> 

This is a good argument why considering individual traces is bogus, as
you've so aptly pointed out.

> 
> Here are the conclusions I *think* we want:
> 
>   {alice, bob}                 are sufficient to cause e
>   {david}                      is sufficient to cause e
>   {alice, bob, david}          are sufficient to cause e
>   {alice, bob, zebedee}        are sufficient to cause e
>   {david, zebedee}             are sufficient to cause e
>   {alice, bob, david, zebedee} are sufficient to cause e
>   {alice}                      is not sufficient to cause e
>   {bob}                        is not sufficient to cause e
>   {zebedee}                    is not sufficient to cause e
> 
> The fact that adding a dummy subject to the group preserves "is sufficient
> to cause", is what we would expect.

The problem with "sufficient to cause" is that it presumes that
collusion is not possible. How can we be sure that alice and bob won't
collude to cause e? Hence, I see "sufficient to cause" as less useful
than "can cause (possibly with the assistance of others)", which is what
TC is trying to capture.