基于重写的访问控制策略

理论计算机科学电子笔记171（2007）59-72www.elsevier.com/locate/entcs基于重写的访问控制策略Anderson Santana de Oliveira1，2INRIA LORIA615，RueduJardinBotaniquee，54600Villers-l`es-Nanncy，Frannce摘要在本文中，我们提出了一个形式化的访问控制策略的基础上重写。策略所针对的系统的状态被表示为代数项，这允许我们对策略环境的几个方面进行策略由重写规则集实现，重写规则的评估产生授权决策。我们讨论了术语重写系统的属性之间的关系，如连续性和终止性，以及它们对定义可信访问控制策略的影响保留字： 访问控制策略，术语重写系统1介绍术语重写[1]是一种用于指定和原型化系统的良好范例。它已被证明在定理证明，程序转换和代数规范中很有用。在许多实际情况下，其简单的形式背景允许快速原型化和验证各种系统。在计算机安全领域，术语重写已经成功地应用于帮助推理它的某些方面，特别是在安全协议的验证中[17，7]。然而，项重写在安全策略中的应用并不多：据我们所知，很少有方法试图将重写的使用引入这个领域[2，12]。建议读者参阅第7节中有关相关工作的更广泛讨论。访问控制关注的是声明允许主体（或主体）执行的操作，以便操作给定系统的对象（或资源）。描述这种保护的最广泛的框架是访问控制矩阵，这是几个操作系统设计中采用的模型1santana@loria.fr2由CAPESBEX.2120.03-8支持。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.05560A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）59矩阵的行包含主体（系统的活动实体，如进程和用户），列列出系统的受保护实体（相关对象，如文件），单元格包含访问权限（读，写，执行等）。）被分配给关于受保护资源的每个活动实体。只有在相应的单元格中存在该动作的条目访问控制的一些基本模型依赖于访问控制矩阵的修改变体。例如，军事安全政策[4]为主体和客体增加然后，固定的安全策略声明主体不能写入具有较低安全级别的对象，并且它不能从具有较高安全级别的对象读取-没有读，没有写。尽管访问控制矩阵支持访问控制策略的许多形式化，但它不适合捕获更动态的策略，例如依赖于时间、位置和策略环境的许多其他可能属性的策略。提出了一种基于术语重写的访问控制策略的形式化描述. 策略被表示为重写规则的集合，其评估产生授权决策，而策略被强制执行的请求和环境被表示为代数项。由于我们将政策环境视为术语形式下的这项工作的主要目标是提供一个正式的语义表达的访问控制策略语言，这是能够支持动态的政策，提供一个设计，在那里有可能有maintenance执法机制，并表征可信的政策相关联的属性相应的长期重写系统，实现安全策略。例如，当肯定授权和否定授权都可能时，不存在冲突是一个重要的属性。它确保对于某个访问请求，不会同时分配授权和拒绝。这种形式化的另一个目标是能够促进策略执行。我们在此提出的架构将政策和执行机制明确分离。由于策略是重写规则，因此标准重写引擎可以完成将策略应用于请求并评估结果的工作。本文的结构如下：第2节回顾了一些有用的定义项重写系统，第3节通过一个例子来说明我们想要表达的访问控制策略，第4节介绍了策略环境的元素，第5节介绍并讨论了基于重写的策略，第6节描述了什么样的安全机制是必要的，以执行这些策略，第7节讨论了相关的工作，第8节总结并指出了一些未来的发展。A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）5961−→R2术语重写系统我们回顾一下签名和术语的一些基本定义。 签名S ={S，F}是一组排序S，以及一组函数符号，每个符号通过arity函数（ar：F→N）与一个自然数相关联，表示参数的数量。Fn是元数为n的函数符号的子集，Fn={f∈F| ar（f）= n}。T（x，X）是由给定的函数符号的有限集合F和变量的可数集合X构建的项的集合。 变量的集合发生在项t由Var（t）表示。 如果Var（t）为空，则t称为基项，T（t）是所有基项的集合。 一个置换σ是从X到T（x）的赋值，当它的定义域是有限的时，记为σ={x1<$→t1，.，xk<$→tk}。将替换σ应用于项t∈T（X，X）的结果记为σ（t）。重写规则是表示为l → r的有序项对，其中l，r∈T（n，X），l∈/X，且ndVa r（r）<$Va r（l）。这条规则的左侧和右侧是完全相同的。重写系统或术语重写系统这是一个（有限的或无限的）重写规则集。给定重写系统R，项t重写为项tJ，其表示为t→Rtj如果存在R的规则t→l，t中的位置ω，置换σ，满足t|ω = σ（l），使得tJ= t [σ（r）]。A subterm t|可以应用重写步骤的ω称为redex。一个没有redex的项被称为R不可约或R-正规形式。重写推导是重写步骤t1→Rt2→R.的任何序列。如果存在从t到tJ的重写推导，则重写推导出一个BILITY关系N − → BILITR定义为T RMS：T − → BILITR T J。如果推导至少包含一个步骤，则为+dentedy. 如果所有的重新写入都是重新写入，∗ ∗是有限的。它是连续的，如果对于所有项t，u，v，t−→Ru和t−→Rs，u−→Rs和d v−→Rs，对于某些类型。3激励的例子下面的例子稍微改编自XACML规范[20]，这是Oasis Consortium3的一项倡议，旨在为基于角色的访问控制创建标准标记语言。让我们假设一家医疗公司采取以下政策：(i) 一个人，由他或她的病人号码识别，可以阅读任何记录，他或她是指定的病人。(ii) 一个人可以阅读任何记录，他或她是指定的父母或监护人，而病人是16岁以下。(iii) 医生可以写信给他或她是指定的初级保健医生的任何医疗单位。(iv) 不允许管理员读取或写入患者记录的医疗元素。3http://www.oasis-open.org/62A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）59SIp a t i e n t（+recor d（p a t i e n t（guar di an（抗生物素，payment（ v is a）+phys i ci an（请求req（ phys i ci an（r ecor d（ p a t i e n t（guar di an（antibiotic，payment（ v is a））Si+1p a t i e n t（+r e c o r d（p a t i e n t（guar di an（a n t i b i o t i c and a spirin，payment（ v isa））+phys i ci an（图1.请求写入医疗元素后的系统状态转换这些规则说明了授权对客体和主体属性的依赖性。这反映了现代应用程序在访问控制声明中的可扩展性方面的当前需求，是我们感兴趣的那种策略的代表。高度抽象的访问控制策略声明背后的想法是，策略规范和执行可以与应用程序的其他功能分离，从而避免错误并提高可维护性。在图1中示出了上述医疗系统的可能执行。在给定的时间点，系统处于状态si，其中对象和资源的属性值出现在表的第一行。“+”运算符连接术语，在第5节中有更好的表格的第二行示出了这样的事实，即某个患者记录的主治医师需要为该患者开出新的医疗元素。根据我们刚刚描述的策略，必须为该请求分配授权访问，因此系统状态更改为状态si+1（表的最后一行），包含医疗记录的更新条目。我们对应用程序做了一些假设：应用程序的当前状态以术语的形式表示总是可用的，用户请求也是如此。在实践中，这将需要修改程序以捕获其状态，并在每次访问资源时A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）5963fmod医疗系统签名 是保护STRING.保护Nat.4政策环境关于访问控制，人们感兴趣的是说明允许执行哪些操作，主体（或主体），以操纵给定系统的对象（或资源）。为此，最广泛的表示模式是访问控制矩阵，其中行列出主题，列包含对象，单元格保存有关主动实体相对于被动实体的特权（读取，权限，执行这个模式足以满足强制和自主访问控制模型的大多数需求，但不足以表达高度抽象的策略，如第3节中的运行示例。为了声明这种策略，有必要编写关于主题和资源属性的当前值的句子，而不仅仅是它们的身份。我们称策略环境为与访问控制相关的所有元素的配置。我们称目标系统T为任何必须遵守给定安全策略的任意应用程序。目标由一组状态和状态转换表示，这些状态和状态转换由访问请求触发。对于T的每个状态si，我们关联一个代数项，该代数项包含在si中为真的事实。请求也被表示为术语（参见图1）。我们在这里捍卫的想法，最近也在一些论文中公开[3，21]，是访问控制是应用程序的一个方面，可以独立地指定，实现和维护。此外，应用某个策略的机制应该是应用程序的外部实体。图2显示了策略实施的概览图。状态si中的应用上下文与当前请求req（s，a，o）一起被传递到引用监视器。引用监视器根据当前策略评估每个请求。如果策略授予请求访问权限，则应用程序继续。否则，中止应用的执行4。我们将目标系统T的签名表示为RNT，它提供了构建系统状态表示所需的构造器康-因此，在T的执行的每个阶段的事实的数据库是来自T的设定基础项（T）。在运行的例子中，我们使用顺序排序的规范来形式化问题和Maude[9]的系统。例4.1我们将下面的签名用于第3节中描述的医疗应用，其中患者由一个包含姓名、号码、年龄和监护人的术语表示。 关键字ctor表示它后面的运算符是构造函数。4可以使用例外处理否定授权，但本文不探讨这个问题64A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）59排序患者t 物理学家 记录 管理员监护人医疗元素其他元素。op帕蒂恩：圣陵Nat Nat监护人->病人t[ctor].opad m i n i s trator：Nat −>管理员[ctor].op卫报：S TR I N G −>卫报[ctor].opphy si c i a n：S TR I N GNat −>医师[ctor].opr ecor d：Patien t Physician Medical Elements Patien tPhysician Medical Elements −>Record [ctor].endfmfmodMEDICAL−SYSTEM−TERM−SIGNATURE是包括医疗系统签名。包括政策签名。子分类subsortsubsortsubsortsubsort医师<主题病人不是<受试者..管理员<主题.记录 <对象.医疗元素<对象.简体中文<对象.op读记录：−>行动。上下文SIreq（s，a，o）参考监测策略规则许可证Si+1图2.一般表示模式为了更好地表达策略，有必要指出哪些类别是T中的主体、动作和客体的子类别，并介绍T中可用的动作。例4.2下面的模块说明了我们如何通过使用子分类来确定第3节中介绍的医疗系统中的主体、对象和动作为简单起见，操作被表示为常量A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）5965op欧欧写入记录：−>行动.readMedElements：−>Action。writeMed 要素：−>行动。改为“要素：->行动”。写其他元件： −>行动.endfm排序和子排序允许我们在目标应用程序当前状态的基础项（通过“+”运算符）的连接中出现的子项中区分主语和宾语。术语的顺序排序性质避免了几个常见的错误，因为类型检查是在规范上执行的5基于重写的策略在本节中，我们将讨论通过术语重写系统指定访问控制策略的问题我们提出了一个初始定义的安全策略，其特征策略的语法。这一定义包括潜在的“不安全”政策。在讨论了访问控制策略的期望属性之后，我们提出了“安全”策略的定义安全策略是关于什么是允许的，什么是不允许的声明[5]。在处理访问控制时，（正式的）策略规范语言将有助于明确定义规则，这些规则将管理允许主体在一组资源上执行的操作。为了处理动态策略，策略规范语言必须提供将有关策略环境的高级语句编码为从访问请求到授权决策的函数在下面，我们提出了基于重写的访问控制策略的签名。它清楚地建立了重写系统需要定义的函数，以便计算授权。根据下面的构造器符号，请求被表示为包含3元组的基础术语：主体，动作和对象：req：Subject×Actionn×Object→Request在不同构造函数的帮助下，可以在相同的策略规范中使用肯定授权和否定授权。permit和deny的签名包含subject、action和object，这对每个请求评估生成的权限（或拒绝）提供了更多的控制这些构造函数的配置文件如下所示：{deney，permit}：Subjet×Actionn×Objet→Authorization策略设计器的目标是提供一组规则，引用监视器将使用这些规则来评估每个传入请求。最终的决策并不完全取决于请求，还取决于目标66A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）59fmod策略-签名是sortObject . 排序主题。排序操作。排序Term .sortRequest.排序认证.子排序op欧欧endfm请求 ：允许主题客体动作主体请求[ctor] .：主题行动对象−>认证[ctor] .否认：主题行动对象 −>认证[ctor]. auth：请求期限->Auth或ization。+： Term 期限−>期限 [阿斯伯格]。在提出申请时。在本文中介绍的形式主义中，策略包含一组定义auth操作符的重写规则，其签名是auth：请求×验证→授权auth函数返回一个从nor派生的决策项（允许或拒绝根据请求项和T_parameter参数中包含的信息（对应于事实数据库）发布的malization过程通过使用结合和交换运算符“+"，可以在基项的合取中聚合T对象。这简化了必须应用某个访问控制规则的条件的表达。下面的代码演示了完整的策略签名CNORP定义5.1[基于重写的访问控制策略]基于重写的访问控制安全策略P是T（X，X）上的项重写系统，其中X = XTXXX，其中每个规则左侧的顶部符号是auth函数。该定义指出，如果重写规则的给定集合转换以auth符号为根的术语，则它们是访问控制策略，这对应于给定环境中访问请求的评估语法限制有助于关注在给定上下文中定义应授予的权限的实际问题。虽然这个定义看起来很有限制性，但在实践中，基于重写的策略可以与一组辅助的重写规则一起工作，以帮助定义身份验证功能。以下示例说明如何声明策略。A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）5967例5.2下面的重写规则集将第3节中的自然语言规则转换为我们的形式。重写规则的出现顺序与普通英语语句的出现顺序相同。mod策略1是保护医疗系统术语签名。无功功率：病人t .变pH值：Phys i c ian.varG：Guardian.varADM：管理员 .varss1S2：S TR I N G.无功功率： Term.varN1N2：Nat.var我：医疗元素 .varOE：其他元件.RL[ patReadRecord ]：（req（p，readRecord，record（p，ph，me，oe）），p + r ecor d（p，ph，me，oe）+ t）=>permit（p，readRecord，记录（p，pH值，我，oe））。RL[ guardRead Record ]：（ req（g，readRecord，记录（患者（s1，n1，n2，g），ph，me，oe）），患者（s1，n1，n2，g）+接收器d（p）t（s1， n1， N2， g）， pH值， me，oe）+t）=> permit（g，readRecord，记录（患者（S1，n1，N2，g），pH值，我，oe））。RL[ physWriteMedElem ]：auth（req（ph，writeMedElements，记录（p，ph，me，Oe）），Recor D（P，pH， me，oe）+t）=> permit（ph，writeMedElements，记录（p，pH值，我，oe））。RL[ admReadMedElem ] ：（ req（adm，readMedElements，record（p，ph，me，oe）），adm + recor d（p，ph，me，oe）+ t）=> deny（adm，readMedElements，记录（p，pH值，我，oe））。RL[ admWriteMedElem ] ：auth（req（adm，writeMedElements，record（p，ph，me，oe）），adm + recor d（p，ph，me，oe）+t）=> deny（adm，编写MedElements，记录（p，pH值，我，oe））。68A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）59恩德姆有几个问题可能会使策略实施复杂化。例如，术语重写系统实现策略可以是非终止的。当目标系统对引用发出某些访问请求时，A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）5969监视器，它将无法在有限的时间内计算授权。我们建议应遵循政策规范的细化纪律，以便在执行某些政策之前执行检查许多重要属性的验证步骤在下一节中，我们将讨论基于重写的策略所需的属性。5.1安全策略的属性终止第一个有趣的属性是终止。这确保了每个请求评估都是有限的，从而避免了目标应用程序执行被不确定地阻塞。术语重写系统的终止已经被广泛研究，并且有许多可用的工具可以检查术语重写系统的终止，例如CiMe，Crimp，Cariboo，仅举几例。读者必须意识到，策略组合可能会导致问题，因为终止不是模块化属性[24]。这意味着两个终止项重写系统的规则集的并集可能不会产生终止项重写系统。大多数关于项重写系统并的正结果都假设组合系统的签名是不相交的。关于项重写系统的各种属性的模块性的调查可以在[15]中找到一致性积极和消极授权的组合使用带来两个主要问题：不完整性，当没有为某个请求指定授权时，以及不一致性，当对于访问请求存在否定授权和肯定授权时。政策规范的经典方法采用封闭政策或开放政策假设，这意味着只需要分别指定积极或消极授权。这在实践中显示出限制性。目前的趋势是允许用户区分什么是允许的，什么是不允许的[10]。处理这个问题的另一种方法是采用冲突解决策略，为冲突案件分配优先级。例如 ， 可 以 说 deny 覆 盖 了 为 某 个 请 求 计 算 的 任 何 其 他 授 权 。 相 应 地 ， permitoverridescombinator总是在冲突决策的情况下允许访问。这种消歧在许多策略规范语言中可用，包括XACML [20]。在基于重写的策略的情况下，如果相应的重写系统具有并发属性，则可以避免并发这将确保从给定的请求和应用程序当前状态派生出单个与终止相比，并发对于两个并发项重写系统的合并具有更好的行为。众所周知，连续性是具有不相交签名的重写系统的模块化属性[25]。5在终止竞争主页上查看参考文献和结果http://www.lri.fr/终止竞争/70A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）59完整性完整性意味着每个请求对应一个授权决策。确保完整性的常用方法是假设开放或关闭策略作为默认策略运行。在项重写中，如果所有的基项都可以被简化为只包含构造子的范式，则系统被称为充分完备的[6，13]。在基于重写的访问控制策略的情况下，这包括检查auth函数是否完全定义在策略环境的条款上，以及其范式是否是允许或拒绝构造函数。或者，用户可以利用“Meta”规则来确定默认的决定，在没有赎回的情况下，为一个给定的请求和环境。这些规则的形式auth（req（s1，a1，o1），t）→deny（s1，a1，o1）或auth（req（s1，a1，o1），t）→permit（s1，a1，o1）分别为封闭式或开放式政策。这些规则必须在Meta级别使用，也就是说，标准重写机制必须考虑到这样一个事实，即当没有其他规则适用时，必须选择这些规则鉴于对访问控制安全策略的期望属性的讨论，我们准备引入以下定义：定义5.3[可信安全策略]可信访问控制安全策略是一个终止和连续项重写系统P，它在签名上完全定义了认证功能。信任这个词的选择是为了表达系统管理员可以对基于重写的策略有更多的信心，该策略具有终止，一致性和充分完整性的属性。这确保了策略明确地声明授权。6安全机制在本节中，我们将讨论安全机制如何实现基于重写的策略，以及系统如何被认为是安全的。安全机制确保目标系统T在其整个执行期间确实遵守所实施的策略。状态转换T，si <$→si+1，对应于来自主体的对资源执行动作的访问请求安全机制必须在T的条款和当前请求auth（req（s，a，o），t）上应用由策略P在它评估为permit（s，a，o）的情况下，T的计算可以继续，如果它评估为deny（s，a，o），则强制机制必须中止T的执行。这是执行监控安全机制的特征[23]。如果目标执行的给定状态ti中A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）5971被外部恶意实体修改，并且这种状态是通过一系列积极授权达到的。定义6.1[安全系统]目标系统T被称为安全的w.r.t. - 策略P，如果它从有效状态t0开始，并且对于每个过渡状态ti<$→ti+1，产生新的有效状态。这个定义接近于经典的基于自动机的安全系统方法，来自Goguen和Meseguer[14]，以及最近的Scheneider [23]，其中断言是关于目标系统的可能执行路径的。这种方法的另一个优点是可以重用安全机制来实现不同策略集的访问控制，因为策略和机制之间的分离是明确的。7相关工作与本文描述的工作更密切相关的是最近的倡议，将术语重写引入到安全策略的规范中在[12]中，术语重写用于控制数据的机密级别，通过描述降级函数，在并发编程环境中，其形式模型基于进程演算的变体。在[2]中，作者将访问控制列表和基于角色的访问控制（RBAC）建模为术语重写系统。它们表征了策略的一致性、整体性和完整性，而重写系统的属性定义了它们，因此共享了本文的一些目标。然而，我们专注于动态方面的政策环境，以指定授权，以及如何访问控制规则可以集成在程序开发。在一般情况下，我们在这里提出的访问控制列表和RBAC的方法相比，主要的优点是，它是可能的，以一种灵活的方式来表达更多的政策环境的约束。大多数基于规则来指定安全策略的形式化方法依赖于某种“逻辑语言”的方言我们提到[16，11，18]，引用几个。重写有一个相关的逻辑[9]和微积分[8]，这使得它成为一个适当的框架，为各种系统建模。重写使用模式匹配作为其核心机制的事实使得许多重要的理论结果，是有用的安全策略分析，以及。例如，考虑策略组合下的一致性问题。我们知道，在基于逻辑的访问控制策略的情况下，这个属性可以通过限制规则的形式来保持，如[16]中所讨论的。另一方面，基于重写的方法可以从现有的结果中获益，这些结果涉及到连续属性的模块性在同样的观点下，一些必要的条件下，项重写系统的终止被保存，是已知的[22，19]。这使得重写成为一种以声明方式定义策略的有趣方法关于执行机制，这里提出的工作遵循程序监控的路线，并认为实现应用程序的代码72A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）59不信任。作为一个例子，我们提到Polymer系统[3]，它对Java程序实施访问控制基于重写的策略可以作为任何目标应用程序的程序监视器这可以通过将策略签名与目标程序的签名相关联来实现，以便拦截其敏感函数调用。允许这种操作的一种技术是程序转换，其目的是生成新代码，保留程序语义，这是广泛采用术语重写的领域8结论和今后的工作我们讨论了在本文中的形式化访问控制策略使用长期重写。由此产生的语言，使我们能够表达访问控制规则，捕捉动态条件的政策环境，提供了一个灵活的方式来编码授权。根据这个建议编写的访问控制重写规范可以用于快速原型化策略，因为有几个有效的术语重写系统实现可用。访问控制策略的一些关键属性的推理也成为可能，这要归功于我们在策略属性（如一致性）和术语重写系统之间建立的对应关系。作为未来的工作，我们将研究如何重写策略可以是有用的在政策制定和冲突解决方面。为了验证这个模型，还将构建一个用于强制执行基于重写的策略的实现，方法是使用监视器内联方法，如前一节所讨论的9致谢我想让我和我的同事们一起阅读这篇论文的前几个版本，并让我和贾德森·圣地亚哥和霍拉蒂乌·奇尔斯泰亚一起阅读这篇论文的前几我谨此感谢各位裁判提出的宝贵意见及建议。引用[1] Baader，F.和T. Nipkow，[2] Barker，S. 和M. Fernáandez，Termrewritingforaccesscontrol. ，n：E. DamianianddP. 刘先生，教育部，DBSec，Lecture Notes in Computer Science 4127（2006），pp. 179-193页。[3] 鲍尔湖J. Ligatti和D.沃克，用聚合物组成安全策略。，in：V.Sarkar和M.W. Hall，editors，PLDI（2005），pp. 305-314[4] Bell，E.D. 和L.J. 李文生，计算机系统安全，国立成功大学计算机科学研究所硕士论文，国立成功大学计算机科学研究所硕士论文，民国80年。[5] Bishop，M.，[6] Bouhoula，A.和F. Jacquemard，条件约束项重写系统的充分完备性自动验证，技术报告RR-5863，INRIA（2006）。URLhttp://hal.inria.fr/inria-00070163/en/A.S. de Oliveira/Electronic Notes in Theoretical Computer Science 171（2007）5973[7] Cirstea，H.，使用重写和策略的身份验证协议。，in：I. V. Ramakrishnan，editor，PADL，LectureNotes in Computer Science 1990（2001）. 138-152[8] Cirstea，H.和C. Kirchner，重写演算-第一部分和第二部分，纯粹和应用逻辑兴趣小组的逻辑杂志9（2001），pp。427-498.[9] Cl avel，M.， F. 杜兰，S。 Eker，P. Lincoln，N. 我的天啊，J。 M egueranddJ. F. Ques ada，Maude：Specification and Programming in Rewriting Logic. ，Theor。Comput. Sci. 285（2002），pp.187-243[10] di Vimercati，S. D. C.的方法，P. Samarati和S. Jajodia，访问控制的策略，模型和语言。，in：S.Bhalla，编辑，DNIS，计算机科学讲义3433（2005），pp. 225-237[11] Doughnut，D. J.，K. Fisler和S. Krishnamurthi，J.D.和关于动态访问控制策略的推理. ，in：U. Furbach和N. Shankar，editors，IJCAR，Lecture Notes in Computer Science 4130（2006），pp. 632-646[12] 埃查赫德河和F. Prost，声明式的安全策略。Barahona和A. P. Festival，editors，PPDP（2005），pp.153-163.网址http://doi.acm.org/10.1145/1069774.1069789[13] 格内迪格岛和H. Kirchner，Computing constructor forms with non-terminating rewrite programs. ，在：A. Bossi和M. J. Maher，editors，PPDP（2006），pp. 121-132.[14] Goguen，J. A.和J.Meseguer，安全策略和安全模型。IEEE Symposium on Security and Privacy，1982，pp. 11-20[15] Gramlich，B.，不相交和构造子共享条件重写系统的终止性和连续性。，Theor。Comput. Sci. 165（1996），pp. 97比131[16] Halpern，J. Y.韦斯曼（V. Weissman），《运用一阶逻辑推理政策》（Using first-order logic to reasonabout policy）。，in：CSFW（2003），pp. 187-201.[17] Jacquemard，F.，M. Rusinowitch和L.维格纳隆，正在编译和验证安全协议. ，在：M. Parigot和A. Voronkov，editors，LPAR，Lecture Notes in Computer Science 1955（2000），pp. 131-160.[18] Jajodia，S.，P. Samarati，M. L. Sapino和V.S. Subrahmanian，灵活支持多种访问控制策略。，ACMTrans.Database Syst.26（2001），pp. 214-260[19] Middeldorp，A.，项重写系统直和终止的一个充分条件，在：LICS（1989），pp. 396-401[20] Moses，T.，可扩展访问控制标记语言（xacml）2.0版，技术报告，OASIS（2005）。[21] Pavlich-Mariscal，J. A.，L. Michel和S. A. Demurjian，使用面向方面编程的基于角色的访问控制的正式实施框架。，在：L. C. Briand和C. Williams，editors，MoDELS，Lecture Notes in Computer Science3713（2005），pp. 537-552[22] Rusinowitch，M.，项重写系统直和的终止性。，Inf. Process. Lett. 26（1987），pp.65比70[23] 施耐德，F. B、可强制执行的安全策略。、ACM传输信息系统安全3（2000），pp. 30-50.[24] 富山，Y.，项重写系统直和终止性的反例。，Inf.过程Lett. 25（1987），pp. 141-143[25] 富山，Y.，项重写系统直和的church-rosser性质。，J. ACM 34（1987），pp. 128-143