[cap-talk] Delegation/Proxy equivalence and limited lifespan objects?

[Toby Murray]

On Mon, 2007-11-12 at 14:28 +0100, Rob Meijer wrote:
> Has any work been done on patterns like this? and does anyone know if there
> are any conclusive results with respect to equivalence possibilities with
> limited lefespan objects between delegation and proxying?

Firstly, some work has been done but nothing formal as yet. The
Communicating Conspirators page at erights.org has an informal analysis
of delegation vs. proxying
http://www.erights.org/elib/capability/conspire.html

Now in terms of "proving" an "equivalence" between delegation and
proxying, little work has been done. I'll wager, however, that were one
able to "prove" such a thing, that the model in which the proof was
constructed would have to be adequately crippled in order to make it
less than useful for reasoning about authority. This is because no such
equivalence holds, in my opinion, when using fine-grained notions of
authority.

Some corner cases highlight why the equivalence doesn't exist in
general.

Rights amplification is a good example. Suppose Bob has a capability c
to Carol. Suppose Alice has a capability d to Dennis such that when
combined with c results in rights amplification. (Let's say that Dennis
is an unsealer for Carol or something like that.)

Suppose that Bob is willing to proxy the c capability for Alice but not
willing to delegate it to her. Alice is likewise unwilling to delegate
to Bob but willing to proxy. Alice will never be able to achieve rights
amplification. Nor will Bob.

Hence, there is a clear distinction between proxying and delegating in
the presence of rights amplification.

Suppose Bob is proxying his c capability for Alice. Bob can revoke
Alice's access at any time. Bob can also interfere with Alice's access
to Carol (via c) at any time. Hence, one can reason (informally) that
Bob has /more/ authority over Carol than Alice does.

Were Bob instead to delegate c to Alice, then Bob and Alice would share
identical authority over Carol.

Hence, again, we see an (informal) distinction between the two.

One might reason about it this way:

When Bob is proxying his access to Carol for Alice, Alice's authority to
access Carol is /dependent/ on Bob's behaviour. Once Bob delegates to
Alice, however, Alice's access is no longer dependent on Bob's
behaviour.

Getting some formal notion of this "dependence" would, I believe, allow
one to disprove the equivalence claim. (It probably has to do with the
idea that Alice's authority over Carol is not identical for all
variations of Bob's behaviour.) 

On the other hand, were one reasoning in a model that naturally
distinguishes causation from permission, then that would also make the
distinction plain. In the first case when Bob is proxying for Alice,
Alice can /cause/ Carol to be invoked via Bob, but in the second case
where Bob delegates to Alice, she is given direct /permission/ to invoke
Carol. 

It so happens that the model of authority I'm working with in CSP
naturally has this distinction built-in; but that's incidental to our
discussion.