[cap-talk] Partial authority

[David Hopwood]

Toby Murray wrote:
> On Mon, 2007-05-07 at 17:35 +0100, David Hopwood wrote: 
>>Pierre THIERRY wrote:
>>>Scribit Toby Murray dies 29/04/2007 hora 14:07:
>>>
>>>>ie. if we remove all of o's events from s (to produce some sequence
>>>>s') and if e can't follow s', then we conclude that o causes this
>>>>occurrence of e and hence, that o has the authority to cause e to
>>>>occur.
>>>
>>>How would you characterize the following: Carol creates a wrapper object
>>>that holds a send capability to Ted, and has two methods, shakeLeftHand
>>>and shakeRightHand. Only if both methods are called is Ted sent a fixed
>>>message. If Carol gives Alice a capability to a facet of the wrapper
>>>with only the shakeLeftHand method and Bob one with only shakeRightHand,
>>>has Alice or Bob authority to send the message to Ted?
>>
>>The definition above says that both alice and bob [*] have (partial) authority
>>to cause the message to be sent to ted. 
> 
> <snip>
> 
>>However, while the definition does what we want (for most analysis purposes)
>>in this case, I'm not sure that it does in all cases. Suppose that in addition,
>>david has a capability to send both shakeLeftHand() and shakeRightHand() to
>>carol, and that in a particular execution,
>>
>>s = <david sends carol <- shakeLeftHand(), david sends carol <- shakeRightHand(),
>>     alice sends carol <- shakeLeftHand(), bob sends carol <- shakeRightHand()>
>>
>>e = "carol sends ted <- run()"
>>
>>s'_a = <david sends carol <- shakeLeftHand(), david sends carol <- shakeRightHand(),
>>        bob sends carol <- shakeRightHand()>
>>s'_b = <david sends carol <- shakeLeftHand(), david sends carol <- shakeRightHand(),
>>        alice sends carol <- shakeLeftHand()>
>>s'_d = <alice sends carol <- shakeLeftHand(), bob sends carol <- shakeRightHand()>
>>
>>Now e *can* follow s'_a, s'_b or s'_d. So we conclude, *incorrectly*, that none of
>>alice, bob or david had authority to cause e.
> 
> If I understand your meaning then I disagree. I think your analysis
> might be contradictory.
> 
> 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.

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. (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.)

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?


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 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.)


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.

-- 
David Hopwood <david.hopwood at industrial-designers.co.uk> (note new address)