DKAL

Distributed Knowledge Authorization Language, in short DKAL, is a logic-based language for decentralized polices. Originally it was aimed for authorization policies, but in fact it is appropriate for policies in general. In DKAL world, principals have their own states and compute their own knowledge. DKAL facilitates the analysis of policies. Are the given policies consistent? Do they comply with various regulations? Is privacy protected? And so on.

Publications

[5] Yuri Gurevich and Itay Neeman
DKAL 2 --- A Simplified and Improved Authorization Language
Microsoft Research Tech Report, February 2009.

Knowledge and information are central notions in DKAL, a logic based authorization language for decentralized systems, the most expressive among such languages in the literature. Pieces of information are called infons. Here we present DKAL 2, a surprisingly simpler version of the language that expresses new important scenarios (in addition to the old ones) and that is built around a natural logic of infons. Trust became definable and its properties, postulated earlier as DKAL house rules, are now proved. In fact, none of the house rules postulated earlier is now needed. We identify also a most practical fragment of DKAL where the query derivation problem is solved in linear time.

[4] Yuri Gurevich and Itay Neeman
The Infon Logic
Bulletin of European Association for Theoretical Computer Science Number 98, June 2009

Infons are pieces of information. In our work DKAL (Distributed Knowledge Authorization Language), we discovered that logic of infons is a conservative extension of intuitionistic logic by means of connectives ``p said" and ``p put" where p ranges over principals. Here we investigate infon logic and a primal fragment of it. In both cases, we formulate an infon calculus, develop a Kripke-type model theory, prove soundness and completeness, and prove the subformula property that is important for computational complexity. We stratify primal logic by quotation depth. In applications, quotation depth is small. Our most involved technical result is this: The derivability problem for any bounded-depth fragment of primal logic is solvable in linear time. One consequence is that the (ground) derivability problem (whether a given query follows form the given ground hypotheses) for SecPAL is solvable in linear time. SecPAL is a precursor of DKAL and expresses many important access control scenarios.

[3] Yuri Gurevich and Arnab Roy
Operational Semantics for DKAL: Application and Analysis
TrustBus 2009, 6th International Conference on
Trust, Privacy and Security in Digital Business.

DKAL is a new authorization language based on existential fixed-point logic and more expressive than existing authorization languages in the literature. We present some lessons learned during the first practical application of DKAL and some improvements that we made to DKAL as a result. We develop operational semantics for DKAL and present some complexity results related to the operational semantics.

[2] Yuri Gurevich and Itay Neeman
DKAL: Distributed-Knowledge Authorization Language
21st IEEE Computer Security Foundations Symposium (CSF 2008), pp. 149-162.
Extended abstract of 1.

DKAL is a new declarative authorization language for distributed systems. It is based on existential fixed-point logic and is considerably more expressive than existing authorization languages in the literature. Yet its query algorithm is within the same bounds of computational complexity as e.g. that of SecPAL. DKAL’s communication is targeted which is beneficial for security and for liability protection. DKAL enables flexible use of functions; in particular principals can quote (to other principals) whatever has been said to them. DKAL strengthens the trust delegation mechanism of SecPAL. A novel information order contributes to succinctness. DKAL introduces a semantic safety condition that guarantees the termination of the query algorithm.

[1] Yuri Gurevich and Itay Neeman
DKAL: Distributed-Knowledge Authorization Language
       First appeared as
Microsoft Research Technical Report MSR-TR-2007-116, August 2007.
       This version is
Microsoft Research Technical Report MSR-TR-2008-09, January 2008.

DKAL is an expressive declarative authorization language based on existential fixed-point logic. It is considerably more expressive than existing languages in the literature, and yet feasible. Our query algorithm is within the same bounds of computational complexity as e.g. that of SecPAL. DKAL's distinguishing features include

  • explicit handling of knowledge and information,
  • targeted communication that is beneficial with respect to confidentiality, security, and liability protection,
  • the flexible use and nesting of functions, which in particular allows principals to quote (to other principals) whatever has been said to them,
  • flexible built-in rules for expressing and delegating trust,
  • information order that contributes to succinctness.