First-Order Logic for Flow-Limited Authorization
This addresses the need for secure authorization systems in domains like security and privacy, though it appears incremental as it builds on existing logic and information-flow concepts.
The paper tackled the problem of reasoning about authorization decisions under information-flow policies by introducing FLAFOL, a first-order logic that provides a non-interference guarantee while supporting all first-order logic connectives, with all theorems proven in Coq.
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.