is N3 modal? ABLP logic n3 examples.

[bblfish]

As I am working on extending Solid Access Control with more flexible use cases, I wanted to see how far using the Abadi, Burrows, Lampson and Plotkin (ABLP) modal logic of says could help me formalise this work. Luckily Dan Connolly in 2009 wrote up some N3 rules that are now in the repo formalising the ABLP Logic) (see pointers).

But ABLP is a modal logic. Especially these two formulas from the 1993 paper A Calculus for Access Control in Distributed Systems page 8:

\begin{align}
& \vdash A \text{ says } (s \supset s') \supset (A \text{ says } s \supset A \text{ says } s') \tag*{(A)}  \\
\text{ if } &\vdash s \text{ then } \vdash A \text{ says } s \tag*{(B)} 
\end{align}

The first formula [A] is formalised on line 42 of says.n3

{ ?A :says { ?s => ?s2 } } => { { ?A :says ?s } => { ?A :says ?s2 } }.

The second formula [B] is given by @dckc on line 43

{ ?A a :Principal. ?s a log:Truth } => { ?A :says ?s }.

I think that is an error since what [B] means is not that ?s is True, but that it is a theorem, i.e. something like owl rules. It would not make sense for a thief to think that because he knew where the stolen jewels were, that the police did so too.

In any case, those formulas are modal formulas. As we discussed a while ago, folks, I understand that members of this list believe N3 should be a first-order logic. Does that exclude it being more? It seems like it should not stop that since the says relations is pretty central to the web.

[dckc]

Hi. Thanks for tagging me on this subject. Since joining Agoric in early 2021, I have been wondering...

... what would happen if we mixed the Agoric platform's ability to scale down to clusters and single machines with the notion of a SOLID pod.

Next... whether N3 is modal... that is: how to formalize reflection in N3, is an open research problem, for me:

• reflection tag in my bibliography
• reflection tag in my blog
• reflection tag in my bookmarks

The coolest thing I've seen lately is:

• The reflective Milawa theorem prover is sound (down to the machine code that runs it). Jared Davis and Magnus O. Myreen. Journal of Automated Reasoning. Springer. August, 2015. Volume 55(2), Pages 117-183.

But the relevance of the question has faded, for me. Someone pointed out that the main result of logic research is computation. I'm now more interested in constructive logic and the curry-howard correspondence that gives rise to things like functional programming than the approach in N3. (meanwhile, Milawa uses classical logic...)

When it comes to flexible access control for Solid, I am persuaded that the question of who says something is not the core of the matter. As Stiegler said in his 2004 PictureBook of Secure Cooperation:

The patterns here do not require individual authentication. Rather, these patterns focus on authorization: ask not, “who are you?”, but rather, “are you allowed?”. This was always the crucial question anyway; by asking this better question, we get a better answer.

I have been hoping to persuade folks to use capability-based security over access control lists for quite a while now...

• Secure Mashups: CSRF-resistent alternatives to WebID 2011-07

hm... that one seems to be missing the capabilities tag

[bblfish]

@dckc: Deepak Garg's Ph.D. dissertation, 2009 Proof Theory for Authorization Logic and Its Application to a Practical File System uses the "says" modality to build a Proof Carrying Authentication based Posix File System that uses Capabilities to speed up authorization, which seems like a good idea. They use intuitionistic logic, which makes sense since the point is to prove access from the available evidence. It may also work with RDF since we can think of named graphs as proof objects.

I am just reading the paper. It seems they are using a logic that is slightly weaker than lax modality - a strange modality that contains only one operator. In the 2006 paper Access control in a core calculus of dependency Martin Abadi shows that the says operator is an indexed strong monad, if I remember correctly. The monad allows information to not leak from its context... In a later paper A Modal Deconstruction of Access Control Logics Abadi shows that one can map to an indexed version of the S4 modal logic.

