Reference. First-Order Logic for Flow-Limited Authorization

Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti, Ross Tate, Owen Arden · CSF · 2020 · security information-flow · DOI
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.

Cite
Cite as @hirsch_etal_2020 (helia, typst) · \cite{hirsch_etal_2020} (LaTeX)
BibTeX
bibtex · 10 lines
@inproceedings{hirsch_etal_2020,
 title = {First-Order Logic for Flow-Limited Authorization},
 author = {Hirsch, Andrew K. and Amorim, Pedro H. Azevedo de and Cecchetti, Ethan and Tate, Ross and Arden, Owen},
 year = {2020},
 url = {https://arxiv.org/abs/2001.10630},
 booktitle = {2020 IEEE 33rd Computer Security Foundations Symposium (CSF)},
 publisher = {IEEE},
 doi = {10.1109/CSF49147.2020.00017},
 pages = {123--138}
}
hayagriva YAML (typst)
yaml · 18 lines
hirsch_etal_2020:
  type: article
  title: First-Order Logic for Flow-Limited Authorization
  author:
  - Hirsch, Andrew K.
  - Amorim, Pedro H. Azevedo de
  - Cecchetti, Ethan
  - Tate, Ross
  - Arden, Owen
  date: 2020
  page-range: 123-138
  url: https://arxiv.org/abs/2001.10630
  serial-number:
    doi: 10.1109/CSF49147.2020.00017
  parent:
    type: proceedings
    title: 2020 IEEE 33rd Computer Security Foundations Symposium (CSF)
    publisher: IEEE
Download: hirsch_etal_2020.bib · hirsch_etal_2020.yml
Cites 45 works (0 here)
External (45)
hirsch_etal_2020 reference entries/refs/hirsch_etal_2020/hirsch_etal_2020.hel