ARBAC策略的自动化符号分析（扩展版）
密码学与安全
2010-12-30 v1 计算机科学中的逻辑
摘要
管理访问控制策略最广泛的框架之一是管理型基于角色的访问控制（ARBAC）。已经提出了几种自动化分析技术来帮助维护ARBAC策略的理想安全属性。许多可用技术的一个局限性是用户和角色集合是有界的。在本文中，我们提出了一个符号框架来克服这一困难。我们通过采用最近用于模型检查无限状态系统的方法，这些方法使用一阶逻辑和最先进的定理证明技术，设计了一种参数化用户和角色数量的自动化安全分析技术。使用原型实现的初步实验似乎证实了我们技术的可扩展性。
引用
@article{arxiv.1012.5590,
title = {Automated Symbolic Analysis of ARBAC-Policies (Extended Version)},
author = {A. Armando and S. Ranise},
journal= {arXiv preprint arXiv:1012.5590},
year = {2010}
}
备注
Long version of the paper entitled "Automated Symbolic Analysis of ARBAC Policies" published in Proc. of 6th Int. Workshop on Security and Trust Management (co-located with EUROPKI'10, CRITIS'10, and ESORICS'10), Athens, Sept. 23-24 (2010). Also, to appear in LNCS