Fibred SecurityLanguage

摘要

We study access control policies based on the says operator by introducinga logical framework called Fibred Security Language (FSL) which is able to deal withfeatures like joint responsibility between sets of principals and to identify them by meansof first-order formulas. FSL is based on a multimodal logic methodology. We first discussthe main contributions from the expressiveness point of view, we give semantics for thelanguage (both for classical and intuitionistic fragment), we then prove that in order toexpress well-known properties like 'speaks-for' or land-off', defined in terms of says, wedo not need second-order logic (unlike previous approaches) but a decidable fragment offirst-order logic suffices. We propose a model-driven study of the says axiomatization byconstraining the Kripke models in order to respect desirable security properties, we studyhow existing access control logics can be translated into FSL and we give completeness forthe logic.