Discussion:
Analyzing Authority with CSP - link broken (was: Backwater: some small progress)
(too old to reply)
Mark Miller
2007-04-29 06:04:36 UTC
Permalink
[...] Toby Murray's
<http://web.comlab.ox.ac.uk/oucl/work/toby.murray/analysing_authority.pdf>
uses another process algebra, CSP, to reason about authority. [...]
Oops. I just tried that link, and it's broken. Toby, where can this
paper be found?
--
Text by me above is hereby placed in the public domain

Cheers,
--MarkM
Toby Murray
2007-04-29 13:07:50 UTC
Permalink
Indeed. Sorry about that.
I was going to wait until we heard back from the FCS-ARSPA reviewers
until I pointed to the current draft, which is what we submitted there.

You can find it here:
http://web.comlab.ox.ac.uk/oucl/work/toby.murray/papers/analysing_authority.pdf

The analysis technique described in this newer version is quite
different from that described in the original paper. The original
version tried to extract causal relationships from Finite State
Automata. We used CSP as a means of describing such automata.

The new version works on the CSP denotational semantics directly. This
obviously makes the technique less applicable to other modelling
formalisms. However, this has a number of advantages:
+ we can use a standard CSP model checker like FDR to do the analysis
rather than having to hand craft our own tool
+ the new definitions handle nondeterminism correctly, while the old
ones didn't.
+ we can more easily compare our technique to other sorts of analyses
such as information flow analyses, that are fairly well understood in
the context of CSP.

The second point above is crucial. Nondeterminism is extremely useful
for building abstract models of systems.

The third point is also very useful. I've suspected for a while now that
standard notions of information flow like non-interference ought to be
viewable as some sort of special case of authority analysis. (The
special case being that we're restricting our attention to systems of
just two subjects: High and Low, and we're interested in finding out
whether High has absolutely no authority over Low.)

However, it probably does require a bit of familiarity with CSP and its
standard semantic models.

The basic idea is this:

suppose we're trying to determine whether some objec, o, in our system
has the power to cause some event, e, to occur. For example, o might be
Alice and e might be Carol overwriting Bill. Hence, we're trying to
determine whether Alice can cause Carol to overwrite Bill.

We look at all sequences of actions that our system as a whole can
perform. In particular, we're interested in all sequences leading up to
the event e. Using standard CSP sequence notation, we're interested in
all sequences
s ^ <e>

each s ^ <e> represents one of the ways in which the event e can occur
within our system. for each s ^ <e>, s is the sequence of events that
precedes this particular occurrence of e.

for some particular occurrence of e, represented by s ^ <e>, we can
conclude that the object o has caused e to occur if o was involved in s,
and had o not been involved in s, e wouldn't have occurred.

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.

Unfortunately, in the face of nondeterminism the above breaks down. We
might have some (nondeterministic) system in which o can't cause e to
occur, but depending on how we resolve the nondeterminism, in practice o
might be able to cause e to occur. Therefore, we need a definition of
causation that holds if and only if there is some way to resolve the
nondeterminism in a system such that when the nondeterminism is
resolved, causation holds for the deterministic system.

We go on to show that there is such a property and describe how one can
use a standard CSP model checker like FDR to test for this property. It
gets a bit involved at times, but the above is the general idea.

Please feel free to pester me about any of the details or general ideas
contained in that paper.

MarkM: I have a feeling that you've thought about causation and
authority a bit before. I came across the 'causation' page on
erights.org the other day. This work is a first attempt to try to build
a formal notion of authority from causation. It's scope is perhaps a bit
restricted, given how deeply wedded it now is to CSP. But I can't see
why a similar approach couldn't be taken with the semantics of other
process algebras (although I'm unfamiliar with them so could be
completely wrong here.)

Thanks for the interest, btw. It's exciting to know someone else is
interested in this work.

Cheers

