First-Order Logic for Flow-Limited Authorization
Cryptography and Security
2020-12-11 v1 Logic in Computer Science
Programming Languages
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 theorems in this paper are proven in Coq.
Keywords
Cite
@article{arxiv.2001.10630,
title = {First-Order Logic for Flow-Limited Authorization},
author = {Andrew K. Hirsch and Pedro H. Azevedo de Amorim and Ethan Cecchetti and Ross Tate and Owen Arden},
journal= {arXiv preprint arXiv:2001.10630},
year = {2020}
}
Comments
Coq code can be found at https://github.com/FLAFOL/flafol-coq