formalization

[bblfish]

Any access control layer for Solid will need mathematically based formalization. Why here more than elsewhere?

Authorization and Authentication are achieved by communication between clients and servers attempting to coordinate action. A client needs to know what resources it can access in what mode and which credentials to show. This gives rise to a fundamental client-server symmetry, or perhaps rather a duality. The role of the Guard on the server is one of verification of credentials according to access control rules. The role of the client is to decide which credentials to offer that will give it access. These rules need to be stated independently of the implementation, since we will continue to have many different implementations.

In an antagonistic environment, just working with probability of failure is not an option. Put in software engineering terms: unit tests alone will not do. This is because any failure - however unlikely it is - will, when discovered, be abused by an antagonist to its full potential, making an unlikely failure into a likely or even constant threat. This threat will reduce trust in the ability of agents to cooperate safely on Solid, and hence reduce its growth.

We thus have two reasons for the need for mathematical formalization. 1) description independent of implementation 2) proof of the correctness of the protocol.

Where should we start? We should of-course try to build on the best work in this area. RDF provides a framework for publishing data, but the OWL specs building as they do on RDF, has the most to say about reasoning on the web, using many features that are needed by our protocol, and was designed with a thought on being understandable for "end users", for the web, and with close attention to issues of complexity. This is unlikely to be all that is needed, but it can already provide a big step forward, and provide some grounding, opening views on other needed formalization steps.

I could now give a few examples of how I see this working with ACP, but as it is very likely that I will make a formalization mistakes, I will instead start sub-issues with ideas on how this can be done and link them to this issue.