Toby
Post by Mark Miller
[...] Toby Murray's
<http://web.comlab.ox.ac.uk/oucl/work/toby.murray/analysing_authority.pdf>
uses another process algebra, CSP, to reason about authority. [...]
Oops. I just tried that link, and it's broken. Toby, where can this
paper be found?
Mark S. Miller
2007-04-30 00:26:27 UTC
Permalink
Post by Toby Murray
MarkM: I have a feeling that you've thought about causation and
authority a bit before. I came across the 'causation' page on
erights.org the other day. This work is a first attempt to try to build
a formal notion of authority from causation.
Do you mean <http://erights.org/decision/causality/three-types.html>? Thanks
for reminding me. In terms of the taxonomy I explain on that page, I'd say:

* Horton supports an analog of "Moral Causality" -- tracking who should be
held responsible for an action, whether or not they actually caused it in the
other senses of the term.

* The authority analysis that you and Fred are doing uses an analog of "The
Causality of the Physicist". However, the treatment of non-determinism leads
to differences. For safe reasoning about confidentiality, we must take account
of causation through specificational non-determinism, i.e., covert channels.
For safe reasoning about integrity, Fred's thesis explains why he can safely
ignore covert channels. Potential overt causation is somehow usefully more
constrained than "The Causality of the Physicist", but in ways not captured by
that web page.

