First-Order Logic for Flow-Limited Authorization

Authorization policies and information-flow policies interact in complex ways. We give a first-order authorization logic that is aware of information-flow policies


Andrew K. Hirsch, Pedro H. Azevedo Amorim, Ethan Cecchetti, Ross Tate, and Owen Arden


We present the Flow-Limited Authorization First-Order Logic (FLAFOL), a logic for reasoning about authorization decisions in the presence of information-flow policies. We formalize the FLAFOL proof system, characterize its proof-theoretic properties, and develop its security guarantees. In particular, FLAFOL is the first logic to provide a non-interference guarantee while supporting all connectives of first-order logic. Furthermore, this guarantee is the first to combine the notions of non-interference from both authorization logic and information-flow systems. All the theorems in this paper are proven in Coq.

Publication History

Appeared in CSF 2020.
A talk on this material appeared in FCS 2019.


Official Version

Technical Report

<span>%d</span> bloggers like this: