Jason (jcreed) wrote,
Jason
jcreed

Due to a very welcome coincidence, I ran into Nate Foster in the hallway who told me that Jeff Vaughan's defense was happening. Went to it --- very interesting. Seems he is a major contributor to the whole Aura thing.

While listening to the talk I noticed a funny pattern in all the examples I've ever seen in authorization logics, though, including the examples given in the talk itself: whenever you have "K says A", the proposition "A" always seems to be a negative proposition in the focusing sense! One always sees (at least in the CMU-centric set of work by Frank, Deepak Garg, Henry de Young, Lujo Bauer, Mike Reiter, etc. that I am familiar with) that the logic is set up so that A being positive is allowed, and some sense is made of it, but it never seems to be particularly useful to do so.

Moreover I think there's something philosophically kind of fishy (or at least different) about "assert"ing a positive proposition.

Let me start at the beginning then: What is a sensible "assertion" or "authorization"? What kind of thing P makes the sentence "I assert that P" or "I authorize that P" make good sense?

The most basic sensible thing to do is to assert atoms whose raw meaning is fundamentally a matter of a principal's say-so. Example: If I own file F, then "you are allowed to write to file F" is a sensible thing to put after "I assert", "I authorize". Perhaps also "you are allowed access to enter my office" to take a family of examples from the Grey project. (Indeed, I might argue that "you are allowed to write to file F" isn't quite a proper proposition in the usual sense until the moment that I prefix it with "I assert"... the question remains: allowed by whom? Someone who doesn't own the file might say that they allow you to and it wouldn't matter if they didn't own the file)

So, bear with me when I claim out of the blue that these atoms are best thought of as negative atoms.

Next, we certainly have that an implication is a sensible kind of assertion: if A is a proposition, and P is an assertion, then A → P is an assertion. Example, I might assert: if it's monday, then you are allowed to write to file F. It's clear to me that this is a useful form of assertion, because it permits reasonable real-world delegation examples like "if I'm on vacation then my grad student can have access to my office".

Next, we can imagine quantifying over various domains: this is still negative propositions. If someone has many students, modify the last example to "I authorize that, for all grad students g, if I'm on vacation then g can have access to my office".

Okay, so there's lots of negative propositions that make sense as authorizations. Big question: what sense, does it make, if any, to say:

"I authorize that 0"

where 0 is, you know, void, bottom, the unit for disjunction. I claim that this doesn't make sense as an "authorization"/"assertion" in the sense that I'm trying to get at. Right? I can't authorize that 0, because it's not up to me. 0 is just not true. It's a garden-variety proposition, not an assertion by a principal.

How then do all these authorization logics that do allow such things get off the ground? I claim that this is by making a relatively benign mumbo-jumbo-y philosophical confusion between authorization and an essentially epistemic logic that nonetheless has (a superset of) the same inference rules. Apparently, you can kind of get by allowing agents to assert contradictory things, and kind of identifying the fact that "K believes the fact that K has authorized P" with "K authorizes P" because, thanks to cut-elimination, the only proofs of the former (when P is a proper assertion) are proofs of the latter.

So I seem to be advocating using just a conservative* subset of systems that already exist and seem to work fine. Why waste that expressive power? I don't know for sure myself. I think an argument could be made, parallel to the usual story for type systems, that you're making it harder to shoot yourself in the foot and assert things you don't want to, if the syntax of the language rules out certain assertions that probably aren't what you meant, while leaving in enough stuff to handle the examples you encounter in practice.

And indeed, in my Great Breadth Of Experience (snerk) in attending talks about authorization logics, I don't recall seeing a motivated example of an authorization that wasn't negative. So there!

*which is to say, the existing systems are conservative extensions of the subsystem that I'm pointing out.
Tags: authorization, logic, modal, talks
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 11 comments