Access Control and Negation

[bblfish]

We have use cases that require negation such as Block access to agents and ACP has constructs such as noneOf and an acp:deny mode as discussed in the Teleconf on 28-April, which also require negation. This has quite dramatic implications for how reasoning can be handled.
Let me explain.

Regular and Geometric Logic

It is important here to realize that first order logic comes in two complementary pieces:

• regular logic: a positive fragment with conjunction, existential quantifiers (blank nodes) and a concept of Truth,
• geometric logic: a negative fragment - the dual - with disjunction and Falsity (and so universal quantification I think)

This is shown very clearly in @epatters' "§8 Categorical Logic" chapter of the paper Knowledge Representation in Bicategories of Relations.

In the chapter 9 Patterson looks at what happens when a dual concept of disjunction is added to the category: this gives us coherent logic also known as geometric logic. One can find an nice explanation of how this ties in with computing on the web site Skolem Machines.

The advantage of Category Theory is that it helps bring out these fundamental symmetries and dualities, which can otherwise get lost in a sea of details. Once this duality is clearly understood another very good article to look at is the OWL 2 Profiles: An Introduction to Lightweight Ontology Languages paper, as that explains clearly why the OWL language fragments were chosen as they were. An import diagram is this one:

Where negation appears (in the antecedent or consequence of a rule is important here).

Relevance to Access Control

There are going to be many different ways this is relevant, but below are some initial thoughts.

WAC and regular logic

The current WAC spec is conceived within the framework of regular logic. This has a number of advantages, especially regarding efficiency of calculations. For if one does not have negation then, to find if some agent has access to a resource, it suffices to find a positive statement of that fact. So if we had an Access Control Resource (ACR) that :imports other ACRs then the Guard protecting access to the resource or the Guard protecting the divulging of credentials on the client, could stop at the first rule that gave access to the given resource. There would be no need to look further.
I think this fragment is covered by OWL2 Rule Language fragment of OWL which states:

The OWL 2 RL profile is aimed at applications that require scalable reasoning without sacrificing too much expressive power.

ACP and geometric logic

As ACP is moving into the space where negation and disjunction are allowed, expressible in OWL as using concepts such as union, complementOf the search for a matching rule is going to be quite different.

First of all, it will be necessary to look at ALL the rules, even after having found a positive match, since a later rule could make a negative statement about the individual requesting access. Second I think one may also need to search not just for positive properties of the individual authenticating but for logical consequences of those properties, since some of those may exclude the user.

Todo

In any case it will be important for a Guard to know if the access control rules contain any such negative statements, as that will determine if it can stop on a positive answer or if it has to continue searching for negatives.

This should be visible to a client and server guard as quickly as possible on reaching the access control rules, so that it does not need to search through linked-to or imported acls if it does not need to.

What is the best way for this to be made visible?

[elf-pavlik]

First of all, it will be necessary to look at ALL the rules, even after having found a positive match, since a later rule could make a negative statement about the individual requesting access.

I believe that everyone supporting negation understands that and accepts that consequence.

Second I think one may also need to search not just for positive properties of the individual authenticating but for logical consequences of those properties, since some of those may exclude the user.

Could you please provide example illustrating it? Preferably based on one of the use cases included in UCR draft. Otherwise extended version of one of those use cases or new use case if needed be.

[bblfish]

So I think we agree that

• negation leads to a different verification algorithm
• WAC does not use negation
• there are good use cases for both
• if one wants to support both regular and geometric logic, then one needs a way to make it clear which is being used

[elf-pavlik]

there are good use cases for both

I don't think we should rush to conclusion that negation lowers performance in significant way and would cause issues. I wouldn't expect access policies to reach size of DBpedia dump.

Let's be careful not to fall into premature optimization.

[matthieubosquet]

negation leads to a different verification algorithm

Yes

WAC does not use negation

Yes

there are good use cases for both

If by "both" you mean "both algorithms", I would agree with Elf that optimisations in the ACP resolution algorithm might mean the use of geometric logic wouldn't necessarily significantly impact performance. Obviously, coming up with cases where geometric logic would be really expensive computationally will be easy, but I don't think that is what we're trying to prove here.

if one wants to support both regular and geometric logic, then one needs a way to make it clear which is being used

Yes. I am not extremely familiar with that terminology, but it seems like the correct level of abstraction for this discussion and drawing the parallel explicitly seems valuable to me. I'm also keen to learn the category theory concepts, please don't hesitate to point out if the way I interact with you through those seems erroneous.

Might we say that when using intersection, exclusion and denying of access modes, one moves from the realms of regular to geometric logic?

And would it be correct to state that as long as someone restricts themselves to unions and allowing of access modes, one remains in the realm of regular logic?

Hence that both regular and geometric logic are indeed supported by ACP or in other words that if ACP allows the use of the latter, it doesn't impose it?

[bblfish]

Hence that both regular and geometric logic are indeed supported by ACP or in other words that if ACP allows the use of the latter, it doesn't impose it?

Certainly, ACP is not yet finished, so there may be mechanisms that can be put in place to deal with the topic of this thread.
There has to be a way to make explicit what the reasoning is going to be.

[kjetilk]

there are good use cases for both

I don't think we should rush to conclusion that negation lowers performance in significant way and would cause issues. I wouldn't expect access policies to reach size of DBpedia dump.

Let's be careful not to fall into premature optimization.

I don't think this falls into the category of premature optimization at all. We can certainly use formal methods to study the impact of a decision before it becomes a problem, and we really need to do that, that's just hygiene.

My greatest fear is that we introduce things that becomes deeply ingrained and so the cost of change becomes high. By using formal methods, we can study realistic scenarios and then assess their impact. Yes, we don't expect access policies to reach the size of the DBpedia dump, but what do we expect, and how can we qualify those expectations a decade from now?