没有合适的资源?快使用搜索试试~ 我知道了~
20理论计算机科学电子笔记71(2003)网址:http://www.elsevier.nl/locate/entcs/volume71.html20页基于多集项重写的组通信协议建模Grit Denker1,2和Jon Millen1,3计算机科学实验室,SRI国际,门洛帕克,CA 94025,美国。摘要安全组管理协议在涉及联盟成员之间的保密认证通信、认证组决策或组成员身份和访问控制的安全管理的应用中是必不可少的。新的语言和模型是必要的,以适当地捕捉这样的协议的概念,并使他们服从形式化分析。为此,我们开发了多播公共认证协议规范语言(MuCAPSL)及其中间语言MuCIL(MuCAPSL中间语言)。MuCIL是基于多集项重写规则,允许状态变化被简洁地呈现,并在某种程度上,密切配合现有的协议分析工具的要求。借助群-迪-赫尔曼协议套件,我们说明了如何使用多集项重写安全组通信的原则关键词:协议规范,安全组管理1介绍可靠的多播协议已经被开发为向一组进程提供消息和成员服务的可靠有序传递的手段构建用于公共网络的多播协议的一个挑战是安全性。诸如联盟成员之间的保密认证通信、认证的组决策或组成员的安全管理和访问控制等服务是安全可靠的组管理的核心。新的协议和框架已经被设计来在网络上创建多播组并支持安全的组通信*由DARPA通过SPAWAR系统中心根据合同N66001-00-C- 8014提供支持[1]我们感谢卡罗琳·塔尔科特(Carolyn Talcott)对本文早期版本提出的有益建议2电子邮件地址:denker@csl.sri.com3电子邮件地址:millen@csl.sri.com2003年3月,出版社dbyElsevierScienceB。 V. 操作访问和C CB Y-NC-N D链接。登克尔-米伦21(e.g.、GDOI [2]、GSAKMP [9])。一些现有的用于安全通信的密钥交换协议已经扩展到组设置(例如,群Di Chine-Hellman GDH [13]及其认证形式A-GDH [1])。关于组管理协议的形式化分析只有少数结果Pereira和Quisquater分析了A-GDH [12],Meadows在GDOI的早期版本中发现了安全漏洞[11]。 组管理协议的分析对形式化分析技术提出了新的挑战。新的语言特性和模型是必要的 , 以 适 当 地 捕 捉 这 些 协 议 的 概 念 。 MuCAPSL ( Multicast CommonAuthentication Protocol Specification Language ) 及其 中间 语言 MuCIL(MuCAPSL Intermediate Language)就是为了满足这些需求而设计的基本的设计原则是(i) 提供一种高级的,但数学上有良好基础的协议语言,允许将已发布的安全组通信协议描述轻松转换为形式语言(ii) 提供一种单一的公共接口语言,可以用作许多形式化分析技术或工具的输入格式。MuCAPSL和MuCIL是CAPSL和CIL协议分析工具对单播协议的扩展[5,6,4]。MuCAPSL为多播安全协议提供了高级规范概念,例如使用单播和多播寻址的消息传递,组成员数据和基本加密运算符。MuCIL更接近于协议的状态转换它有两个目的:在多集项重写方面帮助定义MuCAPSL的语义,以及作为一个接口,通过它可以使用各种工具分析MuCAPSL中指定的协议本文的重点是MuCIL及其术语重写语义。我们将说明建模组通信协议的帮助下,组Di Die Hellman(GDH)协议套件的想法GDH的概述见第2节。第3节提供了一个多播协议的语义框架。 重写规则生成在第4节中介绍。第5节介绍了今后的 工作。2群迪-赫尔曼协议我们借助Group Di Jade-Hellman(GDH)协议来说明语义模型,该协议是Cliques协议套件的基础[13,14]。GDH[13]是两方Di Chine-Hellman密钥协商方案到任意组大小的扩展GDH协议集由密钥分配算法和成员添加和删除协议组成出于本文的目的,我们选择密钥分发协议作为示例,因为它包含寻址到特定组成员的单播消息以及寻址到所有组成员的广播消息。GDH中的组密钥是根据来自每个登克尔-米伦22下流式M组成员。为此目的,每个群成员Mi具有随机数Ni。组成员位置编号(“M i“中的它们在某种程度上是稳定的,但可以因为组成员的变化而改变通过将取幂基g提高到所有随机数的乘积来计算组密钥,nN i组成员。每个群成员都知道取幂基,而单个随机数对特定的群成员是秘密的。在消息交换中,成员们传递部分密钥值,这些密钥值保持他们的秘密,并且仍然允许其他组成员计算共享组密钥。图1示出了大小为4的组的组成员之间的通信。成员M1向其邻居M2发送一个由取幂基g和gN1组成的数组。每个中间成员接收这样一个数组,将每个数组元素与自己的随机数相乘,并将接收到的消息的第一个数组元素复制到其传出消息中。这样,在组成员之间发送的数组的长度总是等于接收成员的位置号。GDH的这个最后,最后一个组成员收到一个长度为n的数组,它通过将第一个数组元素提高到Nn次幂来计算组密钥。在此之后,Mn在多播中用包括其随机数N n的部分键值的数组(“向下滚动”阶段)回复该组其他组成员可以通过将适当的数组元素提升到其随机数的幂来计算来自该多播消息的组密钥。意图所有组成员共享组密钥G上流式尼。M1gN1g1M2M2gN1N2克N2男3M3gN1N2N3gN2N3gN1N3gN1N24M1-3gN2N3N4gN1N3N4MgN1N2N4 4组密钥:gN1N2N3N4Fig. 1. 概述:组密钥-Hellman密钥分发2.1角色分离在GDH协议中,我们可以区分三个不同的角色,在不同的行为序列的意义登克尔-米伦23−M1上流式M广播Mi上流式上流式M广播MN上流式广播MMiMN角色是M1、Mi和Mn。M1是M1的角色,即发起密钥分发的组成员。角色Mn中的成员Mn是群的最后一个成员,其位置号等于群大小。所有其他成员都是Mi角色(只有一个角色Mi,而不是从2到n1的每个i都有一个角色图2示意性地表示了这些角色。多播消息通过用方框终止消息箭头来指示,如来自Mn的广播消息中所消息目的地为图二. 密钥分发协议图2中的示意性角色图可以通过更详细地显示消息的内容来详细说明这在图3和图4中完成。M1N1,gn克尔克gk= 1,k#jMj=1.. n-1ID-1ID-1NkNkgk=1 ,gk= 1,k #jj=1. ID-1IDidNkNkgk=1 ,gk= 1,k #jj=1. IDn克尔克gk= 1,k #jj=1.. n-1图三. 密钥分发协议n-1n-1NkNkgk=1 ,gk= 1,k #jj=1. n-1n克尔克gk= 1,k #jj=1.. n-1M见图4。 密钥分发协议M登克尔-米伦24这些图抽象了许多重要的细节,例如如何存储接收的消息,何时计算新的密钥贡献Ni,以及如何组成消息。这些细节是MuCAPSL规范的一部分,可以在[7]中找到。图形符号仅用于概述相关协议角色,并说明主要消息流程和消息内容。2.2MuCAPSL规范由于我们的重点是在MuCIL中重写术语,因此我们在这里不包括然而,它可能有助于看到部分样本,所以这里是M1的角色规范协议密钥分发;角色M1:GDH代理;假设return 1;HOLDSNxt;新消息N;-> Nxt:g^N,g;<- KD;Kn=KD[1]^N;结束M1;...END KeyDist;在这个规范中,KD是整个下行数组;M1只需要它的第一个元素来计算新的组密钥Kn。3多集项重写语义如GDH协议所示,在组通信协议中存在各种不同的事件。 这些事件包括多播和单播消息的发送、消息内容的接收和检查,以及改变组成员状态的内部(加密)计算。所有这些事件都必须在底层语义中相应地建模,以捕获组通信协议的含义。在MuCIL方法中,协议被理解为状态转换系统。每个协议事件都会使系统经历一次状态转换。协议是通过一组转换规则来描述的,F1,. ,Fk−→FX1,. ,Xm:G1,. ,Gn,其中每个Fi和Gj都是“事实”。 事实是原子公式的形式P(t1,.,t r),其中P是谓词符号,自变量t i是项。一个项是由常数、变量和函数符号构成的变量、常量和函数都是类型化的.登克尔-米伦25−→∃它们通常用于逻辑公式;变量可以被实例化。函数符号表示协议中使用的加密等计算。在协议建模中,事实用于表示进程进入状态或消息的传输 网络环境的状态是基础事实的多集合,当规则左侧的事实可以与多集合中的事实匹配时,规则有资格触发当规则触发时,多集中的匹配事实被移除,并被规则右侧的事实替换,根据模式匹配所需的替换进行将事实从多集减少了它的多重性,如果它是一个以上在右侧事实中,预先量化的变量用新的常量实例化,就像逻辑中的skolemization步骤一样。在加密协议模型中,这些变量表示随机数,因此必须使用新值实例化它们。用于密码保护的多集项重写方法的起源出现在[8]和[3]中。3.1MuCIL符号作为一种用于表达协议转换规则的语言,MuCIL具有特定的语法和对事实中使用的谓词符号的特定选择。MuCIL中的规则,以及事实和术语,都是用函数符号表示的,表示一个树结构,带有标记的节点有零个或多个有序的子节点。MuCIL中有两种规则--形式规则(事实(...),id(.),事实(.)) 和条件重写规则的形式规则(事实(...),id(.),事实(.),如果(.))。“ids”项列出了量化的变量。The “if” clause contains a boolean为了方便起见,引入了条件规则原则上,一个条件规则可以由一系列无条件规则来模拟,其中第一个转换创建一个状态,该状态携带评估测试条件的结果这两个规则的序列可以通过信号量策略来原子化。然而,条件规则更容易产生和理解。在本文中,为了可读性,我们使用规则形式的事实(变量)的事实,如果测试中的地方的操作规则(事实s(事实s),ids(变量s),事实s(事实s),if(测试))(和类似的无条件规则)。MuCIL有一个约定,只有具有复数函数名的术语(例如,事实、ID、项)具有可变数量的参数。格式条款(.) 出现如此频繁,为了本文的可读性,它被[…]]中。登克尔-米伦263.2事实对于多播协议建模,使用了三个事实谓词:用于消息的mmsg,用于协议角色进程(我们称之为“代理”)的状态的消息事实具有mmsg([. ]),其中术语表示消息字段。我们在消息事实中不保留发送者或接收者地址还有单播消息和多播消息之间没有区别,因为攻击者可以重新广播单播消息,或者阻止任何消息(多播或非多播)到达多个或任何目的地。表示协议角色中座席状态的事实至少有四个参数:state(ident,role,state-label,[...]).第一个参数是组成员,第二个是它的角色,第三个是状态的序列号或其他标签,第四个是代表代理的瞬时本地内存的术语列表,例如随机数,会话密钥和其他组成员的名称。规则中典型的左侧代理状态事实可能如下所示state(M1,KeyDistM1,2,[])这里,M1不是角色名,而是GDHAgent类型的变量,尽管这个标识符是从规范中给出的角色名中借用的角色名KeyDistM1是通过组合协议和角色名自动生成的常量。我们必须这样做,因为角色名称在协议中不是唯一的。这个例子没有组件术语,因为角色不需要任何特定于会话的内存;它只使用和修改组成员的内存状态记忆组件的一个重要概念特征是,它们的值要么是未定义的,要么是这是真的,因为协议规范中的状态变量被认为对协议会话具有单个值,然后在会话结束时随着协议进程的终止而消失(通常,我们使用术语我们在第四个参数中将状态分量值聚集到一个术语列表中,因为这些值是协议特定的,而每个协议的每个角色都有前三个。组成员的状态包括成员的身份、位置号和组的大小等组成部分集团成员国事实具有以下形式member(ident,[...]).登克尔-米伦27成员的身份是一个特定固定类型的对象因此,组成员是一个抽象,允许单个用户(类型为Principal)作为所有者独立地参与多个不同组的成员由于组成员状态组件在协议会话中持续存在,因此它们永远不会被视为未定义,但始终被视为已持有。然而,与代理状态变量不同,它们可以在任何协议会话期间更新.事实上,可以想象,一个角色或同一集团成员的两个或多个代理人可以多次更新这些信息状态中成员标识之后的状态组件取决于组协议体系结构。给定组的特定组件集在MuCAPSL规范中声明为GroupMember子类型定义的一部分。因此 , 我 们 声 明 具 有 以 下 命 名 属 性 列 表 的 Group-Member 的 子 类 型GDHAgent:pos,n,Kn,N,Nxt,KU,KD。它们分别存储有关组成员构成组密钥、上行下行邻居的地址以及上行下行和下行部分密钥的数组属性的名称在MuCAPSL规范中有意义,但在MuCIL规则中没有意义然而,翻译器试图通过使用属性名称(以及状态变量名称)作为规则中相应的虚拟变量的名称来因此,MuCIL规则中典型的左侧成员事实如下所示:member(M1,[pos,n,Kn,N,Nxt,KU,KD]).4事件和规则生成状态转换规则需要用于协议操作、攻击者操作,有时还需要用于与安全目标的定义和检测相关的操作。我们在这里只讨论协议规则,因为其他规则不是协议特定的,或者它们受到不同分析工具的限制MuCAPSL组协议规范通常指定多个协议,因为相同的组响应不同的协议以实现这种功能。例如密钥分发、添加成员、删除成员、组拆分或组合并。在每个协议中,有几个角色-例如,在GDH密钥分发协议的情况下有三个角色。每个协议中的每个角色都被单独指定为涉及消息和计算操作的事件列表对于每个角色,我们生成一系列状态转换规则,从初始化规则开始创建第一个代理状态。在MuCAPSL中,我们区分了三种不同的消息事件:接收消息、发送单播消息或发送组播消息。MuCAPSL事件的具体语法在这里并不重要;登克尔-米伦28[10]. 在抽象语法级别,这三个消息事件是recv(terms(.)),send(ident,terms(.)),mcast(terms(.))如前所述,MuCIL忽略了发送和mcast之间的差异。发送和接收之间的区别在于,发送生成如下转换:成员(M,[. ])、state(M,. )−→成员(M,[... ])、state(M,. ),mmsg([. ])及一接收生成一过渡相似成员(M,[. ])、state(M,. ),mmsg([. ])−→ member(M,[. ])、state(M,. )在这两种情况下,座席状态标签都会递增。接收转换还可以修改成员和代理状态的组件请注意,通过引用相同的组成员,将代理和代理状态事实绑定在一起。根据规则触发的语义,接收规则从多集中删除消息事实如果消息应该是多播的,那么多个组成员如何接收它?答案有三个选择一种可能性是更改规则,在右侧包含相同的消息事实,以便为其他收件人保留该消息事实这种冗余被认为是不可取的,因为它使规则生成器的输出变得混乱。或者,我们可以在MuCIL规则语义中为消息事实设置一个例外。最后,我们观察到,没有例外是必要的预先服务状态可达性,因为标准的攻击者被假定为能够复制消息。MuCAPSL也有等式事件term = term,它生成的规则根本没有消息,只有一个状态修改。一个等式可以是一个测试或一个作业。如果它是一个测试,则等式会在规则中的if条件中重新出现,并且唯一的状态修改是在代理状态中增加状态标签如果是赋值,则修改成员和座席状态组件需要一个特殊的事件来使属性的值被更新为新的值,例如,在GDH密钥分发中,当组成员需要一个新的随机数时。这是MuCAPSL中的事件NEWX,或抽象语法中的new(X)如果状态变量最初没有被保存或之前没有被接收,则无论它们在哪里被首次使用,都会为它们生成新的值MuCAPSL有几个有限的结构用于控制流。我们试图避免支持IF-THEN-ELSE,因为当分支发生时,协议应该结束一个角色并开始两个新角色中的一个,选择信息存储在属性中。但是,与其他执行流程构造一样,MuCIL可以使用更改状态标签的规则和现有的事实类型来支持条件分支。在多播组协议中经常需要像DO-UNTIL这样的东西登克尔-米伦29尽管它在GDH示例中没有出现。当一个组的领导者必须等待一些指定数量的其他成员的响应才能继续进行时,需要它来获得多数票,或共识,或协议,或足够的分裂秘密份额来重新生成它。ABORT事件是一种绕过角色的正常要求的方法-在每个状态下只需要一种消息。一些组协议广播中止消息,该消息停止每个成员正在扮演的任何角色中止消息将发送到单独的角色,该角色将发出ABORT事件以停止该组成员的现有代理。4.1执行性规则生成器将MuCAPSL事件转换为重写规则。在此过程中,必须通过可实现性检查,以确定规范是否可实现。可实现性算法确定代理必须做什么来发送或接收消息(多播或单播),并在给定代理的当前状态的情况下判断显式和隐式操作是否可能状态转换规则是可实现性算法的产物。可实现性失败意味着无法生成正确建模事件的可实现性的关键概念是可计算性、可接受性和可逆性。如果一个代理持有必要的变量(或者在随机数或会话密钥的情况下,可以在随机数上生成),并且复杂项中涉及的所有函数都可以由代理访问,则项可以由代理计算。如果函数是公共的(这是正常情况),或者对于代理来说是私有的,那么它们是可访问的。私有函数对于用户来说是本地的,但它们不是状态组件,因为它们是常量,而且它们通常与拥有组成员的主体相关联,而不是与组成员相关联。它们用于保存永久信息,例如主体的长期秘密密钥sk(A),它是A私有的。因此,sk(Alice)可以被Alice计算,但不能被Bob计算。私有函数是用私人财产在MuCAPSL。如果代理拥有足够的变量和子项来执行隐含的模式匹配,则表示消息字段的项是可接收的对复杂术语的模式匹配意味着通过反转用于合成术语的操作来提取其组成部分的能力。连接总是可逆的,如果正确的键是可计算的,则连接也是可逆的。因此,为了接收指定为ped(pk(A),X)的消息,需要A的秘密密钥sk(A),并且如果协议指定该消息由不同的主体B接收,则该协议将是不正确的。在接下来的部分中,我们将详细介绍在规则生成过程中如何处理每个事件我们从处理任何事件之前生成的初始化规则开始。登克尔-米伦304.2状态初始化状态初始化规则是那些在左侧没有状态谓词的规则。成员状态事实和座席状态事实都有初始化规则转换器生成初始代理状态事实,但不生成成员状态事实。成员初始化规则类似于−→成员(M,[A,B,...])如果(.).其中M是具有属性A、B、. 等等。我们假设每个主体和组只有一个成员国这一假设很重要,因为它消除了关于哪个成员国受角色转换规则约束的这个唯一性假设应该用if条件来表示它很难表达,因为它指的是整个多组事实。规则生成器不尝试生成成员初始化规则。每个角色都有一个初始化规则来生成相应的初始代理状态事实。在MuCIL中,我们用所有状态变量生成初始状态事实,其中一些可能在初始状态中未定义,并且仅在协议的后续步骤中分配,因为它们的值在消息中生成或接收。碰巧的是,在密钥分发协议中没有使用状态变量(定义或其他),因此角色M1的初始状态谓词是state(M1,KeyDistM1,0,[])。角色规范可能有有两种假设:“holds”假设,表示某些状态变量具有有意义的初始值(但不指定这些值),以及其他假设,写为布尔表达式,给出或约束属性或持有的状态变量的对成员属性的假设用于标识它可以执行哪些角色。例如,在GDH中,角色M1是pos= 1时唯一可能的角色。约束属性值的假设成为该角色的初始化规则的状态变量最初是未定义的还是保持的对于规则生成器来说是重要的信息,因为如果该变量尚未保持,则使用状态变量的值的事件不可实现规则生成器知道哪些变量最初被保持,因为它们被假设为保持,并且它确定哪些最初未定义的变量后来由于协议事件而被保持状态变量的保持状态在规则中并不显式,但在确定哪些规则是可实现的时是隐式密钥分发协议中三个角色的初始规则,distin-由位置编号属性pos的值所隐藏的是member(M1,[pos,...])−→ state(M1,KeyDistM1,0,[ ]),member(M1,[pos,...])、登克尔-米伦31−→−→−→if(eqn(pos,1))member(Mi,[pos,n,...])state(Mi,KeyDistMi,0,[ ]),member(Mi,[pos,n,.]),if(and(isgrtr(pos,1),isless(pos,n)成员(Mn,[pos,n,...])state(Mn,KeyDistMn,0,[ ]),member(Mn,[pos,n,.]),if(eqn(pos,n))第一个和最后一个可以在没有if条件的情况下编写,分别用1或n代替pos,用模式匹配代替条件测试人们可能还会问,是否可以为同一个角色创建多个代理实例。这是可能的形式主义,但通常被认为是不可取的。协议规范可以通过显式地向成员状态添加信号量属性来防止并发角色复制。下面我们讨论ABORT操作时,将进一步描述这类问题4.3发送和Mcast很容易生成一条规则,该规则发送一条包含术语X1,..., X n. 首先,测试X1,.,n是可计算的。如果是,规则简单地增加状态标签并将消息添加到右侧事实。在GDH KeyDist角色M1中发送g^N,g产生规则成员(M1,[...,N,.] )),state(M1,KeyDistM1,1,[])成员(M1,[...,N,.])、state(M1,KeyDistM1,2,[]),mmsg([exp(g,N),g])4.4新当属性由于NEW事件而接收到新值时,或者当首次使用作为随机数的状态变量时,新值由转换规则创建,其中该属性或变量出现在存在量化列表中。在GDH示例中,角色M1中的代理必须生成新的临时数N,然后才能向其邻 居 发 送 部 分 密 钥 。 在 MuCAPSL 中 , 这 表 示 为 NEW N , 解 析 为 new(N)。以下是针对图1中的代理M1的NEW N事件生成的规则。KeyDist协议。成员(M1,[...,N,.])),state(M1,KeyDistM1,0,[ ])−→(N!)成员(M1,[...,N!,.]),state(M1,KeyDistM1,1,[])请注意,我们必须发明一个新的虚拟变量N!为新登克尔-米伦32值N。4.5数据类型和术语在我们解释其他类型事件的规则生成之前,我们需要更多地说明规则事实中使用的术语的构造某些对象类型和函数签名被认为是MuCAPSL翻译器给出了一个包含内置符号的抽象数据类型规范的序言,并且允许用户提供额外的声明。在Prelude中,最通用的对象类型是Object,其最重要的子类型是Boolean和Field。Field类型的对象可以显示为消息内容字段。Field有一个子类型Atom,包含熟悉的对象类型,如Principal,Nonce和Nat(自然数),以及一些特定于加密的类型,如Pkey(公钥)。非原子字段是通过使用构造函数cat进行连接而形成的。序言声明了公钥加密运算符ped和私钥加密和解密运算符SE和SD。对于有限长度的对称密钥,算术运算定义在Skey类型上。在多播组协议中,通常需要可变长度的消息或消息字段,以及需要保持类似数组的值序列的属性(例如,GDH的上行和下行消息中的部分密钥的数组)。出于这个原因,我们根据需要引入了Array类型和子类型数组由自然数索引,其元素的类型为Field。有子类型Sarray,其元素类型为Skey,以及其他一些类型。(数组子类型目前无法在Mu- CAPSL中参数化定义,因此我们需要为具有不同元素类型的数组指定子类型数组有一些运算符,比如at用来提取第i个元素,with用来给第i个元素赋值,proj用来投影到数组的连续子序列,acat用来连接两个数组,size用来确定数组的长度有一些元素级的运算符可以简化普通的群计算,例如MuCAPSL中的A^^N,使用抽象语法aexp(A,N),创建一个A值的数组,每个值的幂为N。在MuCAPSL中,也可以将组成员属性定义为函数,也就是说,它们在任意数据类型上进行索引。例如,可以将组成员的密钥表声明为一个函数,其中存储了每个其他组成员的共享密钥skTable(GroupMember):Skey.将此函数作为一个属性包含进来,允许我们为每个表条目单独重新分配值。与数组不同,函数不是数据类型的对象但是,出于规则生成的目的,它们的处理方式类似。接下来的两个部分解释了接收事件和等式事件的规则生成登克尔-米伦334.6接收的规则生成在一种语言中,接收消息在概念上是复杂的,在这种语言中,接收到的术语被解释为模式,并且它们提到的状态变量可能会或可能不会由于接收消息而被修改假设一个协议生成一个随机数N,它首先从生成它的用户A发送给用户B,然后从B返回给A。当B接收到N时,它是一个新的值,将被存储在B当A从B接收到N时,消息中接收到的值将与最初生成的值A进行比较,以测试协议中可能的错误或干扰对于状态变量,我们可以简单地通过观察状态变量是unfined还是hold来确定哪个操作是合适的对于属性,任何一个动作都是可能的,并且可能在给定的消息中预期,并且指定必须显式地指示预期的动作在MuCAPSL中,接收到的消息中的未修饰的属性N应该被存储,而语法形式?N表示消息中N的值应该等于已经存储的旧值,并且应该执行比较测试前缀问号的抽象语法是compare(),但“compare”是一个翻译器指令,在最后的MuCIL。一新的NN发送N?N接收NB接收N发送N图五. 接收如果N是一个属性,则事件recv([N])被解释为一个分配。下面是实现它的规则的草图,用于某些角色在状态4. 成员(M,[. N.]),state(M,roleM,4,[...]),mmsg([N!])−→成员(M,[. N!...]),state(M,roleM,5,[...])请注意,我们必须发明一个新的变量名N!对于消息中的N如果接收事件是recv([compare(N)]),则生成相同的规则,只是不需要N!它在任何地方都使用N。因此,状态改变只包括增加状态标签,并且只在比较成功时发生,也就是说,消息包含已经在成员状态中的N 值 。如果N是状态变量而不是属性,则存在两个差异:在状态事实而不是成员 事 实 中 找 到 N , 并 且 规 则 生 成 器 可 以 检 测 到 使 用 以 及 变 量 的unfined/holded状态所隐含的操作。在不匹配的情况下,规则生成器可以生成正确的规则并向用户发出警告。登克尔-米伦34从上面的讨论中,应该清楚如何为单个属性或状态变量的接收生成规则,这可以根据需要由“比较”运算符“?"限定接收函数项接收函数项recv([f(s,t)])要求代理能够对f(s,t)进行模式匹配。这意味着接收器对项的结构理解得从数学上讲,这体现在可接受性和可逆性的概念中。一种可能性是函数值可以由接收方从其自身的状态计算出来,并与消息中的函数值进行比较如果出现在消息项中的所有变量都有“compare”前缀,这是合适的结果是一个除了状态标签之外不改变任何东西的转换规则否则,函数必须反转。一个函数的可逆性在MuCAPSL中表示,就像在CAPSL中一样,通过一个特殊的公理。比如说,可逆(ped(pk(A),X),X,sk(A))说ped在其第二个参数X中是可逆的,如果代理可以计算解密密钥sk(A)。连接在两个参数中都是可逆的(有两个公理),其他函数(如哈希函数sha)没有被建模为可逆的,也没有可逆性公理。因此,sha(X)只有在期限可以从X的持有价值计算时才是可接收的。如果一个函数项如f(s,t)可以被代理人求逆以获得s或t,那么接收f(s,t)就简化为接收s或t或两者,如果可能的话。因此,如果sk(A)是可计算的,则ped(pk(A),X)仅当X是可接收的时才是可接收的,并且转换规则包括接收X的结果。像cat(X,Y)这样的项对X和Y都是可逆的,并且转换以从左到右的顺序反映了接收两者的递归累积效果数组和函数属性会导致特殊情况,因为它具有一个特殊的属性,即可以修改一个命名的复杂对象,同时只提供它的一个组件。在MuCAPSL中,数组引用表示为A[N],抽象语法为at(A,N),在公理意义上是不可逆的,因为整个数组A和(通常)索引N都不能从at(A,N)确定。这个术语也不是可计算的,因为它指的是一个新的值。(The旧值将被称为?A[N].)然而,这个术语应该被认为是可接收的,因为接收代理可以存储消息中给定的值放入适当的数组元素中。如果A是一个属性,则接收事件recv([at(A,N)])将检查N是否可计算,并生成如下规则成员(M,[. A....]),state(M,roleM,3,[...]),mmsg([V])−→成员(M,[.与(A,N,V)...]),state(M,roleM,4,[...])登克尔-米伦35其中mmsg中的V取代消息中的at(A,N),并通过替换给定索引处的一个元素来更新数组请注意,V是一个新的Field类型的虚拟变量如果A是一个状态变量,则不允许在(A,N)处接收事件,因为状态变量只能设置一次,而且必须是整个数组对象。还有一些其他的情况,我们没有空间在这里介绍,比如类似的函数属性处理4.7等式事件规则等式事件eqn(x,y)可以是测试或赋值,取决于左侧项x。等式的右边总是要进行可计算性测试。一般来说,等式事件eqn(x,y)是一个测试,以下例外情况将其解释为赋值:(i) eqn(X,t)其中X是未定义的状态变量(ii) eqn(X,t)其中X是属性(iii) eqn( at(A,i),t)其中A是Array类型的属性(或子类型)(iv) eqn( proj(A,L,N),B)其中A是Array类型的属性,B是Array类型的属性(v) eqn(F(x),y)其中F是函数属性(vi) eqn(con(x,y),z)或eqn(cat(x,y),z),它们得到特殊处理;见下文。测试被转换为规则,其中等式在规则的条件下,类似于上一节中的测试规则未定义状态变量或原子属性的赋值规则类似于上一节中接收事件的赋值规则唯一的区别是在规则的左侧没有消息事实,因为这些分配是内部状态转换。在左侧具有级联的等式事件产生两个新事件,即,在con的情况下的eqn(x,head(z))和eqn(y,tail(z)),以及在 cat 的 情况 下的eqn(x,first(z))和eqn(y,rest(z))。分别具有非原子属性A和F的事件eqn(at(A,i),t)、eqn(proj(A,L,N),B)和eqn(F(t),t,J)被解释为赋值。将项t分配给(A,i)处的数组元素的模型如下:规则:成员(M,[. A.]),state(M,.,n,[.])−→成员(M,[.其中(A,i,t).]),state(M,.,n+1,[...]).还检查i是否可由代理计算。该规则意味着我们用新的项t替换属性A中位置i处的旧值。对于事件eqn(proj(A,L,N),B),我们检查L和N是可计算的,并将原始数组A替换为新数组,该新数组是通过将原始数组A投影到两个子数组(子数组登克尔-米伦36−e1en不(c)Ce1en不(c)C从索引1到索引L1,以及从索引N+1到A末尾的子数组,然后将这些子数组与B连接起来。对应的规则是member(M,[.个... ]),state(M,.,n,[.] ])−→成员(M,[.一个J... ]),state(M,.,n +1,[.] ]),其中,AJ定义为acat(proj(A,1,pls(L,mns(1),B,proj(A,pls(i,1),size(A)。对于属性F,类似地处理事件eqn(F(t),tJ)我们的解决方案为函数符号引入了谓词更新,用于指示函数的值发生了变化。成员(M,[. F... ]),state(M,.,n,[.] ])−→成员(M,[. update(F,t,tJ). ]),state(M,.,n +1,[.] ])。但是,这是作弊,因为MuCAPSL中没有函数类型像F这样的函数符号没有类型,所以update不是一个真正的函数,因为它没有合法的签名。根据工具或分析技术的表达能力,必须在每个分析技术或工具的上下文中单独找到处理规则中更新谓词的方法4.8迭代循环规则解析器将迭代循环转换为dountil(events(e1,.,e k),c),其中序列e1,.,将执行事件的Ek,直到条件C变为真。DO-UNTIL事件中的问题是,其中一个事件ei可能在第一次循环执行期间设置先前未定义的状态变量,但随后同一事件是对后续执行中该变量的测试。为了处理这个问题,我们为循环创建两个状态序列,当状态变量在循环体中从unfined变为defined时。第一个序列只使用一次,第二个状态序列用于所有后续执行。该流程如图6所示。见图6。 具有未定义状态变量的规则生成器可以判断一个状态变量是否被定义为登克尔-米伦37在循环开始时保存所有状态变量的当前状态,并将其与第一次循环执行后的当前状态进行嵌套的DO-UNTILs可以递归处理。4.9中止角色指定的最简单形式是一系列发送和接收事件。在这些协议中,在给定的状态下只需要一种消息类型有时,希望允许组成员或领导者多播一个特殊的中断消息,告诉其他成员离开他们的当前状态并返回到某个稳定状态。组成员接收(或未能接收)此消息,并以某种特定于协议的方式对其进行操作这种行为在MuCAPSL中通过添加一个额外的Abort角色来表示,该角色接收之后是ABORT事件,然后是在假设执行此角色的组成员已终止其所有其他角色代理的情况下执行的任何其他协议特定事件如果组成员是单线程的,即它一次只能执行一个代理,而不是Abort角色代理,则重写规则版本会更简单。Abort角色中的ABORT事件被转换为如下规则:成员(M,[...]),state(M,Abort,1,[]),state(M,R,N,T)−→成员(M,[...]),state(M,Abort,2,[])其中M、R、N和T都是变量,因此任何单个非中止代理状态都将匹配并终止。单线程属性可以通过添加一个不可见的信号量属性,修改初始化transition(除了Abort角色)来测试和设置它,并终止transition来重置它来保证。在MuCAPSL中,给GroupMember子类型一个MUTEX属性会导致转换器添加信号量当单个组成员可以并发执行多个角色或任何角色的多个实例在这种情况下,信号量会记录代理的数量,中止角色会一直等到信号量达到零才继续。5计划为了使MuCAPSL对协议分析师有用,我们需要提供翻译工具和文档。我们目前正在完成MuCAPSL-MuCIL翻译器,该翻译器可以解析和键入Mu-CAPSL规范,并为协议生成MuCIL规则特别是,我们将添加一个优化阶段,以便在可能的情况下组合连续的MuCIL规则,就像我们为CIL所做的那样。登克尔-米伦38在不久的将来,我们将研究目标规范。MuCAPSL和MuCIL中需要形式化诸如“完美前向保密”和“前向/后向访问控制”之类的保密translator用于表示目标、执行场景和攻击者模型的能力将逐步扩展。验证和模型检测技术必须重新研究和扩展组通信协议。引用[1] G. Ateniese,M. Steiner和G. Tsudik.新的多方认证服务和密钥协商协议。IEEE Journal on Selected Areas in Communication,2000。[2] M. Baugher,T. Hardjono,H. Harney,andB. 维斯 组域 的解释。互联网草案,IETF,2001年。http://www.ietf.org/internet-drafts/draft-ietf-msec-gdoi-01.txt。[3] I. Cervesato,N. Durgin,P.
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- 京瓷TASKalfa系列维修手册:安全与操作指南
- 小波变换在视频压缩中的应用
- Microsoft OfficeXP详解:WordXP、ExcelXP和PowerPointXP
- 雀巢在线媒介投放策划:门户网站与广告效果分析
- 用友NC-V56供应链功能升级详解(84页)
- 计算机病毒与防御策略探索
- 企业网NAT技术实践:2022年部署互联网出口策略
- 软件测试面试必备:概念、原则与常见问题解析
- 2022年Windows IIS服务器内外网配置详解与Serv-U FTP服务器安装
- 中国联通:企业级ICT转型与创新实践
- C#图形图像编程深入解析:GDI+与多媒体应用
- Xilinx AXI Interconnect v2.1用户指南
- DIY编程电缆全攻略:接口类型与自制指南
- 电脑维护与硬盘数据恢复指南
- 计算机网络技术专业剖析:人才培养与改革
- 量化多因子指数增强策略:微观视角的实证分析
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功