I read the ACL acronym for Access Control Logic. If you have a use case you think I would struggle with, please drop a note on my dissertation github so that I can see if I can overcome it :-)

Ah yes, concerning WebID: We initially used TLS because it was deployed and worked across all browsers. Sadly it was very limited, only allowing essentially one type of credential to be used (developing ASN.1 credentials did not seem very enticing). But things are much more flexible with the new HttpBis HTTP Signature RFC, which is nearly finished. I implemented it in Scala (client and server) and have a short video demo of how it could be used for big data. For more ideas on how to tie it to WebIDs and social networks and more see my Use Cases, especially the Social Networking ones.

I want to put some demos where I can use an N3 reasoner in the next weeks to better understand those tools. So I need to start using @josd's EYE reasoner seriously.

[bblfish]

Ah I found a thread where we discussed this on the N3 mailing list in August 2001 with @doerthe and @pchampin .

[bblfish]

Also one should refer to the paper Using Semantic Web Technologies for Policy Management on the Web used N3 and already mentioned Proof Based Authentication.

[dckc]

I read the ACL acronym for Access Control Logic.

Read it where? Above, I spelled it out: "use capability-based security over access control lists".

.... Posix File System that uses Capabilities to speed up authorization

Posix capabilities are, unfortunately, not an application of Capability-based security

If you have a use case you think I would struggle with, please drop a note on my dissertation github so that I can see if I can overcome it :-)

As noted above: CSRF.

To elaborate further, see:

• 2009-02 ACLs don't Tyler Close, HP Laboratories
  Abstract: The ACL model is unable to make correct access decisions for interactions involving more than two principals, since required information is not retained across message sends. Though this deficiency has long been documented in the published literature, it is not widely understood. This logic error in the ACL model is exploited by both the clickjacking and Cross-Site Request Forgery attacks that affect many Web applications

[bblfish]

I read the ACL acronym for Access Control Logic.

Read it where? Above, I spelled it out: "use capability-based security over access control lists".

I meant to use ACL for Access Control Logic for fun. Where: the link is above.

.... Posix File System that uses Capabilities to speed up authorization

Posix capabilities are, unfortunately, not an application of Capability-based security

If you have a use case you think I would struggle with, please drop a note on my dissertation github so that I can see if I can overcome it :-)

As noted above: CSRF.

To elaborate further, see:

• 2009-02 ACLs don't Tyler Close, HP Laboratories Abstract: The ACL model is unable to make correct access decisions for interactions involving more than two principals, since required information is not retained across message sends. Though this deficiency has long been documented in the published literature, it is not widely understood. This logic error in the ACL model is exploited by both the clickjacking and Cross-Site Request Forgery attacks that affect many Web applications

Ok, you were at least the 3rd person who pointed me to that article, which comes up whenever we discuss ACLs. So I looked at it again very carefully and wrote up this detailed analysis to check whether it applies to what I am proposing to do.

https://github.com/co-operating-systems/PhD/blob/main/Logic/ACLsDont.md

My current conclusion is that it does not since we can use the modal "says that" logic, the lack of which causes the confused deputy problem. Capabilities are just intuitionistic-logic proof objects, I think, and they are very important indeed, but not without proof. And for that, one needs the right logic, and the "says" logic I think provides what we need.

[bblfish]

.... Posix File System that uses Capabilities to speed up authorization

Posix capabilities are, unfortunately, not an application of Capability-based security

I think that may be a problem with Deepak Garg's thesis, even if not a fatal one. He opened himself to the Confused Deputy problem by wanting a proof of concept he could implement and demonstrate with real unix programs without requiring them to be changed.

For the compiler to not fall prey to Confused Deputy described in "ACL's don't" he would have needed to either require that programs accept capabilities as arguments or be changed to keep track of who gave it the arguments, ie, who gave it the order to launch, so that they could correctly determine the rights from the ACL rules. On the Web, all apps need to be built to have the capability to keep track of context, which RDF datasets and languages like N3 allow us to do.