Nexus Authorization Logic (NAL): Logical Results
Andrew K. Hirsch, Michael R. Clarkson

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAccess Control and Trust · Cryptography and Data Security · Distributed systems and fault tolerance
