September 2017

Formal Description and Analysis of Concepts

At the core of the deliverable Formal Description and Analysis of Concepts, is the formal language for describing the different aspects of the project, in particular policies for trust, trust translation, and delegation. These must have not only a clear syntax but also a well-defined semantics.

 

This is important for two reasons. First we want to avoid that in some corner cases it is unclear what a particular policy actually means. In fact, the formalization can often reveal when different partners from academia and industry have a slightly different understanding of an intuitive concept. Discovering and resolving such mismatches early in the project is invaluable.

Second, we want to mechanize policies, i.e., have automated verifiers to determine whether a policy is satisfied or not; obviously such a verifier cannot reason intuitively, but needs a precise algorithm to follow. With a precise semantics of the policy language it is possible to prove (or find counter-examples) that this algorithm correctly implements the policy language, or even better, automatically derive the algorithm from the policy. In fact, inspired from this latter point we have decided to go for a logic programming approach where we have only one language, the LIGHTest Trust Policy Language TPL that is based on Prolog and that allows for declarative policy specification that are directly executable as soon as all concepts are concrete.

Additionally, we envision that for greatest ease of use, we can have simple, possibly visual, languages for end users that can handle most of the common specifications and can be easily mapped into TPL. In fact such a graphical tool is a mandatory part of several other work packages. In this way TPL is a basis and frame for the entire project.

You can read the full deliverable here