• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >A modal logic for role-based access control within the HOL theorem prover.
【24h】

A modal logic for role-based access control within the HOL theorem prover.

机译：HOL定理证明器中基于角色的访问控制的模态逻辑。

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The access-control logic of Lampson, Abadi, and their colleagues [LABW92, ABLP93] makes it possible to assure the correctness of access-control decisions by accounting correctly for identity, credentials, authority, delegation, and privileges. It can be used to describe a variety of access-control policies and to reason about their access-control decisions. However, it lacks an ability to reason about role-based access control (RBAC) [FSG+01, FBK99, FKC03, SCFY96], which is a popular technique for reducing the administrative complexity of associating users and privileges. This dissertation introduces extensions to the access-control logic that can be used to assure the correctness of RBAC access-control decisions. By implementing and extending the access-control logic in a computer-assisted reasoning tool such as the Higher Order Logic (HOL) theorem prover [GM93], the access-control logic and its extensions are proved to be sound. The result is a tool for design and verification engineers to reason about access-control policies including RBAC.In this dissertation, we explain how to use the logic to describe RBAC components, such as user assignments, permission assignments, role inheritance, role activations, and users' requests. We also describe in detail the steps of implementing the access-control logic and its extensions in the HOL theorem prover. Administrative RBAC systems are also explored to see how the HOL theorem prover can be used to formally verify their properties and policies.
机译：兰普森（Lampson），阿巴迪（Abadi）及其同事[LABW92，ABLP93]的访问控制逻辑使得通过正确考虑身份，凭据，权限，委托和特权来确保访问控制决策的正确性成为可能。它可以用来描述各种访问控制策略并推断其访问控制决策。但是，它缺乏推理基于角色的访问控制（RBAC）[FSG + 01，FBK99，FKC03，SCFY96]的能力，这是一种用于降低与用户和特权相关联的管理复杂性的流行技术。本文引入了对访问控制逻辑的扩展，可以用来确保RBAC访问控制决策的正确性。通过在诸如高阶逻辑（HOL）定理证明器[GM93]之类的计算机辅助推理工具中实现和扩展访问控制逻辑，可以证明访问控制逻辑及其扩展是可靠的。结果为设计和验证工程师提供了一种工具，用于推理包括RBAC在内的访问控制策略。在本文中，我们将说明如何使用逻辑来描述RBAC组件，例如用户分配，权限分配，角色继承，角色激活，和用户的请求。我们还将详细描述在HOL定理证明器中实现访问控制逻辑及其扩展的步骤。还探索了行政RBAC系统，以了解如何使用HOL定理证明者来正式验证其属性和策略。

著录项

  • 作者

    Kosiyatrakul, Thumrongsak.;

  • 作者单位

    Syracuse University.;

  • 授予单位 Syracuse University.;
  • 学科 Engineering Computer.Computer Science.
  • 学位 Ph.D.
  • 年度 2010
  • 页码 463 p.
  • 总页数 463
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号