基于重写的访问控制策略分析

理论计算机科学电子笔记234（2009）55-75www.elsevier.com/locate/entcs基于重写的访问控制策略分析ClaudeKirchner，H'el`eneKirchnerINRIA波尔多-西南研究中心351，Coursdelalib'eration，33405Talence，法国Anderson Santana de Oliveira1Universidade Federal do Rio Grande doNorteDIMAp-CampusUniversita'rio-LagoaNova59072-970，Natal-RN，巴西摘要基于重写的方法为安全策略提供了可执行的规范，这些规范可以独立设计、验证，然后使用模块化规则锚定在程序上。在本文中，我们描述了如何执行查询这些基于规则的政策，以增加政策的正确行为的政策作者的信任。我们提供的分析是建立在战略缩小过程中，它提供了必要的抽象，模拟执行的访问请求的策略和解决的机制，如果从安全管理员查询。我们通过对防火墙系统政策的分析来说明这种一般方法关键词：安全策略，术语重写系统，战略重写，战略缩小。1介绍安全策略定义了系统安全的含义。策略通过确定可接受的信息流或通过描述主体对系统内受保护资源所具有的特权来建立对如何访问数据的约束。由于策略反映了某些组织或一般而言某些实体的安全需求，因此随着新威胁的出现或所讨论的系统体系结构的发展，它们会经常发生变化。计算机安全领域当前的挑战之一是对丰富的、表达性强的策略进行建模，这些策略通常以一组规则的形式给出，使得它们的属性可以1由CNPq 152373/2007-1支持。1571-0661/© 2009 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2009.02.07256C. Kirchner等人/理论计算机科学电子笔记234（2009）55正式陈述和证明。例如，策略应该是明确的，这意味着访问不能同时被授予和拒绝。 策略还应该涵盖系统可能遇到的所有相关情况：在处理访问控制时，这意味着回答所有可能的访问请求。在[14，10]中，我们提出了一个基于术语重写的正式策略模型，它提供了几个优点：首先，该语言允许我们处理广泛的安全策略，因为我们可以很容易地描述访问请求的形式和可能的授权决策集，而不会将它们限制为简单的允许或拒绝。 此外，可以以精确和表达的方式定义策略应用，因为可以确定控制规则应用的策略这种方法不仅提供了一个明确的语义访问控制策略，但也适当的技术来验证重要的属性，依赖于底层重写系统的一致性，终止性和充分的完整性。此外，基于重写的框架继承了所有这些属性的模块化结果，这比其他框架具有显著的优势，因为人们可以推断策略组合对组件策略的属性的影响。除了证明这些属性之外，策略设计者还需要了解访问决策是如何生成的。他可能想知道策略如何处理特定类型的请求，特别是那些涉及系统中最敏感信息的请求。在文献中，这通常被称为是否会允许进入？” 回答这些问题会增加 在特定的规范中的策略设计者在本文中，我们建立在我们以前的工作，以提供这种分析基于重写的策略。分析背后的主要机制是缩小，它提供了必要的抽象，模拟重写的策略请求的执行和解决机制的查询。我们扩展的政策语言与涉及变量的请求，我们展示了如何缩小可以用来找到哪些值可以实例化这些变量，以满足给定的请求，从而提供了一个足够的机制来解决这些查询。由于重写的表达能力和计算能力，基于重写的安全策略的框架足够通用，可以应用于各种 安全问题。防火墙政策提供了一个说明性的例子。防火墙是放置在本地网络入口点的安全组件，用于控制其与互联网的交互。其主要目的是检查来自和进入本地网络的数据包传输，并决定是否应该传输或拒绝给定的数据包。真正的防火墙实现通常以规则序列（即全序集）的形式给出，它可以进行递归调用，并且可能有默认规则。例如NetFilter就是这种情况，它是Linux发行版的几个变体中使用的防火墙系统。 重要的是要注意 这样的规则表示被用作规则执行序列的描述。这实际上是由这些系统实现的隐式规则执行策略，而明确表达这种策略的能力是使C. Kirchner等人/理论计算机科学电子笔记234（2009）5557XF≤不 FXV V∈ T F X→策略语义清晰、可维护且可证明。在当前的系统中，安全管理员经常面临避免不一致、冗余或不完整的规则集的问题，例如[24]中所描述的在这里，我们展示了解决查询如何有助于识别这种极其重要的策略的情况，因为它们是保护网络免受众多威胁的最新机制。但是该技术也适用于任何其他形式的基于可伸缩重写的策略。本文的结构如下。在第2节中，我们回顾并说明了基于重写的安全策略的定义。第三节相关定义 给出了重写、缩小和策略。它强调了战略改写的概念，这在考虑应用顺序和更普遍的控制的政策规则的背景下是最重要的。然后第4节展示了如何使用策略收缩来解决查询，并在一大类策略规范中找到相应的请求。它提供了假设分析的示例。为了支持读者的直觉，一个简单的防火墙例子是沿着文件开发的。第5节最后提出了进一步工作的一些看法2重写策略项重写的基本定义可以在[29，31，4]中找到下面将使用以下（，）是从给定的函数符号的有限集合及其profile声明和可枚举的变量集合构建的一阶项的集合。项中的位置被表示为整数序列并由ω表示，而空序列ω表示顶部位置。它们按字典前缀排序。符号t|ω用于表示t在位置ω处的子项。我们写t[s]ω（或者有时简称t[s]）来强调t在位置ω包含子项s。在项t中出现的变量的集合由Var（t）表示。如果Var（t）为空，则t称为基项，T（F）是基项的集合一个置换σ是从X到T（F， X）的一个赋值，具有一个有限域{x1，.，xk} 和 书面 σ = 联系我们 t1，...，xk<$→ tk}。述变量{x1，.，xn}称为它的定义域，记为D（σ）。集合i=1，.，nV ar（ti）记为I（σ）。我们写σ|V是σ对变量集V的限制，σ = σJ [V]表示<$x ∈ V，σ（x）= σJ（x）。重写规则是一个有序的项对l，r（ 一） 、），表示为lr，其中通常要求l不是变量，ar（r）ar（l）. 术语l和r分别称为规则的左手边和右手边。重写系统是一组（有限或无限）重写规则。规则可以被标记，以便轻松地谈论它们。在[14]中，我们介绍了访问控制策略的一般定义，它抽象了可能的请求和决策的集合，因此支持广泛的策略：定义2.1[安全策略[14]]访问控制安全策略是一个5元组（F，D，R，Q，F），其中：58C. Kirchner等人/理论计算机科学电子笔记234（2009）55TF不 FXTFTF(i) F是一个排序的签名;定义数据结构的词汇表。(ii) D是封闭项的非空集合：D（）;用于形式化策略所采取的决策集合。(iii) R是一组重写规则，用于提供策略的本地语义。(iv) Q是一组来自（）：Q（）;的术语，用于描述可接受请求的形式。(v) 策略是R的重写策略，用于指导规则应用，从而提供策略的全局语义。在该定义的注释中提到的局部和全局语义的概念被提供作为一种直观的方式来描述重写规则是描述局部变换的实体和策略的事实，策略是组合这些局部应用规则的方式。这将在下一节（第3节）中正式展开为了说明这个定义，让我们考虑以下简单的例子。示例2.2本示例摘自NetFilterhow-to2.假设一个互联网用户想设置防火墙来阻止任何来自外部的流量进入他的本地网络。由于与Internet连接相关联的接口通常是ppp 0，因此一个简单的方法是拒绝来自此源的所有新数据包为了证明这样一个事实，即它可能是方便的政策，以包含规则以外的直接计算决策，我们还给出了一些额外的规则，允许两个不同的本地计算机共享相同的外部IP地址：对于每个传出的数据包的起源是本地机器，其头部被重写为一个单一的地址。• 此策略的排序签名F为：pckt：地址×地址×州›→决定新建，已建立：›→状态放弃，接受：›→决定eth0，ppp0，10。1.一、1.一、一、10. 1 .一、1 .一、两千一百二十三。123. 1 .一、一曰：›→地址函数pckt计算在网络中传输的分组的决策。• 表示决策的常量符号的集合是D={accept，drop}。• 将R视为以下规则，其中src、dst：Address和s：State是2http://www.netfilter.orgC. Kirchner等人/理论计算机科学电子笔记234（2009）5559→ω→→变量：pckt（src，dst，estab）→接受pckt（eth0，dst，new）→接受pckt（ppp0，dst，new）→删除pckt（10. 1 .一、1 .一、1，ppp 0，s）→ pckt（123. 123. 1 .一、1，ppp 0，s）pckt（10. 1 .一、1 .一、2，ppp 0，s）→ pckt（123. 123. 1 .一、1，ppp 0，s）第一条规则是必须接受与已建立连接有关的数据包。第二条规则匹配任何来源于本地网络的数据包，这些数据包被接受。第三条规则拒绝来自外部网络（ppp0）的任何新数据包。最后两个规则匹配本地机器的IP地址，并将它们重写为从外部网络可见的单个IP地址• 集合Q包括在顶部位置具有符号pckt的所有基项• 这种防火墙策略的一个常见策略是按照给定的顺序应用规则。我们将在下一节中看到如何形式化这个策略上述要素定义了安全策略。值得注意的是递归规则的存在，这对策略定义很重要，但并不直接派生权限。[14，10，12]中给出了进一步的例子来说明这个定义。在这一框架内，政策评估相当于通过战略性地改写地面请求进行的评估。让我们在下一节介绍这个概念3战略改写和缩小[28]中定义并研究了策略重写和缩小;感兴趣的读者可以参考它以获得更多细节。给定重写系统R，T（F， X）中的项t重写为另一项tj，如果存在R的重写规则l→r，t中的位置ω和替换σ使得测试|ω=σl和TJ=t[σr] ω。 记为t →Rtj，其中ω，l → r，σω，l r，σ或者R可以省略。 不|ω称为redex。一个没有redex的术语被称为不可约R或在R-正规形式，或只是正规化。 回复由R诱导的重写关系的传递闭包记为R_R。术语重写系统R→生成抽象归约系统，即标记的有向图R =（O R，SR），其结点是项O R<$T（F，X），其有向边是重写步：SR={t → tJ|对于ω a在t中的位置，t →RtJ}。一个R-导子或R-归约序列是图R中的一条路π;当它是有限的时，π可以写成t0→φ0t1→φ1t2。 . →φn−1tn其中φi是标号，并且我们假设t0通过导数π = φ0φ1.约化为t n。φn− 1;也记为t0φ0φ1...φn−1tn或简称t0n是π的长度。 当一个derivation的长度为零时，它是空的，在这种情况下，它的源和目标是相同的。从t发出的空派生表示为idt。π的源是单例{t0}60C. Kirchner等人/理论计算机科学电子笔记234（2009）55R- -RRR∈R OS表示为dom（π）。π的目标是单例tn，当没有语法歧义时，它被表示为（π t0）或简称为πt0;注意，-推导是其归约步骤的串联。π1和π2的级联当它存在时，是一个新的R-导子。通常识别重写系统（即，一组重写规则）与其生成的抽象归约系统（即，R允许的所有导子的集合）。 重写系统直接对应于一个唯一的抽象归约系统，它可以被看作是描述所有派生集的通用方法。 反之不是真的，因为根据一组推导，生成重写系统通常不是唯一确定的。3.1战略重写定义3.1[抽象策略]对于给定的抽象归约系统：一个抽象的策略是的所有导子（有限或非有限）的集合的子集。在对象t上应用策略Et表示为Et。它表示所有对象的集合，这些对象可以通过在t中的推导从t到达：t = {tJ|<$π ∈ <$使得t → πtJ} = {πt|π ∈ π}。当在t中没有派生有源t时，我们说在t上的策略应用失败。在一组对象上应用策略t，就是对集合中的每个元素t应用策略t。结果是对象集合中所有t的t的union。策略的定义域是一组对象，这些对象是在dom（dom）=δdom（δ）中派生的源。包含所有空派生的策略为Id={idt|t ∈O}。现在可以给战略改写下一个定义定义3.2[策略重写[28]]设=（R，R）是重写系统R生成的抽象约简系统，并且是的策略。策略重写派生（或策略重写派生下的重写派生）是策略重写派生的一个元素。策略性重写步骤是重写步骤t →RtJ，它发生在推导过程中，记为t → RtJ。一个策略可以通过列举它的所有元素来描述，或者更合适地说，战略语言。人们采用了各种方法，产生了稍微不同的策略语言，如ELAN[30，8]，Eurgo[36]，Tom[6，5]3或最近的Maude[9]。所有这些语言都关注提供抽象的方法来表达对规则应用程序的控制，通过使用Maude的rexexivity和元级别，或者ELAN或Rexego的重写策略的概念。自下而上、自上而下或最左最内等策略是描述重写规则应如何应用的高阶特征。Tom、ELAN和Replego提供了灵活且富有表现力的策略语言，其中高级策略通过组合低级原语来定义。关于这些策略语言的更多细节，我们参考[28]3http://tom.loria.frC. Kirchner等人/理论计算机科学电子笔记234（2009）5561>>t tσrt→ωt→在我们要考虑的安全策略的上下文中，有几个策略是主要感兴趣的：策略universal（R）表示由一组重写规则R生成的所有派生，策略inner（R）表示R的规则仅应用于所有严格子项不可约的项的派生命令（r1，...，rk）表示其中规则r1，...，在所有严格子项都不可约的项上按此顺序尝试r k。最后一种策略对应于最内层优先级重写（简称IP重写），定义如下。当重写系统R是部分有序的，我们说r1比r2有更高的优先级，如果r1大于r2，记为r1r2。最内层优先级重写可以定义如下：定义3.3 [最内层优先级重写[21]]给定重写系统R，规则上具有偏序，T（F，X）中的项t IP-重写为tJ，如果存在R的重写规则l → r，t中的位置ω和替换σ使得t|ω=σl和J=[]，使得Rω，l→r，σtJ，没有真子项|ω是IP可约的，并且不|ω不能被任何比l → r优先级更高的规则约化。 这是写IPω，l→r，σ 其中ω，l → r，σ或R可以省略。 不|ω被称为IP Redex。没有IP-redex的术语称为IP-归一化的。有了这个定义，我们得到：命题3.4项t是IP归一化的，如果它是归一化的。如果t是正规化的，那么t确实是IP正规化的。 让我们用反证法来证明其逆命题。如果t不是正规形式，则存在最里面的位置和适用于该位置的非空规则集。 通过选择一个规则，它们之间的优先级越高，我们得到IP重写步骤，并且t不是IP归一化的。Q如果一个替换的图像中的所有项都是（基）IP归一化的，则称该替换为（基）IP归一化的。根据命题3.4，我们可以简单地考虑归一化替换。3.2的缩减处理在[26，16]中引入的缩小过程与重写非常相似，但在那里，匹配被统一所取代让我们回顾一下它通常的定义：定义3.5 [缩小]给定重写系统R，T（F，X）中的项t缩小为项tJ，如果存在R的重写规则l → r和t中的位置ω，并且使得t|ω和l可以用一个最一般的 单位元（简称mgu）σ进行单位化。然后tJ=σ（t[r]ω）。这表示为t~Rω，l→r，σ tJ或t~tJ，当我们不需要精确使用哪个重写规则以及在哪里使用。让我们记住，重写规则中的变量是隐含的普遍量化的，因此，重写规则中的变量集可以始终被假设为与窄项中的变量集不同（即，在上述定义中，Var（t）62C. Kirchner等人/理论计算机科学电子笔记234（2009）55V不|不O SNN电子邮件 F×T F Y→ω，l→r11α t→Rar（l）=）。让我们也注意到，缩小包含重写，因为变量不相交项之间的匹配也是一个统一器。现在基于缩窄过程，项重写系统R生成另一个抽象归约系统N=（OR，SR），其中OR= T（F， X），并且SR= {t~J~Rω，l→r对于ω a在t中的位置}。 对于重写关系，我们可以定义战略性缩小。定义3.6 [策略收缩[28]]给定重写系统R生成的抽象归约系统=（R，R），以及一个策略收缩派生（或策略收缩派生下的收缩派生）是一个策略收缩派生的元素。一个策略性的缩小步骤是缩小步骤t~RtJ，它发生在一个推导过程中，记为t~RtJ。3.3通过缩小我们现在感兴趣的是形式化地精确描述（策略性）重写和（策略性）缩小是如何相关的。它可以独立地表示为[22]和[15]中给出的抽象归约系统上定义3.7[模拟]设（O1， →1）和（O2， →2）是两个抽象约简系统。（O1，→1）Γ-模拟（O2， →2）对于关系Γ ∈O1 × O2，当对于具有源s2和目标sJ2的每个归约步骤s2→2sJ2，存在具有源t1和目标tJ1的相应归约步骤t1→1tJ1，使得t1Γs2和tJ1ΓsJ2。让我们定义关系r（）（、）as：tΓu如果t是u的基实例。 下面的引理需要这样一个事实，即抽象归约系统（T（F），→）模拟抽象归约系统（T（F， Y），~）。引理3.8对任意项t∈ T（F， Y）和重写系统R，如果t~ω，l→r，σtj，则σ（t）→ ω，l→ r，σTJ，对σ的任意基实例α，α（t）→ ω，l→ r，σα（TJ）.证明清 楚 ， 如 果 t~ω ， l→ r ， σtJ， 则 σ（ t） → ω ， l→ r ， σtJ。 因 为α是 σ的instance ， 所 以 α=μσ 。 则 α （ t ） =μ （ σ （ t ） ） ω ， l→rμ （ TJ ） . 但 tJ=σ（t[r]ω），所以μ（tJ）=μσ（t[r]ω）=α（tJ）。Q因此，抽象归约系统（T（F， Y），~）中的导子对应于抽象归约系统（T（F），→）中的导子集合命题3.9对任意项t∈ T（F， Y）和重写系统R，如果t~Rω1，l1→r1，σ1t1... ~Rωn，ln→rn，σntn，则恩... σ1（t）→Rωn，ln→rntn并且对于σ n的任何基实例α.σ1（t），（）Rω1，l1→r1Rωn，ln→rnα（tn）。给定一个终止重写系统R，让我们考虑N，T（F，X）中项的规范化基础实...→...→C. Kirchner等人/理论计算机科学电子笔记234（2009）5563例的子集关系式ΓN <$T（F， Y）× N为64C. Kirchner等人/理论计算机科学电子笔记234（2009）55N →不 FYω1，l1→定义为：urNt，如果t是u的归一化基实例。抽象归约系统（（，），~）ΓN-模拟抽象归约系统（，）这一事实建立起来稍微微妙一些，并且是由J.M.Hullot [26].引理3.10设t0是一项，ρ是一个归一化代换.若ρ（t0）→ R→TJ1，则存在替换σ和μ使得：ω，l r(i) t0~Rω，l→r，σt1，(ii) μ（t1）=tJ1，μ是归一化的，(iii) ρ = Var（t0）μσ（即ρ x ∈ Var（t0），ρ（x）= μσ（x））.这个结果很容易通过归纳步骤的数量扩展到任何重写推导：命题3.11设t0是一项，ρ是一个归一化代换，使得：ρ（t0）→R→r1Rωn，ln→rntJn.则存在置换σi（i = 1，.， n）和μ，使得：(i) t0~Rω1，l1→r1，σ1t1... ~Rωn，ln→rn，σntn，(ii) μ（tn）=tJn，μ被归一化，(iii) ρ= Var（t0）μσn.σ1（即ρx∈Var（t0），ρ（x）=μσn. σ1（x））。因此，当不考虑策略时，窄化推导ΓN-模拟重写推导在更一般的策略重写和缩小的情况下，模拟结果只针对特定的策略，如最内层或最外层重写[22]，我们在这里解决优先级重写[21]的问题。求解方程目标的缩窄过程的完备性在文献中已有大量的研究。结果总结见[1]。在保持完整性的同时确定变窄的问题研究得较少。 再次 在[1]中可以找到一种技术状态，以及几个类的定义在重写系统中，缩小具有有限的搜索空间，而不需要重写系统的连接。3.4基于IP窄化让我们在这一节集中讨论最内在的优先级重写和相应的 其思想是通过适当地设置约束c，CJ，通过约束收缩步骤（t，c）~IP（TJ，CJ）来捕获任何IP重写α（t）IPs。对于所有满足CJ（和c）的归一化基替换α，我们应该得到α（t）上的IP重写步和结果项α（TJ）。约束是一阶方程公式，平凡约束总是为真，记为id。现在让我们来分析这些约束的构造。为了使规则l→r在t中的某个位置ω上的应用成为可能，我们首先需要找到...→C. Kirchner等人/理论计算机科学电子笔记234（2009）5565→|c cVar tσD（σ）I（σ）|V ar（t）.ωJ≥ ωlJ→ rJinR V|ωJ/tω和l的mgu，比如说σ。然后，为了在位置ω处通过规则l r是IP可约的，基归一化实例α（t）必须满足以下条件：• α是σ的instance。 请注意，我们也可以考虑缩小替换 作为方程约束t的解形式，|ω =？l;在下文中，我们也用σ表示这个解出的形式。则α满足σi <$α是形式α=μσ[Var（t）<$Var（l）]的σ的一个实例• 在ω的位置ωJsun x处不可能有IP重写（记为ωJ≥ω）：<$ωJ ≥ ω，<$LJ → RJ ∈ R，<$γ，α（t）|ωJ/= γ（lJ）。由于α是归一化的，ωJ是t中的一个不变位置。换句话说，α必须满足约束c_inn，它是所有可能的质量约束ωJ和l_Jcinn=V ar（lJ），t|ωJ/= lJ。ωJ≥ω lJ →rJ ∈R• 没有更高优先级的规则适用于位置ω：<$LJ → RJ> l → r ∈ R，<$γ，α（t）|ωγ（lJ）。换句话说，α必须满足约束cprio，它是所有可能的不等约束lJc优先级=lJ→rJ>l →r∈RV ar（lJ），t|ωi = lJ。在这个涉及σ的缩窄过程中施加了一些重命名条件我：• 规则的变量与术语的变量保持不相交：Var（t）<$Var（σ（t））和Var（l）总是不相交的集合;• 由mguσ引入的变量，即I（σ），与D（σ）不相交。这个条件意味着单位元是幂等的（σσ=σ），所以σ（tJ）=σ（σ（t[r]ω））=tJ;我们将需要以下三个引理，借用或改编自[34]。引理3.12如果t是项，σ是替换项，则Var（σ（t））= Var（t）\D（σ）I（σ）|V ar（t）.这对native是有用的，在前面的假设下，约束inn和prio的自由变量属于（）。 作为引理3.12的结果，如果是在收缩步骤中使用的单位元，则σ（c_inn）=ar（l_J），σ（t）=l_J并且σ（c_prio）=l_J→ r_J> l → r ∈ R_r_ar（l_J），σ（t）|ωi = lJ在V ar（t）中具有自由变量\引理3.13假设我们有置换σ，θ，θJ和变量集合A，B使得（B\D（σ））<$I（σ）<$A。 如果θ = θJ [A]，则θσ = θJσ [B]。66C. Kirchner等人/理论计算机科学电子笔记234（2009）55→α t→ω，l→rω，l→r2005年5月t0，c ~0t1，c .. . ~1αt→0引理3.14设R是一个具有优先级的重写系统，并假设我们有替换σ，θ，θJ和变量集合A，B，使得• θ |A正常化• θJσ=θ[A]• B <$A\D（σ））<$I（σ）|A.那么θJ|B 也是正常的。IP窄化然后在约束项上定义，即项对（t，c）和一阶方程约束。定义3.15[受约束的IP缩窄]设t是一个项，c是一个约束。 定 义 了（t，c）上的约束IP缩窄步长，如果存在系统R的规则l r，t中的不变位置ω，约束t的替换σ解|ω=？l和一个约束cIP=cincprio，使得σccIP是可满足的。然后TJ = σ（t [r] ω）和CJ= σ（c）<$σ（cIP）。 这表示为（t，c）~IP（tJ，cJ）。从（IP收缩步骤）开始的IP收缩ω，l→r，σt0，c0）是一个约束考虑到约束条件的限制，我们得到以下结果。引理3.16对于任意项t∈ T（F， Y），用优先级重写系统R，如果（t，c）~IP （tJ，cJ）则对于σ的任何基归一化实例，α=μσ，的ω，l→r，σμ满意度cJ，（） IPω，l→rα（tJ）。证明让我们考虑s=α（t）项 其子项s|ω是l和ω的一个实例是t中的一个位置，因为α是归一化的。 因为α是σ的一个实例，所以σ（t）→RtJ，α（t）= μ（σ（t））→Rμ（tJ）= μ（σ（t [r] ω））= α（tJ）。此外，由于μ满足σ（cIP），α满足cIP，因此特别是对于α V ar（lJ），t|ωJlJ（对于所有不可变位置）ωJ≥ωint. So α（t）|ωJ不能是R中规则的左手边的instance，并且s 的任何真子项|ω是IP-不可约的。出于同样的原因，S|由于α是ar（LJ），t的解，所以ω不能用优先级比l → r高的规则lj → rj约化|ω=lJ。因此，从α（t）到α（tJ）的约简步骤是最内层的，优先级，并且s=α（t）是IP-可约为α（tJ）。Q因此，一个IP缩窄派生对应于抽象归约系统（T（F），→IP）中的一组派生命题3.17设R是一个有优先级的重写系统。 对于任意项t0∈ T（F，Y），以及任意约束c0，如果（） IPω1，l1→r1，σ1 （） IPωn，ln→rn，σn（tn，cn）则对于σ = σn. σ1，α = μσ，使得μ满足Cn，我们有（） IPω1，l1→r1IPωn，ln→rnα（tn）。...→C. Kirchner等人/理论计算机科学电子笔记234（2009）55671αt→0cαt→n1t0，id~t1，c .. . ~1αt→0\n∧∧V∧∧1V V V\ V2n通过归纳证明了IP-窄化推导的长度。引理3.16提供了n=1的情况。则 对于任何基归一化代换α=μσ，使得μ满足Cn= σ（c0）<$σ（cIP）<$σ（cIP）<$.. σ（cIP），α也 可以是写为α = μJσ1，其中μJ = μσn.σ2。 则μJ满足c1=σ1（c0）<$σ1（cIP），因此（） IPω1，l1→r1α（t1）。根据归纳假设，由于α（t1）= μσn，σ2（t1）和μ满意度，（）IPω2，l2→r2IPωn，ln→rnα（tn）。Q通过总是为真的平凡约束id实例化初始约束，我们得到以下推论。推论3.18设R是一个具有优先级的重写系统。对 任意项t0∈ T（F，Y），如果（） IPω1，l1→r1，σ1 （） IPωn，ln→rn，σn（tn，cn）则对于σ = σn. σ1，α = μσ，使得μ满足Cn，我们有（） IPω1，l1→r1IPωn，ln→rnα（tn）。相反，下面的提升引理受[21]和[23]的启发引理3.19（IP提升引理）设R是具有优先级的重写系统。 设s ∈ T（F，Y），α是一个代换，使得α（s）在s的一个不变位置ω是IP-可约的，且V一组变量，使得V ar（s）<$D（α）<$V。 如果α（s）→IP tJ，如果α满足约束c，则其自由变量包含在ω，l→rJ JV，则存在项sμ，σ，使得：∈ T（F， Y），一个约束c和标准化替换(i) （s，c）~IPω，l→r，σ(ii) μ（sJ）=tJ(iii) μσ=α[V](iv) μ satives c J.（sJ，cJ）证明我们总是可以假设V ar（l）和V是不相交的。 我们有α（s）|ω= β（1），对于某些β，D（β）≠ ar（1）。 由于ω是s中的不变位置，并且由于α和β的区域不相交，|ω和l可由α <$β = γ统一。 设σ是这两项的幂等最一般的单位元 设SJ= σ（s [r] |ω）。因为σ是一个mgu，所以存在ρ使得ρσ=α<$β=γ。设VJ =（V\D（σ））<$I（σ）且μ = ρ|VJ.显然D（μ）<$VJ。另一方面，Var（sJ）= Var（σ（s[r]））ar（σ（s[l]））=ar（σ（s））=ar（s） D（σ） I（σ）|通过引理3.12，得到ar（sJ）VJ. 从而得到ar（sJ）D（μ）VJ. 由于μ=ρ[VJ]，μ（sJ）=ρ（sJ）=ρσ（s[r]）=ρσ（s）[ρσ（r）]=α（s）[β（r）]=tJ.让我们证明μσ=α[V]。 由于μ=ρ[VJ]和VJ=（VD（σ））I（σ），我们通过引理3.13得到μσ = ρσ[V]，因此μσ = α[V]。让我们证明μ满足约束cJ=σ（c）σ（cinn）σ（cprio）。由于c，cinn，cprio的自由变量在V中，所以σ（c）σ（cinn）σ（cprio）的自由变量包含在VJ中。 由...→...→68C. Kirchner等人/理论计算机科学电子笔记234（2009）55于μσ = α [V]，且α满足V上的c，则μ满足σ（c）。 由于α（s）→IPtJ，α满足c的优先级。由于μσ=α[V]，则μ满足σ（cinn）<$σ（cprio）。C. Kirchner等人/理论计算机科学电子笔记234（2009）5569ω1，l1ωn，l nnω2，l2ωn，l nn最后，由于（iii），如果α被归一化，μ也被3.14归一化。Q这个结果可以通过归纳重写导子的步骤数来扩展：命题3.20设t0是一项，ρ是一个正规化代换，V Y是一个使V ar（t0）<$D（ρ）<$V的一组变量。 如果ρ（t0）→ IP→tJ1... → IPtJn，如果ω1，l1r1ωn，ln→rnρ满足一个约束c0，其自由变量包含在V中，存在归一化替换σi（i=1，...，n），约束条件ci（i= 1，.，n）和基归一化置换μ，使得：(i) （t0，c0）~IPω1，l1→r1，σ1(ii) μ（tn）=tJn，(iii) ρ= μσn. σ1 [V]，(iv) μ satisfies c n.（t1，c1）...~IPωn，ln→rn，σn（tn，cn），证明证明是通过归纳的长度的推导。对于n=1，它来自引理3.19。让我们假设n-1的性质，并考虑ρ（t0）→IP→r1 tJ1... →IP→rtJn. 根据引理3.19，对于任意c0，V中的变量使得α满足c0，存在（t0，c0）~IP（t1，c1），Jω1，l1→r1，σ1β（t1）=t1，βσ1=ρ[V]且β满足c1。由于β是归一化的，满足c1，因为TJ1=β（t1）→IP→r2 tJ2. →IP→rtJn，通过归纳假设，存在归一化置换σi（i = 2，.，n），约束条件ci（i = 2，.，n）和基归一化置换μ，使得：(i) （t1，c1）~IPω2，l2→r2，σ2(ii) μ（tn）=tJn，(iii) β = μσn.σ2 [VJ]，(iv) μsatisfiescn.（t1，c2）. ~IPωn，ln→rn，σn（tn，cn），其中VJ包含Var（t1）<$D（ρ）。 由于βσ1=ρ [V]，β=μσn.σ2 [VJ]和V\D（σ1）<$I（σ1）<$VJ，根据引理3.13，我们得到ρ=βσ1=μσn.σ2σ1 [V]. Q通过总是为真的平凡约束id实例化初始约束，我们得到以下推论。推论3.21设t0是一项，ρ是一个正规化代换，V Y是一组变量使得V ar（t0）<$D（ρ）<$V。 如果ρ（t0）→ IP→tJ1... → IPtJn，有存在规范化替换（=1个ω1，l1r1（ωn，ln→ rn ） 和σi i，...，n）， 约束 cii = 1，.，n基归一化置换μ，使得：(i) （t0，id）~IPω1，l1→r1，σ1(ii) μ（tn）=tJn，(iii) ρ= μσn. σ1 [V]，(iv) μ satisfies c n.（t1，c1）...~IPωn，ln→rn，σn70C. Kirchner等人/理论计算机科学电子笔记234（2009）55（tn，cn），例3.22让我们假设以下规则的顺序如下（优先级C. Kirchner等人/理论计算机科学电子笔记234（2009）5571，2，σ∧∧，3，σ是较小的标签）：1. pckt（src，dst，estab）→接受2. pckt（eth0，dst，new）→接受3. pckt（ppp0，dst，new）→drop四、 pckt（10. 1 .一、1 .一、1，ppp 0，s）→ pckt（123. 123. 1 .一、1，ppp 0，s）五、 pckt（10. 1 .一、1 .一、2，ppp 0，s）→ pckt（123. 123. 1 .一、1，ppp 0，s）让我们将IP窄化应用于项t=pckt（x，y，new）和约束标识。由于new和estab是两个不同的常量，因此规则1不适用。置换σ=（x=eth 0 <$y=yJ<$dst=yJ）是一个具有规则2的mgu。这里cJ=lJ→rJ∈RVar（lJ），newf =lJsrc，dst，pckt（etho，yJ，new）/=pckt（src，dst，estab）这就等同于真。因此：t~IP接受。规则3也适用于替换σJ=（x=ppp 0y =yJJdst=yJJ）。这里的约束是cJ=lJ→rJ∈R Var（lJ），newf =lJz，pckt（ppp0，yJJ，new）pckt（eth0，z，new）zJ，zJJ，pckt（ppp0，yJJ，new）/=pckt（zJ，zJJ，estab）这又等同于真。因此，t~IPJ下降。使用规则缩小IP范围4 5是相似的。我们现在准备将这些结果应用于战略重写和缩小to rewriting重写based基础policies政策.4基于重写的策略的基于缩小的分析在我们的框架中，政策评估是通过战略重写地面请求。因此，为了安全策略的安全设计，已经确定了几个属性[14，11]。定义4.1[终止性、一致性、决策完整性] [11]安全策略f=（F，D，R，Q，f）是• 终止，如果对于每个q∈Q，源q在q中的所有导子都是有限的。• consistent如果对于每个查询q∈Q，应用于q的最多返回一个结果：如果n =1，则 n = 1，n = 1，则n = 1。72C. Kirchner等人/理论计算机科学电子笔记234（2009）55• 决策完全，如果<$q ∈Q，<$d ∈D，使得d∈<$ q。C. Kirchner等人/理论计算机科学电子笔记234（2009）5573为了处理政策分析，我们现在增加了表达查询的可能性定义4.2给定安全策略T=（F，D，R，Q，T），查询是T（F，Y）的一个项，其中Y是不同于X的一组查询变量。约束查询是一对T（F， Y）项和一阶方程约束。基于前面第3节的结果，我们现在可以通过解决查询来分析安全策略的行为。该方法依赖于为给定查询构造缩小树：所有可能的（策略性的）缩小步骤都应用于该项，并且递归地应用于结果项，从而产生可能无限树。一般直观的想法是，缩小树提供了一个很好的模拟重写派生树，对应于请求评估的政策。我们假设安全策略是终止的，以便考虑规范化的条款，替换和实例化。有相当强大的技术来检查终止，如递归路径排序[13]，语义标记[37]，依赖对[3]等。这些和其他技术已经由几个工具实现，这些工具允许验证大量重写系统的终止：例如AProVE [20]，TTT [25]和CiME [32]，仅举几例。所有这些验证方法和工具都是静态地检查终止，这对于指定灵活的策略非常有吸引力特别考虑最内层终止，具体方法已在[2，19，23]中给出。 技术也被研究用于终止最外层重写[23]，延迟重写[18]或优先级重写[35，21]的终止。此外，通常可以证明一般的终止（即对于普遍策略），这意味着在任何策略下都是终止的。例4.3例2.2中的策略不是决策完成的：请求pckt（123. 123. 1 .一、1，ppp 0，new）在该系统中是不可约的，因此不能被评估为判决。如果我们在系统中