使用 Prover9 自动验证基于角色的访问控制策略约束
密码学与安全
2015-03-27 v1
摘要
访问控制策略用于限制仅对授权用户访问敏感记录。指定策略的一种方法是使用基于角色的访问控制 (RBAC)，其中授权被授予角色而非用户。用户被分配给角色，使得每个用户可以访问其角色允许的所有记录。RBAC 因其灵活性而备受关注。RBAC 中的一个问题是处理约束。通常，策略应满足预定义约束，例如职责分离 (SOD) 规定不允许用户扮演两个冲突角色。基于策略验证约束的可满足性是耗时的且可能导致错误。因此，自动化验证至关重要。在本文中，我们提出了一个在一阶逻辑中指定策略和约束的理论。此外，我们给出了一个全面的约束列表。我们基于用户与角色之间、角色与记录权限之间、用户与记录权限之间、以及用户、角色与记录权限之间的关系来标识约束。然后，我们使用称为 Prover9 的通用定理证明器工具来证明约束的满足性。
引用
@article{arxiv.1503.07645,
title = {Automated Verification Of Role-Based Access Control Policies Constraints Using Prover9},
author = {Khair Eddin Sabri},
journal= {arXiv preprint arXiv:1503.07645},
year = {2015}
}
备注
10 pages in International Journal of Security, Privacy and Trust Management (IJSPTM) Vol 4, No 1, February 2015