@inproceedings{e6af47c8865c45028b6661c49d4a2b7e,
title = "First-Order Logic for Flow-Limited Authorization",
abstract = "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.",
keywords = "authorization, authorization logic, information flow, logic, proof theory",
author = "Hirsch, \{Andrew K.\} and \{De Amorim\}, \{Pedro H.Azevedo\} and Ethan Cecchetti and Ross Tate and Owen Arden",
note = "Publisher Copyright: {\textcopyright} 2020 IEEE.; 33rd IEEE Computer Security Foundations Symposium, CSF 2020 ; Conference date: 22-06-2020 Through 25-06-2020",
year = "2020",
month = jun,
doi = "10.1109/CSF49147.2020.00017",
language = "English",
series = "Proceedings - IEEE Computer Security Foundations Symposium",
publisher = "IEEE Computer Society",
pages = "123--138",
booktitle = "Proceedings - 2020 IEEE 33rd Computer Security Foundations Symposium, CSF 2020",
address = "United States",
}