[cap-talk] Is "Authority" Subjective?

[David Wagner]

Toby Murray writes:
>Suppose we have a system represented as the following CSP process:
>
>P = a1 -> a2 -> b -> STOP [] 
>    b -> STOP
>
>Now suppose that actions a1 and a2 are performed by some object Alice
>and b is performed by another object Bob. Does Alice have authority to
>cause Bob to perform b?

I'm not convinced this provides a suitable framework for thinking
about authority.

Reasoning about authority requires reasoning about counterfactuals.  
More specifically, it requires reasoning about what would have happened
had Alice made a different choice.  For instance, we ask: What happens
if we Alice chooses to perform action X?  What happens if Alice chooses
not to perform action X?

If we can identify some action X, such that (a) if Alice chooses to
perform X, then Y inevitably ensues, and (b) if Alice chooses not to
perform X, then Y cannot follow, then I think at that point we might
be in a position to declare that Alice has authority to cause or not
cause Y.  This requires reasoning about both a real-life Alice that
will choose to perform X and an imaginary counterfactual Alice' that
will refuse to perform X.

However, it looks to me like your framework does not provide any way
to reason about Alice's "choices" or what freedom Alice does and does
not have.  Your framework does not provide the ability to reason about
counterfactual imaginary Alices, or to characterize the scope of what
Alice can and cannot choose to do.  Alice's actions are constrained by the
underlying system and by what the security monitor will allow her to do,
but as long as she plays "within the rules of the game", our framework had
better account for the fact that Alice can choose among many strategies
for playing this game.  But that doesn't show up in your framework.

I wonder if the non-determinism in CSP might be confusing things.
Thinking about causality -- even coming up with a satisfactory definition
of causality -- is harder when non-determinism is floating around, and
it's harder to get a good intuition on this.

It looks to me like you're trying to use the non-determinism in CSP
as a way to model the actors' choices, but I have doubts about whether
it is the right approach to that.  At the heart of the matter is *who*
chooses which of the many non-deterministic paths will be followed.
When we reach a non-deterministic choice point, who should we think of
as choosing which transition to take?  I suspect that in your intuition
you are tempted to think "Alice chooses whether to take the a1 transition
or not", but that isn't supportable by CSP, because CSP doesn't allow
you to make distinctions about who is choosing which transition to take.
I think in CSP we have to think about this as though the Environment
is making these choices, and the Environment is a fourth actor who
you haven't accounted for.

If you ask me, I would suggest starting from a different framework.
Let me sketch one that might support the kind of investigation I think
you are interested in taking.  Suppose the actors are Actors={A,B,C,...}.
Treat A as the name of an actor, not as the specification of a process
itself.  Introduce a map I : Actors -> Processes, where Processes might
be the set of CSP processes or the set of all finite-state automata
or you name it (the framework will need to choose one).  I(A) is A's
implementation.  Also, model the security restrictions imposed by the
underlying system as a set of admissible values of I.  The admissibility
constraints determine which "moves" are allowable by "the rules of the
game", and I(A) models A's strategy.  (For instance, in an ACL system, the
admissibility constraints ought to model that I(A) cannot access resource
R unless A appears in R's ACL; in a capability system, the admissibility
constraints should require that I(A) can only invoke a capability C if
I(A) received C from some other process or if I(A) created C.)

Then you need to introduce some way to model communication between
the actors.  For instance, you might specify: there are n^2 communication
channels, one for every pair (A,B) of actors; each channel is a queue of
elements from some alphabet \Sigma; I(A) can append an element to the
end of any channel ch(A,.), and I(B) can pop an element from the front
of any channel ch(.,B), but not vice versa; and channels are in-order
and reliable.

Now we can use the semantics of the process and communication model
to assign a semantics to each choice of I.  In other words, the map I
determines the behavior (or possible behaviors) of the composed system.

We need a notion of "equivalence" of behaviors; write I ~_B I* if
the behavior(s) of B in the system I is "equivalent" to the behavior(s)
of B in the system I*.  For instance, we might consider them
"equivalent" if the set of possible traces of B in I is equal to
the set of possible traces of B in I*, or we might consider them
"equivalent" if there is a bisimulation between the B-part of I
and the B-part of I*.  The choice of our notion of "equivalence"
is another paremater of this family of frameworks; the framework
will need to choose one.  The key part is that equivalence only looks
at the behavior(s) of B, and ignores the behaviors of all other
components of the system.

Suppose we want to determine whether A has any authority over B.
In what follows, let I,I* denote two admissible maps that differ
only at A: i.e., I(X)=I*(X) for all X!=A (but possibly I(A)!=I*(A)).
Say that A has no authority over B if for all I,I*, we have
I ~_B I*.  Say that A has some authority over B if there exists
I,I* such that I ~_B I* does not hold.  (Note that in the latter case
A's authority might be partial, such as the case where A's influence
over B is subject to C's approval.  Also we will be heavily reliant
upon choosing a good notion of "equivalence".)

I have a gut feeling this kind of definition might more or less coincide
with our intuition about what we mean by authority, though that hypothesis
remains to be explored.  What do you think?

One aspect of authority this definition doesn't encompass is secrecy.
It doesn't allow us to formalize statements like "A has authority to
learn the secret key K"; it only allows us to formalize statements about
side effects.

This definition does have the benefit of being objective, so if we agree
that this comes close to matching what we intuitively mean by authority,
then maybe that helps answer your question about whether authority is
objective or subjective.