[e-lang] A broken brand?

[Toby Murray]

2009/8/20 Toby Murray <toby.murray at comlab.ox.ac.uk>:
> I've made some progress towards a formal statement of the security
> property of this pattern.
>
> In a system in which this pattern is instantiated, producing an
> unsealer 'u' and box 'b' whose contents is 'c':
> 1. an object that cannot acquire a proxy to b nor b itself, and cannot
> acquire c from any object other than u should not be able to acquire
> c.
> 2. an object that cannot acquire a proxy to u nor u itself, and cannot
> acquire c from any object other than u should not be able to acquire
> c.

Actually, more simply, that should be:

"An object that does not possess both u and a proxy to b, or b itself,
cannot have c returned to it by u."

This is nicer because it requires fewer assumptions about the other
objects in the system in order to test (e.g. that they won't pass an
object c etc.).

> We define an object p to be a "proxy to object o", if: p is not an
> unsealer and p can call o in response to an invocation, or p can call
> a proxy to o in response to an invocation.

Boxes are also not proxies by definition.

This new property is equivalent to the old with respect to David's
original attack scenario.

Sorry for the confusion

Toby