Linear authorization logics (LAL) are logics based on linear logic that can be used for modeling effect-based authentication policies. LAL has been used in the context of the Proof-Carrying Authorization framework, where formal proofs are constructed in order for a principal to gain access to some resource elsewhere. This paper investigates the complexity of the provability problem, that is, determining whether a linear authorization logic formula is provable or not. We show that the multiplicative propositional fragment of LAL is already undecidable in the presence of two principals. On the other hand, we also identify a first-order fragment of LAL for which provability is PSPACE-complete. Finally, we argue by example that the latter fragment is natural and can be used in practice.
展开▼
