论文标题
一阶逻辑用于流量限制授权
First-Order Logic for Flow-Limited Authorization
论文作者
论文摘要
我们介绍了流量限制的授权一阶逻辑（FLAFOL），这是在存在信息流策略的情况下进行有关授权决策的逻辑。我们将Flafol证明系统形式化，表征其证明理论特性并开发其安全保证。特别是，Flafol是第一个提供非干预保证的逻辑，同时支持一阶逻辑的所有连接剂。此外，此保证是第一个从授权逻辑和信息流系统中结合非干预概念的一种保证。本文中的所有定理在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.
