没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记117(2005)183-207www.elsevier.com/locate/entcsMSR密码协议规范语言的依赖重写逻辑扩展表示Iliano Cervesato1ITT工业公司,美国弗吉尼亚州亚历山大市高级工程和科学Mark-Oliver Stehr2伊利诺伊大学厄巴纳-香槟分校,计算机科学系,厄巴纳,IL 61801,美国摘要本文提出了一个浅,因此有效地嵌入安全协议规范语言MSR到重写逻辑与依赖类型,一个例子的开放演算的建设,它集成了关键概念,从方程逻辑,重写逻辑和类型理论。MSR基于一种一阶多集重写的形式,扩展了存在名称生成和以子排序的依赖类型为中心的可扩展类型基础设施。这种编码旨在作为使用现有的一阶重写引擎(如Maude)实现MSR规范和分析环境的基础。保留字:MSR,协议规范,构造的开放演算,依赖类型,Maude。1介绍MSR起源于一种简单的面向逻辑的语言,旨在研究各种假设下协议分析的可判定性[8]。它演变成了一个精确、强大、灵活,但仍然相对简单的框架1电子邮件地址:iliano@itd.nrl.navy.mil2电子邮件地址:stehr@uiuc.edu1571-0661 © 2005由Elsevier B. V.出版,CC BY-NC-ND许可下开放获取。doi:10.1016/j.entcs.2004.06.023184I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183−→RWLDT−→本文)OCC). . . . . .. . . .a.[14个]. . .<.. . . ..图1. MSR嵌入重写逻辑对于复杂密码协议的规范,可能被构造为协调子协议的集合[3,5]。它使用一阶原子公式上的强类型多集重写规则来表达协议动作,并依赖于一种形式的存在量化来象征性地建模随机数和其他新数据的生成。依赖类型是一种有用的抽象机制,在其他语言中不可用。例如,公钥/私钥对它们的所有者的依赖性可以在类型级别自然地表达。最后,MSR支持一系列有用的静态检查,包括类型检查[4]和数据访问验证[6]。这项工作概述了编码的核心MSR到重写逻辑(RWL),更准确地说,到其扩展与依赖类型(RWLDT)。重写逻辑[11]利用了这样的观察:许多范式可以自然地通过条件重写模基础方程理论来捕获,多集理论是并发系统和协议的规范化的一个特别重要的案例。最近,在[14]中研究了等式逻辑和具有依赖类型的重写逻辑的组合,其名称为构造的开放演算(OCC)。在本文中,我们证明了OCC的一个受限制的谓词实例,我们称之为依赖类型重写逻辑(RWLDT),可以用来以一种保留所有类型信息的方式表示类型化MSR规范。RWLDT本身并不支持存在名称生成的表达式:我们的编码用计数器实现了它。此外,确保结果代码的可执行性需要一些注意。将从MSR到RWLDT的映射与从RWLDT到RWL的映射组合在一起,这已经作为OCC原型的一部分实现[14],我们获得了从MSR到RWL的编码,这可以作为基于RWL的语言(如Maude [9])中MSR执行环境的基础。图1中总结了这种两级方法,它比直接映射到RWL有一些优势。第一个是模块化和关注点分离:从MSR到RWLDT的映射仅RWL(莫德)MSR..I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183185我与动态(由规则给出)有关,但保留静态部分(由声明、类型和术语给出)。第二个优点是RWLDT似乎是用户交互的正确级别,因为术语和类型与MSR的术语和类型密切对应。最后,类型的保存和RWLDT是OCC的子逻辑的事实提供了适当的抽象层次的形式推理,这不是本文的主题,但我们希望在未来探索的这项工作是即将推出的MSR原型的基础,它最终将在Maude上运行[9]。MSR和RWLDT之间的语言相似性允许比直接实现简单得多的构造。将MSR映射到流行的CAPSL中间语言[10]将更加困难,因为MSR具有比CIL更丰富的类型本文的其余部分组织如下:我们分别在第3节和第4节介绍MSR和RWLDT。在第5节中,我们定义了从MSR到RWLDT的映射,陈述了它的关键属性,并概述了一些简单的优化。在第6节中,它被应用到我们正在运行的示例Otway-Rees协议中。最后,我们讨论了本文的首先是一些符号。2符号我们用[]表示空列表,用逗号表示列表连接。我们用黑体字表示列表中的标识符,并用上标表示它们的长度。因此,Xn表示n个元素的列表当长度信息与上下文无关或很容易从上下文推断时,我们通常会偶尔,我们会写|X|对于列表X的长度。我们把X的第i个元素记为Xi(或Xn).我们将列表中所有元素的构造都表示为列表本身的构造:例如,我们可以将(MN1. . N n),以及对于NX 1:U1. . Xn:U n.3MSR密码协议规范语言为特定安全协议定制的MSR实例的语法已在[4,5]中给出。在这里,我们将专注于一个更抽象的语法,目前正在[7]中进行形式化,它允许用户声明操作符,如消息连接和加密,而不是将它们硬编码在语言中。下表给出了MSR语法的核心:186I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183方面类型种类上下文状态规则角色M 、NTKDSρP* *= X|* =M|::=类型M N状态| princ|msg | {X : T }T J|{X:T}K::=·::=·|D,X:K|D,X:T| S、M::=规则j:X:U。 (S−→Y:V。S J)::= ROLEi:PRINC. T. ρ| ROLE i : FOR P : princ . T. ρMSR基于一阶项,为了简单起见,我们仅限于标识符(X)和应用。这里,X可以是绑定变量,也可以是先前声明的标识符。为了简洁起见,我们描述原子类型(即,类类型的对象),就像它们是术语一样。保留的原子类型包括状态(state)、主体(princ)和消息(msg)。 我们写{X:T}TJ,一个依赖类型,当X在TJ中不自由出现时,将此语法简化为T→TJ。上下文(在[4,5]中称为签名)是术语声明的列表常量和类型族。状态是一个逗号分隔的多项集(类型为state)。稍后我们也将逗号用于消息连接,这是一种通过周围上下文消除歧义的重载。一条规则将两个状态S和SJ联系起来。后者可以通过一系列存在性声明(例如,用于创建随机数),而规则中的其他变量通常在其头部被普遍量化。角色是由零个或多个存在谓词声明前缀的非空规则序列。我们假设MSR规范满足受限格式,其中存在预测用于引入局部中间状态,以便对角色内部的规则进行序列化。角色有一个独特的所有者P,它可以是通用角色中的任意主体,也可以是固定的主体(例如,一个服务器),用于锚定角色,由关键字FOR(不是绑定器)引入。如[4,5,7]中所述,MSR 特别是,我们假设MSR的本机子类型是由显式子类型模拟的,MSR的模块结构已扩展为单个声明序列,并且所有类型信息都是显式的,而MSR允许逐点重构。简单的预处理或标准技术可以解释这些差异。在本文中,我们不处理MSR的其他它们将是今后工作的主题。I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183187BK我们将依靠Otway-Rees认证协议[12]来说明MSR的使用在该协议中,发起者A想要获得短期秘密密钥kAB以与响应者B安全地通信。它们依赖于服务器S来生成该新密钥,服务器S与它们分别共享长期秘密密钥kAS和kBS本方案的(i) A→B:n,A,B,{nA,n,A,B}kAS(ii) B→S:n,A,B,{nA,n,A,B}kAS,{nB,n,A,B}kBS(iii) S→B:n,{nA,kAB}kAS,{nB,kAB}kBS(iv) B→A:n,{nA,kAB}kAS这里,A和B的范围是任意的主体,S是固定的主体,即密钥服务器。此外,n,nA和nB是随机数,新生成的值旨在避免旧消息的重播。如前所述,我们假设除了princ、state和msg以及它们的元素之外的其他类型的适当声明。对于这个例子,我们依赖于类型nonce,类型家族ltK和stK(分别用于长期和短期密钥),以及串联(重载为infix“,“)和加密(写为{})作为额外的消息构造函数。我们使用状态谓词N 用于表示消息过境在网络上上标p、n和k分别表示从主体、随机数和短期密钥到消息的强制,并且l表示从长期密钥到消息的强制。加密函数所需的共享密钥(完整的MSR使用子排序)。完整的MSR规范可以在[4]中找到。这里我们只显示响应者的通用角色(B):角色2:PRINC.{B:princ}princ → nonce → nonce →(ltK B S)→ state。⎛ ⎞Princ. 随机数。 kBS:(ltKBS). X:msg.<$N(nn,Ap,Bp,X)−→ <$n:nonce。⎟⎜规则21:Bn p p⎟n n ppN(n,A,B,X,{n,n,A,B}lBS),(L B A n nB kBS)⎛ ⎞Princ. n,n A:nonce. 中文(简体)⎜ ⎟规则22:请注意BS:(ltKB S)。k AB:(stKA B).⎠N(nn,Y,{nn,kk}kl),(L B A n nB kBS)−→N(nn,Y)B AB BS这个角色是通用的,有两个规则,都在B和L的量化器范围内。相反,S的角色将是锚定角色,因为S是固定的委托人。188I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183ΣΣ拉吉拉吉ΣMSR的操作语义[4,5]使用转换判断来转换[S] R形式的配置。 这里S是MSR状态,R是收集活动角色的活动角色集,即,实例化的并且可能部分执行的角色,在下一步可用,并且MSR是MSR动态上下文(在[4,5]中称为签名),其说明了在状态S中可用于R的所有动态生成的新鲜常量。 使用比[4,5]稍微丰富的语法,我们以ACTROLEi:FORA的形式编写一个活动角色:王子 与N:T。ρ(同样FOR和WITH都不是绑定器),这意味着它是通用角色ROLE i:PRINC:PRINC的实例。 T. ρ,其中P由A 实例化,L由N实例化,或者锚定角色ROLE i:FOR A:princ的实例。 T. ρ,其中L由N实例化。在本文中,我们首先依赖于两个判断形式来描述transi.命题:给定声明D和角色P,判断D,P <$[S]R−→组:a我[S]RJ表示完全实例化,即,所有外部普遍和存在性量化器的实例化,角色i(A和N定义特定的实例,的作用)。 我们写D,P<$[S]R−→组:ai、j[SJ]RJ 来表示一个过渡,在应用来自活动角色i的规则j时(具有A的实例,N),如果已完全执行,则移除活动i。如果可以导出这些跃迁中的一个,我们简单地写D,P<$[S]R−→I,EJRj[S]在[4,5]中可以找到这种语义的稍微更抽象版本的规则。4用依赖类型构造的开放演算(OCC)是一类类型理论,它涉及元素、类型和论域三类项,并通过实例化和限制导出依赖类型重写逻辑(RWLDT)。类型作为元素集合的抽象,而universe作为类型集合的抽象。OCC由定义全域结构的OCC签名参数化。在本文中,我们使用一个固定的签名S =(S,Type,:,R,≤)与谓词论域S={Type,Type 1,Type2,. },它们形成了一个累积的谓词层次结构。 这意味着我们有类型:类型1:类型2. ,一个子类型关系-J操作类型≤类型1≤类型2. (也称为子宇宙关系),和(s,s,s HSJ)∈R,SJ∈ S,其中H表示w.r. t的最小上界.≤。3OCC的形式系统被设计为在命题作为类型的解释下有意义,其中命题被解释为类型和证明3选择纯型系统的标准参数R的结果是,对于任意的特殊类型S:s(在一个外环Γ中)和T:s′(在一个外环Γ中, X:S),当s,s ′ ∈ S时,我们可以求出任意的特殊类型p{X:S}T:s′′(在一个外环Γ中),或s′′=sHs′.我EI. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183189被解释为这些类型的元素。 因为在OCC中,术语和类型之间没有先验的区别,而且类型和命题之间也没有先验的区别,所以我们同义地使用所有这些概念。OCC具有纯类型系统中已知的标准构造(参见[1,14,15])和一些其他的。OCC项可以是以下之一:论域s、变量X、类型化λ-抽象[X:S]M、依赖函数类型{X:S}T,类型断言M:T,表示命题A的不相关证明的一个构造函数A,命题等式M=N,或运算命题的三个证明之一,写作||A,!!A,还是?A.在这里和下面我们通常使用M、N、P、Q、S、T、U、V、A和B在OCC术语范围内,X、Y、Z在名称范围内。操作命题可以是结构命题,||,由!!指定的计算命题,或者是一个由??表示的断言命题。随后,我们使用τ来在这三个变量上进行范围{||“啊!”,??}。OCC上下文是X:S形式的声明列表。 空的上下文写为[]。通常,我们使用Γ来在OCC上下文上进行范围OCC规范在本文中简单地称为OCC上下文Γ。这样的规范可以通过形式为R:{Y:S}{YJ:S}T→Type的声明引入重写谓词。 其思想是,每个重写谓词可以被视为一个标记的转换系统,它可以以与重写逻辑规范非常相似的方式执行。 注意,R:{Y:S}{YJ:S}T→Type是三元谓词R的声明,其中S是类型T是动作的类型,其范围可以从原子标签到重写证明,这取决于应用程序 的 要 求 。 在 类 型 T 不 依 赖 于 Y 和 YJ 的 情 况 下 , 该 声 明 采 用 R :S→S→T→Type的形式。由于我们正在使用OCC的谓词实例,因此基于经典集合论和合适的论域来定义模型论语义是非常简单的[14]。然而,本文适当的抽象层次是操作语义,这是由OCC的正式系统。它是Maude [9]中实现的重写逻辑[11]及其成员方程子逻辑[2]OCC的形式系统定义了OCC判断的可导性J和已被证明是健全的w.r.t. [14]第14话 为了简洁起见,我们只对所有的判断及其直观的操作意义作一个非正式的解释。• 类型推断判断ΓM→:S断言项M是上下文Γ中推断类型S的元素在操作上,通过语法指导的类型推理给出了Γ和M,并得到了S,190I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183使用计算方程对Γ的结构方程取模进行约简。• 类型判断Γ<$M:S断言M是上下文Γ中类型S的元素。在操作上,给出了Γ、M和S,验证Γ∈M:S相当于类型检查。类型检查总是简化为类型推理和断言子类型判断的验证。• 结构平等判断||(M = N)用于表示M和N被认为是在上下文中T的结构上相等的元素。在操作上,结构平等是通过一个适当的术语来实现的,该术语表示-这样,当它们参与计算时,在结构上相等的项就不能被区分开。• 计算等式判断Γ!!(M=N)是定义简化项的归约概念的判断该判断指出,在上下文中,元素M可以简化为元素NI.在操作上,给出了Γ和M,并且N是使用Γ中的计算方程模Γ中的结构方程约化M的结果。• 断言判断??A说明A在上下文Γ中可通过操作语义学证明在操作上,给出了Γ和A,并且通过使用以下公式的组合归约来验证判断:计算方程和穷举的目标导向搜索使用的作为sertional命题在Γ。这两个过程都发生在对Γ中的结构方程取模。• 主张平等的判断 (M=N)表示M和N在Γ中断言相等,这是一个将相等视为谓词的概念 并包含结构和计算平等的判断。在操作上,Γ、M和N是给定的,判断像其他断言判断一样以目标导向的方式被验证。• 断言子类型判断Γ??(S≤T)包含了断言等式判断,并指出S是T在Γ中的一个子类型,这是宇宙层次累积性的结果。在操作上,而T、T和T则是给定的,判断像其他断言判断一样以目标导向的方式得到验证。• 计算重写判断Γ!!(R MMJP)表示通过在Γ中为重写谓词R指定的计算重写规则,元素M可以重写为元素MJ,并且该重写由元素P标记。 在操作上,给出了Γ和M,并通过在Γ中应用计算重写规则来计算MJ模的计算和结构方程在Γ。 此外,I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183191构造用于该重写的抽象见证P通过固定本节开头的签名,我们介绍了OCC的一个特殊实例。为了本文的目的,我们进一步限制了这个实例,要求规范使用唯一的固定重写谓词R,声明为R:S→S→T→Type。这个想法是,这个三元重写谓词精确地对应于标记的重写关系重写逻辑。为了提醒我们这种对应关系,我们在下面将OCC的这种受限子语言称为依赖类型重写逻辑(RWLDT)。4由于R是唯一的,我们可以使用通常的符号[P]:N而不是较不直观的(RM N P)。 同样,我们使用Γ!![P]:MN表示相应的计算重写判断。5将MSR映射到RWLDT在本节中,我们给出了从MSR到RWLDT的映射的精确定义。kinds、types、terms和state的翻译非常直接。角色和规则的翻译可能看起来有点技术性,但其基本思想很简单。为了使读者更容易理解,我们分三步介绍角色和规则的映射:在5.1- 5.3节中,我们给出了一个以相当明显的方式正确的初始映射,然后我们在5.4和5.5节中的两个进一步的结果是一个映射,它不仅是正确的,而且确保了所得到的RWLDT规范的可执行性(在普通重写系统的意义上)。此外,它避免了引入任何超连续的中间状态,这将导致不必要的不确定性,特别是如果我们使用的符号状态空间探索的翻译的结果5.1初始上下文MSR多集联合构造将被转换为普通的RWLDT函数联合。为此,我们将初始上下文定义为包含以下声明的OCC上下文。有多重集的结构公理:state:Type,empty:state,联合:州→州→州,union_list:||{X,Y:state}(unionX Y)=(unionY X),4与[14]相比,我们在OCC的介绍中省略了断言重写判断,因为我们在本文中不需要重写条件。这些条件在RWL中得到承认,因此在RWLDT的最一般版本192I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183union_assistant:||{X,Y,Z:state}(union(union X Y)Z)=(unionX(unionY Z)),union_id:||{X:state}(union emptyX)= X.初始上下文还包含以下声明,我们只是直观地描述它们。当我们安排翻译时,它们的目的将变得清晰。• princ:Type,msg:Type.主体和消息的类型。• Tij:princ → T → state。 对于每个具有存在性量化器类型T和规则j的角色i,将使用令牌(Tij AN)来表示角色i已经用值A和N实例化的事实。• nat:类型,0:nat和S:nat→nat。自然数用于索引新符号,即,过去没有使用过的符号• F:nat→state。 作为我们的表示的不变量,有一个唯一的(FN),它保存下一个可用的新鲜索引N。• V<$:nat→V。对于可以生成的类型V,该函数都允许我们通过自然数对其元素(中的一些)进行索引,这是生成这种类型的新鲜符号的 一种方式。• E:{T:Type}T→状态。 术语(ET M)表示M是T类型的元素,作为状态的一部分。我们将仅在第5.4节中使用该等同器械。• act:类型,Ai:对每个角色i采取行动,Aij:对每个规则j采取行动。这些常量用于标记翻译产生的重写规则5.2翻译种类、类型、术语、状态和上下文对于下面的内容,我们假设MSR规范不使用除了state、princ和msg之外的初始上下文引入的名称。我们还假设所有声明和绑定的变量都是不同的。这允许清晰地呈现主要思想,而不必担心重命名和捕获。然后,我们定义MSR种类、类型、状态和上下文的翻译如下:• kind(type)=类型type({X:T}K)={X:type(T)}kind(K)• type(X)=Xtype(state)=statetype(princ)=princtype(msg)=msgtype(T M)=(type(T)term(M))type({X:T}TJ)={X:type(T)}type(TJ)I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183193• term(X)=Xterm(M N)=(term(M)term(N))• state(·)=空state(S,SJ)=(unionstate(S)state(SJ))state(M)=term(M)• context(·)=初始上下文context(D,X:K)=context(D),X:kind(K)context(D,X:T)=context(D),X:type(T)。随后,(联合(S1,.,Sn))合并(unionS1(union( S2,.,S n)和(union())表示空。我们也把这个术语称为S1的正式多集,.,S n.这个转换的充分性由以下定理表示:定理5.1如果D是一个良好类型的MSR上下文,则:(i) 如果K是MSR类,则D MSR中的K类型(D)K类型(K):RWLDT中的类型1(ii) 另外,如果D是K类且T是MSR类,则DT:MSR中的K上下文(D)type(T):RWLDT中的kind(K)(iii) 如果另外DT:K和M是MSR项,则DM:MSR中的T i上下文(D)term(M):RWLDT中的type(T(iv) 如果S是MSR状态,则D_STATE(S):RWLDT中的状态此外,D是良好类型的,如果上下文(D)是良好类型的。证明素描。首先,可以直接验证每个MSR推理规则[7]可以由RWLDT[14]的一个或多个推理规则模拟因此,等价式(i)-(iv)的方向为正方向为了处理这些等价的更有趣的方向,我们首先,注意到RWLDT的几个特征与本证明的目的无关。我们的表示并没有以任何基本的方式利用更高的宇宙(超过类型0)或宇宙子类型(类型1在我们的表示中的唯一用途是作为种类的类型)。没有使用RWLDT的计算方程和断言命题。结构方程仅用于表示MSR状态(多集),并且它们以精确表示MSR语法的方式使用。RWLDT的计算重写公理对类型检查没有任何影响,所以这里可以忽略它们。另一个主要的简化是MSR以及RWLDT中的表示不使用λ-抽象,并且RWLDT的类型断言和λ-运算符也不使用。因此,许多194I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183RWLDT [14]的推理规则可以被忽略或简化为平凡的情况,因为它们不能用于RWLDT推导或仅以平凡的形式使用。例如,如果没有λ-抽象和计算方程,计算等式就简化为结构等式。如果没有断言命题,断言命题的推理规则除了断言相等和断言子类型之外都是超级复杂的。如果不使用更高的宇宙,断言子类型与断言相等一致-结构的平等和α-转化。现在很容易通过使用MSR [ 7 ]的推理规则模拟简化RWLDT的每个推理规则来验证(i)-剩下的一点困难是为了克服MSR中的隐式α转换和RWLDT中的显式α转换(包括其更一般的上下文概念)之间的差距,但是[15]中使用的纯类型系统的证明技术可以很容易地适应我们简单的设置。最后,如果上下文(D)是良类型的,则证明D是良类型的,可以通过使用前面的语句对DQ重要的是要注意,该定理并不意味着上下文上下文(D)中的每个良好类型的RWLDT项是MSR项、类型或种类的表示例如,RWLDT类型Type→Type:Type1的对应物在MSR中不存在类似地,我们可以使用λ-抽象和其他结构在RWLDT,但他们没有对应的MSR。事实上,MSR的受限语法和我们的表示划分出RWLDT的子语言,并且只有该子语言中的术语在操作语义中使用。然而,规范本身需要结构方程和计算重写公理等构造,这些都在这个子语言之外。5.3转换角色和规则为了进一步简化表述,我们假设第i个角色的标识符是i,第j个规则的标识符是j。然后,我们定义MSR角色和规则的转换如下(使用P和PJ在角色序列上进行范围):• ro les(·)=[].roles(ROLE i FOR A:princ. T. ρ)=Ri:role(i,A,RSL:T. ρ)。roles(ROLEi:princ. T. ρ)=Ri:{P:princ}role(i,P,princL:T. ρ)。roles(P,PJ)=roles(P),roles(PJ).• role(i,P,p.l.:T.ρn)={Z,ZJ:nat}{L:type(T)}fresh(Z,L,T,ZJ)→I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183195[Ai]:(FZ)(union((Ti 1 P L),.,(Tin P L)(F ZJ),rule(i,P,L,T,ρn),. ,rule(i,P,L,T,ρn).1N• rulee(i,P,L,T,RULEj:ruleX:U. M−→V:V。N)=JRij:{P:princ}{Z,Z:nat}{L:type(T)}{X:type(U)}{Y:type(V)}新鲜(Z,Y,V,ZJ)→[Aij]:(union((Tij PL),(FZ),state(M)(union((state(N),(F ZJ)。• fresh(Z,Yy,Vy,ZJ)=Yy = V<$y(Z)),Yy = V<$y(S(Z)), . . ,Yy = V<$y(Sy−1(Z)),Z J = Sy(Z).1 1 2 2年在最后一个方程中,我们假设对于V型,存在注入,你是我的朋友初始上下文。:nat→V,需要包含在上面我们用A1,.,An→B,使A1→…→A n→B,这意味着A1,...,n是条件。然而,还应该注意的是,在这里使用条件不是必要的,因为它们都是形式Y=Q,因此可以简单地消除。我们使用条件只是为了更好的可读性,并与MSR语法保持更直接的对应关系。角色定义背后的想法是,它将每个MSR角色映射为到几个RWLDT重写公理:有一个标记为Ai的重写公理,表示该角色的实例化。此外,对于其规则j中的每一个,存在一个标记为Aij(由规则生成)的重写公理。第一个公理Ai,除了生成新实例所需的新项之外,还生成令牌(Ti1 P L),...,(PL中的T),表示此角色的任何规则都尚未执行。其余的每个公理Aij模拟相应的MSR规则j,因此规则的每个应用都删除其相应的令牌。这实现了MSR策略,即活动角色的规则只能执行一次。下面的引理表示新符号的生成在RWLDT中被正确地表示。引理5.2(新鲜度不变性)设(D,P)是MSR规范。RWLDT中的表示保持以下不变量:如果在RWLDT状态中存在形式为(F(Sn0))的项并且没有其他F的出现,则对于每个k(包括0),项(Sn+k0)以及因此V(Sn+k0)是新鲜的,即,它不会发生在国家的任何其他部分证明素描。可以直接验证为我们表示中每个RWLDT重写公理的归纳不变量,使用我们前面的假设196I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183在初始上下文中,0和S未在MSR规范中使用Q为了表达MSR和它的表示之间的关系,我们还需要一个动态实体的表示,比如主动角色:• ac trole s(·)=empt y。actroles(ACTROLE i:FOR A:princ. 与N:T。 ρ)=所有(Tij AN)s.t. ρ包含规则j。actroles(R,RJ)=(unionactroles(R)actroles(RJ)),其中R和RJ的范围在活动角色集上。回想一下ACTROLEi:FORA:princ。与N:T。ρ是主动角色的形式,即,一个已经(完全)实例化并可能部分执行的对象。活动角色集包含这种形式的活动角色的事实对应于以下事实:对于活动角色的每个规则j(即, 尚未执行的规则),项(TijAN)是表示中的分布式状态的一部分。随后的定理证明了在所有其余定理中使用特定形式定理5.3(表示不变性)设(D,P)是MSR规范。如果context(D),roles(P)不存在!![P]:M≠MJ,M是MSR配置的表示,即,对于某个n 、 某 个 MSR 状 态 S 和 某 个 MSR 活 动 角 色 集 , 形 式 为 ( union ( ( F(Sn0)),state(S),actroles(R))R,则MJ也是MSR配置的表示证明素描。同样,这是一个归纳不变量,显然适用于我们表示中的每个RWLDT重写公理。Q为了证明主定理,我们需要以下引理。引理5.4(表示唯一性)设(D,P)是MSR规范。然后,每个在MSR操作语义中可达的MSR活动角色集R都可以由其表示角色(R)唯一地重构证明素描。请注意,活动角色集只能包含那些可以通过(完整)实例化已知角色并随后删除其某些规则(在执行规则后)而实际获得的元素。我们需要考虑两种情况:(i) 如果至少有一个令牌(左)表示活动角色,则此令牌携带完整信息,即i、A和N,以确定初始角色实例。不幸的是,我们需要论证的是,所有形式为(Tij AN)的令牌一起唯一地确定了这个主动角色的规则,即,这些规则仍然需要执行。唯一可能引起混淆的原因是表示可能包含几个I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183197Σ拉吉ΣEΣΣ拉吉具有相同值A和N的相同活动角色i的实例同时执行。由于N是新生成的,所以只有当N是空列表时才会发生混淆,即,当角色没有任何存在量化器时。由于MSR规范的限制格式(存在谓词用于顺序化角色内的规则),这意味着角色只能有一个规则,因此它只能处于一种状态,即它被实例化但未执行之后的状态。(ii) 如果没有表示活动角色的令牌(左),则该角色必须已完全执行,因此通过我们对MSR的操作语义的定义因此,它对活动角色集的贡献也是唯一确定的。Q引理5.5设(D,P)是MSR规范,设S,SJ是MSR状态,设R,RJ是MSR活动角色集。那么对于所有的n,k,我们有以下等价:这是一个关于MSR的例子,它包含了t =n,n=Jn+k。t. D,P<$[S]R−→组:a我[SJ]RJicontext(D),roles(P)[Ai]:(union((F(Sn 0)),state(S),actroles(R)(union((F(Sn+k0)),state(SJ),actroles(RJ),nJn+k RJRJ存在MSR上下文,S.T. D,P[S]−→A,N [S]jiangi、jcontext(D),roles(P)[Aij]:(union((F(Sn 0)),state(S),actroles(R)(union((F(Sn+k0)),state(SJ),actroles(RJ).在这两个陈述中,我们确定了在上下文(D)中结构上相等的术语证明素描。首先,一个观察简化了引理的两个状态的证明:我们可以使用前面的引理来验证,(union((F(Sn0)),state(S),actroles(R)只能表示MSR状态S、MSR活动角色集R,因此只能表示某个动态上下文的MSR配置[S]R同样地,(union((F(Sn+k0)),state(SJ),actroles(RJ)只能表示一个配置[SJ]RJ再次为一些动态上下文J。为了证明引理的第一个等价性,请注意左边表示角色i是为某个主体A实例化的(如果它是泛型的,否则A已经固定),存在量化器是用新符号 实 例 化 的 , 相 应 的 角 色 实 例 被 添 加 到 活 动 角 色 集 。 根 据 左 侧(Becomes_n+k)k上的MSR动态上下文中的变化,可以重新生成一个数据包,其中,这个角色有k个存在量化器。 我们需要验证MSR的操作语义等同于右侧,即,到我198I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183Σ拉吉在RWLDT中应用标记为Ai的重写公理(参见角色定义)使用新鲜度不变性引理很容易看出,角色i的存在量化器使用在此过程中生成的k个新鲜项N正确地实例化。除了保持新鲜度信息之外,该规则的唯一效果是项(Ti 1 A N),.,(A N中的T)被添加到RWLDT状态。这只能对应于将角色i的新实例添加到活动角色集。对于引理的第二个等价,注意左手边表示角色i的实例是从活动角色集合中选择的,并且它的规则j,whi ch是fRULEj:X:U。 M−→V:V。不 , 我 被 处 决 了 。 根 据 在 左 侧 的 动 态 MSR 上 下 文 中 的 变 化 ,(n_becom_S_n+k)k个存在性量化器被定义为一个规则,其中意味着该规则具有k个存在性量化器。我们再次需要验证MSR操作语义中的这一步是否等同于右侧,即,在RWLDT中应用重写公理Aij(参见规则使用新鲜性引理,很容易看出,规则j的量化器使用k个新鲜项被正确地实例化。除了保持新鲜度信息之外,该规则还有两个效果:它用状态(NJ)替换状态(MJ)(MJ和JNJ分别是M和N的实例),这是一个与MSR规则的执行精确对应的步骤,并且它删除令牌(Tij AN),这只能对应于规则被从活动角色中删除的事实,因为它已经被执行。显然,对于这两个等价性,详细的证明将在MSR 生成的新符号和RWLDT生成的新项之间建立双射。Q下面的定理总结了前面引理的陈述:定理5.6(可靠性和完备性)设(D,P)是MSR规范,S,SJ是MSR状态,R,RJ是MSR活动角色集。那么对于所有的n,k,我们有以下等价:这是一个关于MSR的例子,它包含了t =n,n=Jn+k。t. D,P<$[S]R−→I,E[SJ]RJi存在Ps. t。 上下文(D),角色(P)!![P]:(union((F(Sn0)),state(S),actroles(R)))(union((F(Sn+k0)),state(SJ),actroles(RJ),其中我们识别在上下文(D)中结构上相等的术语5.4实现可执行性不幸的是,产生的RWLDT规范在重写的普通意义上不一定是可执行的,因为可能有一些规则的变量在右手边,而不出现在左手边,因此不能执行。I. Cervesato,M.O. Stehr/Electronic Notes in Theoretical Computer Science 117(2005)183199拉吉Σ受匹配约束。因此,我们应用另一个简单的转换,通过使用谓词E:{ T:Type } T → state,使某些类型及其元素在状态中显
下载后可阅读完整内容,剩余1页未读,立即下载
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- 保险服务门店新年工作计划PPT.pptx
- 车辆安全工作计划PPT.pptx
- ipqc工作总结PPT.pptx
- 车间员工上半年工作总结PPT.pptx
- 保险公司员工的工作总结PPT.pptx
- 报价工作总结PPT.pptx
- 冲压车间实习工作总结PPT.pptx
- ktv周工作总结PPT.pptx
- 保育院总务工作计划PPT.pptx
- xx年度现代教育技术工作总结PPT.pptx
- 出纳的年终总结PPT.pptx
- 贝贝班班级工作计划PPT.pptx
- 变电值班员技术个人工作总结PPT.pptx
- 大学生读书活动策划书PPT.pptx
- 财务出纳月工作总结PPT.pptx
- 大学生“三支一扶”服务期满工作总结(2)PPT.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)