@techreport{jeannin2013dkal,
author = {Jeannin, Jean-Baptiste and Caso, Guido de and Chen, Juan and Gurevich, Yuri and Naldurg, Prasad and Swamy, Nikhil},
title = {DKAL*: Constructing Executable Specifications of Authorization Protocols},
year = {2013},
month = {March},
abstract = {Many prior trust management frameworks provide authorization logics for specifying policies based on distributed trust. However, to implement a security protocol using these frameworks, one usually resorts to a general-purpose programming language. When reasoning about the security of the entire system, one must study not only policies in the authorization logic but also hard-to-analyze implementation code.

This paper proposes DKAL*, a language for constructing executable specifications of authorization protocols. Protocol and policy designers can use DKAL*’s authorization logic for expressing distributed trust relationships, and its small rule-based programming language to describe the message sequence of a protocol. Importantly, many low-level details of the protocol (e.g., marshaling formats or management of state consistency) are left abstract in DKAL*, but sufficient details must be provided in order for the protocol to be executable.

We formalize the semantics of DKAL*, giving it both an operational semantics and a type system. We prove various properties of DKAL*, including type soundness and a decidability property for its underlying logic. We also present an interpreter for DKAL*, mechanically verified for correctness and security. We evaluate our work experimentally on several examples. Using our semantics, DKAL* programs can be analyzed for various protocol-specific properties of interest. Using our interpreter, programmers obtain an executable version of their protocol which can readily be tested and then deployed.},
publisher = {Springer Verlag},
url = {http://approjects.co.za/?big=en-us/research/publication/212-dkal-constructing-executable-specifications-of-authorization-protocols/},
pages = {139-154},
journal = {Lecture Notes in Computer Science 7781},
edition = {International Symposium on Engineering Secure Software and Systems (ESSOS 13)},
number = {MSR-TR-2012-24},
note = {International Symposium on Engineering Secure Software and Systems (ESSOS 13)},
}