March 2014 SIEP Workshop

The March 2014 SIEP Workshop takes place at the University of Luxembourg, Campus Kirchberg. On Tuesday an Wednesday, it takes place in room E112, on Thursday in the Salle du Conseil.

Program

For the talks marked with (*) you can find an abstract below.

Tuesday, 11 March
14:30-15:30: Guillaume Aucher: A dynamic logic for privacy compliance (*)
15:45-16:45: Marc Denecker: Default and Autoepistemic logic – Default logic is not a logic of defaults (*)
17:00-18:00: Yang Zhang: A New Access Control Scheme for Facebook-style Social Networks (*)

Wednesday, 12 March
10:00-11:00: Marcos Cramer (supported by Deepak Garg): The Stateful Authorization Logic BL – Proof Theory and Sketch of a Semantics
11:15-12:15: Discussion about BL Semantics and a Completeness Proof
Lunch Break
14:00-15:00: Discussion about Using BL Semantics for Decidability Results for Fragments of BL
15:00-16:00: Marcos Cramer, Agustín Ambrossio: Modelling Delegation and Revocation Schemes in IDP
16:15-17:15: Pieter Van Hertum: Using a declarative specification for execution and simulation: Delegation and Revocation Schemes

Thursday, 13 March
09:30-10:30: Marcos Cramer: A Rich Classification Framework for Revocation Schemes
10:30-11:30: Dov Gabbay: Delegation, Count as, and Security in Talmudic Logic (*)
11:45-12:45: Final Discussion about Plans for Further Collaboration

Abstracts

Guillaume Aucher: A dynamic logic for privacy compliance

Knowledge based privacy policies are more declarative than traditional action based ones, because they specify only what is permitted or forbidden to know, and leave the derivation of the permitted actions to a security monitor. This inference problem is already non trivial with a static privacy policy, and becomes challenging when privacy policies can change over time. We therefore introduce a dynamic modal logic that permits not only to reason about permitted and forbidden knowledge to derive the permitted actions, but also to represent explicitly the declarative privacy policies together with their dynamics. The logic can be used to check both regulatory and behavioral compliance, respectively by checking that the permissions and obligations set up by the security monitor of an organization are not in conflict with the privacy policies, and by checking that these obligations are indeed enforced.

Marc Denecker: Default and Autoepistemic logic – Default logic is not a logic of defaults

A fact apparently not observed earlier in the literature of nonmonotonic reasoning is that Reiter, in his default logic paper, did not directly formalize informal defaults. Instead, he translated a default into a certain natural language proposition and provided a formalization of the latter. A few years later, Moore noted that propositions like the one used by Reiter are fundamentally different than defaults and exhibit a certain autoepistemic nature. Thus, Reiter had developed his default logic as a formalization of autoepistemic propositions rather than of defaults.

The first goal of this paper is to show that some problems of Reiter's default logic as a formal way to reason about informal defaults are directly attributable to the autoepistemic nature of default logic and to the mismatch between informal defaults and the Reiter's formal defaults, the latter being a formal expression of the autoepistemic propositions Reiter used as a repesentation of informal defaults.

The second goal of our paper is to compare the work of Reiter and Moore. While each of them attempted to formalize autoepistemic propositions, the modes of reasoning in their respective logics were different. We revisit Moore's and Reiter's intuitions and present them from the perspective of autotheoremhood, where theories can include propositions referring to the theory's own theorems. We then discuss the formalization of this perspective in the logics of Moore and Reiter, respectively, using the unifying semantic framework for default and autoepistemic logics that we developed earlier. We argue that Reiter's default logic is a better formalization of Moore's intuitions about autoepistemic propositions than Moore's own autoepistamic logic.

Yang Zhang: A New Access Control Scheme for Facebook-style Social Networks

The popularity of online social networks (OSNs) makes the protection of users’ private information an important but scientifically challenging problem. In the literature, relationship-based access control schemes have been proposed to address this problem. However, with the dynamic developments of OSNs, we identify new access control requirements which cannot be fully captured by the current schemes. In this talk, we focus on public information in OSNs and treat it as a new dimension which users can use to regulate access to their resources. We define a new OSN model containing users and their relationships as well as public information. Based on this model, we introduce a variant of hybrid logic for formulating access control policies. A type of category relations among public information are exploited to further improve our logic for its usage in practice. In the end, we propose a few solutions to address the problem of information reliability in OSNs.

Dov Gabbay: Delegation, Count as, and Security in Talmudic Logic

Delegation is a commonplace feature in our society. Individuals give power of attorney to their lawyers to perform certain actions for them (e.g. buy or sell property), institutions delegate to certain employees to sign for them (human resources send letters of appointment) and owners can grant access and administrative rights to other people in relation to their servers.

The logic behind such a system has been studied by several communities. In philosophy this is known as “count as”. X counts as Y in context C. In law there are various rules for power of attorney. In computer science one talks about access control and delegation. This paper examines the approach to delegation in Talmudic Logic.

The current approaches to delegation, mainly study three features
1. Dominance — if several primary sources delegate to secondary sources who carry on delegating then what is the dominance relationship among the chains of delegations
2. Revocation — if some sources revoke the delegation or some change their minds and reinstate, how does this propagate through the chains of delegations?
3. Resilience — if one source revokes delegation do we cancel other delegations from other sources on the grounds that we now do not trust the delegate?

In the literature systems have been constructed which either model or implement a calculus of Delegation-Revocation ( Privilege calculus). Their purpose is to answer the question of whether the chain of delegation and revocations can allow an agent to perform an action and their models are chain update models.

The Talmudic approach is slightly different not only in the details of its model but also in its point view.

The Talmud not only examines the procedure of the actual acts of delegation and revocation and its calculus but also includes the analysis of ordinary actions (not just chain update actions) — their elements of agency, action, deliberation and competence. These attributes have preconditions addressing not only acts but also delegation and revocation chains leading to the actions. The Talmud also addresses cases of delegated agents unable to execute the actions for various reasons, and the possibility of agents going mad or dying during the delegation revocation process, with their repercussions.