cs.CR cs.LO cs.PL
First Order Logic for Flow Limited Authorization. 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 theorems in this paper are proven in Coq.