Nexus Authorization Logic (NAL): Logical Results

TL;DR

This paper presents a revised version of Nexus Authorization Logic (NAL), including new syntax, proof theory, and semantics, with formal verification in Coq, to improve reasoning about distributed system authorization.

Contribution

It introduces a revised NAL with updated syntax, a localized hypotheses proof system, and a new Kripke semantics, all formally verified in Coq.

Findings

Proof theory is sound with respect to the new semantics

Formal proof of soundness is completed in Coq

Enhanced logical framework for distributed authorization reasoning

Abstract

Nexus Authorization Logic (NAL) [Schneider et al. 2011] is a logic for reasoning about authorization in distributed systems. A revised version of NAL is given here, including revised syntax, a revised proof theory using localized hypotheses, and a new Kripke semantics. The proof theory is proved sound with respect to the semantics, and that proof is formalized in Coq.