A formal modeling and analysis approach for access control rules, policies, and their combinations

详细信息    查看全文

• 作者：Vahid R. Karimi ; Paulo S. C. Alencar…
• 关键词：Access control (AC) ; XACML ; AC combining algorithms ; Modeling ; Analysis
• 刊名：International Journal of Information Security
• 出版年：2017
• 出版时间：February 2017
• 年：2017
• 卷：16
• 期：1
• 页码：43-74
• 全文大小：
• 刊物类别：Computer Science
• 刊物主题：Data Encryption; Computer Communication Networks; Operating Systems; Coding and Information Theory; Management of Computing and Information Systems; Communications Engineering, Networks;
• 出版者：Springer Berlin Heidelberg
• ISSN：1615-5270
• 卷排序：16

文摘

Approaches to access control (AC) policy languages, such as eXtensible access control markup language, do not provide a formal representation for specifying rule- and policy-combining algorithms or for verifying properties of AC policies. Some authors propose formal representations for these combining algorithms. However, the proposed models are not expressive enough to represent formally history-based classes of these algorithms, such as ordered-permit-overrides. In addition, some other authors propose a formal representation but do not present automated support for formal verification of properties of AC policies that use these algorithms. This paper demonstrates a new representation that can express all existing AC rule and policy combinations of which the authors are aware. This representation can also be used to automate the formal verification of properties of AC policies related to these algorithms. A new modeling representation for rule- and policy-combining algorithms based on state machines is used to specify rule- and policy-combining algorithms. Examples of these algorithms are programmed in the language of the SPIN model checker, and the programs are then used to support the automated formal verification of properties of AC policies. We present our approach and then use the AC policies and properties of CONTINUE, a conference management system, to compare it with prior work. Our first contribution is a new modeling representation for combining algorithms based on state machines. The second contribution is the formal verification of AC properties under certain combining algorithms that are beyond the capability of other approaches.