* Why do debuggers gain such leverage from allowing us to navigate the call
stack? The call stack represents only a very tiny fraction of the causal paths
in our programs, but these causal paths seems to have a peculiarly high hit
rate at helping us to understand what when wrong. The call stack (and
hopefully, by analogy, Causeway
<http://erights.org/elang/tools/causeway/index.html>) is perhaps like a "story
telling" view of what happened, providing us an analog of "Explanatory Causality".

I don't think I had these three tie-ins in mind when I wrote the essay, but I
do think they work. Do others find this taxonomy useful?
Post by Toby Murray
Thanks for the interest, btw. It's exciting to know someone else is
interested in this work.
Indeed. And thank you for doing interesting work!
--
Text by me above is hereby placed in the public domain

Cheers,
--MarkM
Toby Murray
2007-04-30 09:54:21 UTC
Permalink
Post by Mark S. Miller
Post by Toby Murray
MarkM: I have a feeling that you've thought about causation and
authority a bit before. I came across the 'causation' page on
erights.org the other day. This work is a first attempt to try to build
a formal notion of authority from causation.
Do you mean <http://erights.org/decision/causality/three-types.html>? Thanks
* Horton supports an analog of "Moral Causality" -- tracking who should be
held responsible for an action, whether or not they actually caused it in the
other senses of the term.
* The authority analysis that you and Fred are doing uses an analog of "The
Causality of the Physicist".
But I would hope that Physicist's causation can inform Moral causation.
I would argue that Physicist's causation is the (only?) objective input
into any decision procedure for Moral causation.

In the confused deputy example in "Authority Analysis for Least
Privilege Environments", knowing that Alice can cause Carol to overwrite
Bill allows us to decide that Alice might be responsible for Bill
becoming overwritten.

Also fortunately for us, the scope of the models that we construct will
usually prevent us from being swamped with extraneous causal events. For
example, were I modelling the holocaust, I don't expect my model would
include the Epic of Gilgamesh.

Finally, of course causation is much easier to determine for programs
than for people or historical events. I can model the behaviour of each
entity in my system to a level of detail that is proportional to the
degree to which I trust that entity. Maximally untrusted entities have
maximum behaviour. Very trusted entities have minimal behaviour that
closely approximates their specification. This enables us to more
accurately consider alternate possibilities "if event X had not been" in
our system, than when trying to predict what a person might have
otherwise done had X not occurred in the past.
Post by Mark S. Miller
However, the treatment of non-determinism leads
to differences. For safe reasoning about confidentiality, we must take account
of causation through specificational non-determinism, i.e., covert channels.
For safe reasoning about integrity, Fred's thesis explains why he can safely
ignore covert channels. Potential overt causation is somehow usefully more
constrained than "The Causality of the Physicist", but in ways not captured by
that web page.
Can you elaborate further here? I can't discern your meaning.
Pierre THIERRY
2007-05-07 10:23:54 UTC
Permalink
Post by Toby Murray
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?

Curiously,
Pierre
--
***@levallois.eu.org
OpenPGP 0xD9D50D8A
David Hopwood
2007-05-07 16:35:08 UTC
Permalink
Post by Pierre THIERRY
Post by Toby Murray
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. Let's work through it:

If s is the sequence
<alice sends carol <- shakeLeftHand(), bob sends carol <- shakeRightHand()>
and e is "carol sends ted <- run()",

then removing "alice sends carol <- shakeLeftHand()" from s to give
s'_a = <bob sends carol <- shakeRightHand()>, we see that e cannot follow s'_a

and removing "alice sends carol <- shakeLeftHand()" from s to give
s'_b = <bob sends carol <- shakeRightHand()>, we see that e cannot follow s'_b.

I.e. the definition says that both alice and bob are involved in the causal
chain that leads to run() being sent to ted.


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.

The problem here also occurs in simpler examples, e.g. if we get rid of
shakeRightHand() and bob, and program carol to send ted <- run() if it receives
just shakeLeftHand(), then we conclude incorrectly that neither alice nor david
have authority to cause e.


[*] I prefer lowercase for process names.
--
David Hopwood <***@industrial-designers.co.uk> (note new address)
David Hopwood
2007-05-07 16:54:30 UTC
Permalink
David Hopwood wrote:
[...]
Post by David Hopwood
The definition above says that both alice and bob [*] have (partial) authority
If s is the sequence
<alice sends carol <- shakeLeftHand(), bob sends carol <- shakeRightHand()>
and e is "carol sends ted <- run()",
then removing "alice sends carol <- shakeLeftHand()" from s to give
s'_a = <bob sends carol <- shakeRightHand()>, we see that e cannot follow s'_a
and removing "alice sends carol <- shakeLeftHand()" from s to give
s'_b = <bob sends carol <- shakeRightHand()>, we see that e cannot follow s'_b.
Sorry, cut-and-paste error (the conclusion is unchanged).

and removing "bob sends carol <- shakeLeftHand()" from s to give
s'_b = <alice sends carol <- shakeRightHand()>, we see that e cannot follow s'_b.
Post by David Hopwood
I.e. the definition says that both alice and bob are involved in the causal
chain that leads to run() being sent to ted.
The second example was correct.
--
David Hopwood <***@industrial-designers.co.uk> (note new address)
David Hopwood
2007-05-08 01:50:06 UTC
Permalink
Post by David Hopwood
Sorry, cut-and-paste error (the conclusion is unchanged).
and removing "bob sends carol <- shakeLeftHand()" from s to give
s'_b = <alice sends carol <- shakeRightHand()>, we see that e cannot follow s'_b.
I must not be paying attention. It should have been:

and removing "bob sends carol <- shakeRightHand()" from s to give
s'_b = <alice sends carol <- shakeLeftHand()>, we see that e cannot follow s'_b.
--
David Hopwood <***@industrial-designers.co.uk> (note new address)
Pierre THIERRY
2007-05-07 23:55:09 UTC
Permalink
Post by David Hopwood
I.e. the definition says that both alice and bob are involved in the
causal chain that leads to run() being sent to ted.
That's not exactly the wording of the original definition, which said "o
has the authority to cause e to occur". Here it would then conclude that
alice or bob each has the authority to run ted, which seems erroneous to
me, because alice cannot run ted without bob's help and vice versa.

Curiously,
Pierre
--
***@levallois.eu.org
OpenPGP 0xD9D50D8A
David Hopwood
2007-05-08 02:05:37 UTC
Permalink
Post by Pierre THIERRY
Post by David Hopwood
I.e. the definition says that both alice and bob are involved in the
causal chain that leads to run() being sent to ted.
That's not exactly the wording of the original definition, which said "o
has the authority to cause e to occur". Here it would then conclude that
alice or bob each has the authority to run ted, which seems erroneous to
me, because alice cannot run ted without bob's help and vice versa.
That's a valid point, although arguably "o is involved in the causal chain
that leads to e" is still useful for security analysis, since then we know
that it *may* be possible to prevent e by excluding some behaviours of o.

(The definition does not guarantee that we can prevent e by excluding some
behaviours of o. If o is not involved in the causal chain that leads to e,
OTOH, then we know that changing the behaviour of o is useless in trying
to prevent e.)

In any case, the definition doesn't seem to correspond to an intuitive
notion of authority in cases where the same event can happen as a result
of causal chains involving any of several principals. I'm curious to hear
Toby's response to that.
--
David Hopwood <***@industrial-designers.co.uk>
Toby Murray
2007-05-08 09:48:58 UTC
Permalink
Post by David Hopwood
Post by Pierre THIERRY
Post by David Hopwood
I.e. the definition says that both alice and bob are involved in the
causal chain that leads to run() being sent to ted.
That's not exactly the wording of the original definition, which said "o
has the authority to cause e to occur". Here it would then conclude that
alice or bob each has the authority to run ted, which seems erroneous to
me, because alice cannot run ted without bob's help and vice versa.
Technically, the defn says that both alice and bob each have authority
to cause the event "ted.run()" to occur. Each can cause it to occur
(provided the other takes part too). This fits with my intuition, but
intuition is often a subjective thing.

In either case, whatever you intuition, having a definition of authority
that errs on the side of caution is often a good thing from a security
standpoint. Certainly having a definition that underestimates a
subject's authority is not a good thing. Hence, I think having a defn
that excludes the possibility that alice or bob has authority to run ted
would be dangerous, since clearly both can cause ted to run (but not
alone).

If one wanted to find out whether alice has authority to cause ted to
run without bob's help, then one could perform the same analysis
restricting one's attention to all traces that don't contain any "bob"
events.

In this case, we wouldn't even find any traces with "ted.run()" in them.
Hence, we can easily find out whether a subject is able to cause an
event without another subject's help -- if that's what you're interested
in.

There are other variations on this sort of analysis that can tell you
other things such as whether a particular subject has exclusive
authority to cause some event, and so on. In each case, we restrict our
attention to a subset of the total set of traces for our system.


<snip>
Post by David Hopwood
In any case, the definition doesn't seem to correspond to an intuitive
notion of authority in cases where the same event can happen as a result
of causal chains involving any of several principals. I'm curious to hear
Toby's response to that.
See my response to the original message and my apologies for the delay.
I've been away from email for a couple days.

Cheers

Toby
Toby Murray
2007-05-08 09:32:56 UTC
Permalink
Post by David Hopwood
Post by Pierre THIERRY
Post by Toby Murray
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>
Post by David Hopwood
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.

Similarly, if we remove all "alice" or "bob" events from s'_d, we see
that e cannot follow.

Hence, both david, alice and bob have authority to cause e.

Not that I'm saying that there aren't counter examples for which this
analysis might not work. There may well be and I'm very interested in
any discussion of the deficiencies of this sort of thing.

Cheers

Toby
David Hopwood
2007-05-08 14:06:47 UTC
Permalink
Post by Toby Murray
Post by David Hopwood
Post by Pierre THIERRY
Post by Toby Murray
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>
Post by David Hopwood
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 <***@industrial-designers.co.uk> (note new address)
Toby Murray
2007-05-08 15:18:09 UTC
Permalink
Post by David Hopwood
Post by Toby Murray
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
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.
Post by David Hopwood
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.
Post by David Hopwood
(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.
Post by David Hopwood
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.
Post by David Hopwood
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.
Post by David Hopwood
I think that this is still not the definition we want for most purposes.
{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,
{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.
Post by David Hopwood
{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.

Loading...