Operational Semantics for DKAL: Application and Analysis

DKAL is a new expressive high-level authorization language. It has been successfully tried at Microsoft which led to further improvements of the language itself. One improvement is the separation of concerns between static core policies and dynamic workflow; important safety properties can be proved from the core policies alone, independently from the workflow. Another improvement is true decentralization; different principals live in different worlds exchanging information by means of communication and filtering assertions. We also present some complexity results.

• Type: Conference
• Year: 2009
• Where: TRUSTBUS
• Authors: Yuri Gurevich, Arnab Roy
• Keywords: Core Policies, Important Safety Properties, Security Privacy, Static Core Policies, TRUSTBUS 2009