没有合适的资源?快使用搜索试试~ 我知道了~
一理论计算机科学电子笔记121(2005)23-46www.elsevier.com/locate/entcs一种基于协调的安全协议验证Giacomo Baldi Andrea Bracciali Gianluigi FerrariEmilio TuostoDipartimento di Informatica,Via F. Buonarroti 2,56127比萨我说:{baldig,braccia,giangi,etuosto}@di. Unipi.it摘要寻求系统性质的形式化证明是形式化方法领域中最具挑战性的研究问题之一。它需要开发正式模型以及有效的验证技术。在本文中,我们描述了一个正式的方法来验证安全协议的基础上借用的思想,从开放系统的分析,其中应用程序与另一个动态地共享公共资源和服务,在一个不完全的信任的环境。该方法是支持SPASyA,一个工具的基础上,符号模型检查技术。关键词:形式化方法,形式化证明,安全协议,开放系统,符号模型检验1介绍软件应用正朝着开放式架构发展这种转变的关键方面是交互和动态在应用程序生命周期中的相关性开放系统的特征在于由独立的相互作用的组件组成,这些组件的配置可以随时间动态此外,系统架构可能只是部分可访问的,这既是因为它的动态性,也是因为它可能分布在不同的、不可控的域上。因此,相互作用的组件必须根据资源的动态供应和需求来协调它们的行为。此场景促进了服务环境的创建,1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2004.10.00624G. Baldi等人/理论计算机科学电子笔记121(2005)23通过动态绑定软件组件(先前已发布和检索),标准示例由Web服务技术提供[16]。组件和服务的架构设计的优点已经从几个不同的角度进行了研究,例如,活动组件的动态协调,被理解为“通过将活动片段粘合在一起来构建程序的过程”[ 11 ],或者关于“程序/系统组件的结构,它们的相互关系,以及随着时间的推移管理它们的设计和演变的原则和指导方针”的理论[ 18 ]。然而,尽管取得了许多进展,但将传统技术提升到开放系统中的服务集成的情况下,存在一系列公认的困难,这些困难迫使必须为成熟的架构设计开发的目标和技术升级,[30,3]。例如,额外的信息必须通过组件抽象来形式化,例如它们所基于的假设以及它们可以动态集成/绑定到系统中的条件。此外,这些动态系统需要一个可排序的验证技术来表达感兴趣的属性。在这里,我们提出了一种为安全协议量身定制的规范和验证方法。这一方法是受上文概述的更一般背景的启发。它基本上认为协议是一个开放系统,其中主体(例如,组件)可以在协议的多个运行会话中动态地加入和协调它们自己,其中恶意组件(以下称为入侵者)可以该方法由四个步骤组成:1)指定主体的行为和期望的属性,2)指定意图共享秘密的条件,3)指定入侵者的权力,根据其初始知识,4)自动验证协议执行是否满足或不满足属性。我们已经观察到,根据在先前迭代中获得的关于协议的实际且通常意外的行为的见解,步骤4)的结果可以被有效地利用到步骤2)、3)和4)。此外,步骤2)对动态连接和通信以及验证的有效性有影响。该方法依赖于[9,35]中介绍的正式框架。这包括一个演算的形式化描述的主体增强与语言机制的动态绑定,和一个特设的逻辑来表达的安全属性进行检查。该逻辑断言在协议中交换的数据G. Baldi等人/理论计算机科学电子笔记121(2005)2325此外,该方法由一个名为ASPASyA(通过符号模型检查方法进行自动安全协议分析在模型检查方法中,系统行为是用一个过渡系统来描述的,而必须验证的属性是用逻辑公式表示。公式的可能模型由状态的子集表示,例如对应于终止计算的那些状态。如果公式在所有重要状态下都“完全”成立,验证就成功了,否则就会产生反例。在模型检查的优点中,我们提醒效率(例如,优化的数据结构,如BDD),以及完全自动化的可能性,[14]。在我们的例子中,符号技术被用来克服一些内在的不完整性。 即,在状态空间生成期间,约束收集主体变量的可能值检查变量的赋值是否存在,以使公式整体方法和ASPASyA是非常人性化的交互式,因为问题及其形式化需要高度的专业知识,并允许验证过程被引导到感兴趣的属性。一旦协议及其属性当用户调整时,自动验证阶段开始。我们的框架自然允许改变入侵者的知识,状态空间的一部分被探索,以及在安全中非常频繁的隐式假设的具体化。用户可以适当地混合这三种输入,以检查协议的正确性,而无需修改协议规范或所需属性的规范。第2节和第3节分别回顾了安全协议和正式框架,以使读者了解上下文。验证方法见第4节。第5节报告了与文献中类似方法的比较。第6节载有一些结论性意见。2安全协议:概述安全协议旨在控制某些主体通过“公共通道”进行通信的场景中的相关信息的含义非常广泛,包括保密性、不可修改性或真实性。另一方面,通道是公共的:不可能避免交换的消息被入侵者访问、操纵或破坏。一般来说,安全协议的正式证明需要仔细定义协议所依赖的基本假设,它应该强制执行的安全属性,以及关于26G. Baldi等人/理论计算机科学电子笔记121(2005)23- -入侵者的能力。在下文中,我们简要回顾安全协议,参考[32,23]以获得更全面的介绍。密码学当消息m包含的信息可以直接从m获得时,消息m是明文,而当信息被“隐藏”在消息n中时,消息n是密码 给定密钥k,消息m以密码n=m k加密,并且原始信息只能通过密钥k的知识来检索。 在对称密码学中,相同的密钥k用于加密和解密,而在非对称密码学中,一个称为公钥的密钥用于加密,而互补私钥用于解密。任何主体都可以通过其公钥为另一个主体加密消息。后者是唯一可以用其私钥解密消息的人。此后,我们用I表示入侵者,用A、B、. ,A-和A+是主体A的私钥和公钥,λ-是λ的互补密钥(即, A+(如果λ = A−),A −(如果λ =A+),以及k(如果λ = k是对称密钥),m,n是消息m和n对。为了便于展示,我们假设关键字没有结构,也就是说,它们只是名称。结构化密钥增加了分析的复杂性,可以通过第3节中说明的处理结构化(因此数量有限)消息的相同符号技术来处理。 我们采用完美加密的标准工作假设:密码只能使用其解密密钥解密,即无论拥有多少信息,秘密都无法猜测。请注意,密钥的适当共享(也可以动态获得)是正确分配主体在协议执行中所扮演角色的基本特征。例如,密钥及其所有权可用于将身份归属于主体。方案规范安全协议可以被天真地认为是两个或多个主体之间的协议和属性的具体化机制有很多种下一个例子说明了一个协议的非正式规范作为一个通信步骤的列表。例2.1宽口青蛙(WMF)协议[10]旨在让A发送一个新的会话密钥kab,即在有限的时间间隔内使用的密钥通过可信服务器S发送给B。A和B共享两个私有G. Baldi等人/理论计算机科学电子笔记121(2005)2327密钥为S(分别为kas和kbs)。WMF协议的非正式规范是:(1) A→S:A,{ta,B,kab}kas(2) S→B:{ts,A,kab}kbsA向S发送其名称和具有B的名称的密码、会话密钥kab和S向B发送一个带有会话密钥kab、A的名字和一个新的随机数ts的密码。 nonce,它唯一关联到协议的会话,“近似”在原始公式中使用的时间戳(例如,S不会对A使用相同随机数的两个请求做出反应)。这使得表示更简单,而不需要显式的时间表示(然而,可以嵌入我们的方法中)。⬦请注意,上述描述并不是完整的规范。例如,它没有指定是否只有B和S必须知道kab和ts以及谁可以访问交换的消息。此外,由于入侵者可以适当地利用通过在协议的并发会话中扮演不同角色而获得的信息,因此必须正式指定不同会话的可能交织以及预期由协议强制执行的安全属性,如[10]安全属性协议已经被设计为强制执行许多安全属性。其中,我们考虑完整性(入侵者不能破坏交换的密码),保密性(入侵者不能知道交换的密码),和认证(入侵者不能让主体误解其合作伙伴在通信中的身份)。不同类型的安全属性,如公平性和不可否认性,将在未来的研究中得到解决。例2.2例2.1的WMF协议被期望强制执行kab的保密性:在每个会话中,它的值必须只有扮演A、B和S角色的主体才知道。此外,A对B的认证也是可取的:在B从S接收消息的每个会话中,A必须在同一会话中创建kab,并要求S将其转发给B。 ⬦入侵者模型我们采用(广泛接受的)Dolev-Yao入侵者模型[17]:入侵者是可以干扰所有通信的主体,例如通过隐藏,读取和修改消息,唯一的限制是完美加密假设。入侵者可以拥有一些私有数据,并且可以存储在协议的先前运行中交换的它可以被描述为28G. Baldi等人/理论计算机科学电子笔记121(2005)23PL它的获取的知识和形式化的执行环境,收集所有发送的消息,操纵和发送他们的主体等待一些输入。设N是一个可数的名称集,包含nonce和主名,K是一个对称和非对称密钥集然后,在本文中,集合M ={m,n,. 消息被定义为M::= N |K|{ M}|{M }M.Dolev-Yao入侵者的特征在于一组信息κ,入侵者的知识,以及可以通过分裂已知对、配对和加密已知信息以及解密密钥已知的已知密文而从中导出的信息,记为κ0m0的可判定性在[13]中已被证明用于私钥加密,在[9,35]中已被证明用于公钥加密例 2.3 给 定 κ={{A−1}k , {m}A+ , k} , 它 保 持 κ0{m}k 。 事 实 上 , 从κ0{A−1}k和κ0k,它遵循κ0A−1,这允许解密{m}A+得到m。最后,从κ0k,它遵循κ0 {m}k。3形式化安全协议该方法(在第4节中介绍)依赖于两个成分:加密交互模式演算(cIP)和协议逻辑(),在[9,35]中介绍。微积分允许我们正式指定协议的主体所表现出的行为值得注意的是,演算需要明确指出主体如何连接在一起,即它们如何共享密钥。它由IP演算的一个实例组成,IP演算是在[9]中引入的一种进程代数,用于描述开放系统中组件的行为组成该逻辑用于形式化协议预期执行的属性。它断言入侵者的知识,主体共享密钥和他们交换的数据的方式。此外,它允许对主实例进行量化,以便统一地表达关于多次运行协议的属性。cIP演算cIP演算是π演算家族中的一个名字传递演算[25]。它以[1]的风格扩展了具有密码原语的IP演算,并具有用于动态共享密钥的显式构造cIP处理A(X)[E]s代表读y以表示的主体A通过对变量X进行操作,并将其作为一个变量,以适应最佳的表达式E. 行为表达式由输入和输出G. Baldi等人/理论计算机科学电子笔记121(2005)2329在(d)或(d)(通过公共频道,其名称被省略)中的动作。数据d是变量可能出现的消息。开放变量是E中X发生的绑定器;适用于以下组规则:输入操作中的变量是绑定器,并表示为?x(我们假设输出动作不包含绑定器,输入动作包含每个变量的至多一个绑定器)。因此,变量可以在执行通信动作时实例化,或者在协议执行中主体动态连接到其伙伴时实例化请注意,在[8]中引入了开放变量作为表示资源共享的通用机制,例如:通信通道,其在动态连接在一起的部件之间在本文中,这种机制已经专门用于共享密钥,允许主体在协议运行中进行交互。名称和变量是语法上不同的实体,前者是常量项,后者是占位符,可以用项替换或适时地重命名。主体必须是封闭的:变量必须由输入操作或开放变量绑定示例3.1WMF协议的原则在cIP中形式化如下:一(x,xas)[out(A,{ta,x,kab}xas)]B(zbs)[in({?s,?x,?w}zbs)]S(u,ya,v,yb)[in(u,{?t,v,?r}ya).out({ts,u,r}yb)]。主体A打算与伙伴商定会话密钥,当A将加入协议运行时,伙伴的身份将被分配给其开放变量x,其中S和B可能已经存在。 A的开放变量xas和S的开放变量ya通过使用相同的对称密钥实例化,允许两个主体分享一把钥匙类似地,yb和zbs对S和B起相同的作用。最后,服务器S得到u和v中A和B的身份。⬦为了对多次运行进行建模,可以在主体实例中复制主体,通过用一个独特的自然数索引E中的所有变量(开放或非开放)和所有名称来获得主体实例,例如。 A1(x1,xas1)[ou t(A1,{ta1,x1,kab1}x as1)]。具有不同索引的主实例被区分,即,A1A3。在上下文中,即可以由其他实例动态加入的一组运行实例,引起密钥的进一步共享,如下所述。请注意,实际的共享是由一个从开放变量到键的映射来确定的。事实上,验证任务并不是为了确定设C是一个(运行的)上下文,有n-1个主体实例,并且ov(C)它的前边缘的操作变量的值。GivenAn(X<$n)[En]aprincipal30G. Baldi等人/理论计算机科学电子笔记121(2005)23我C[C−›→ C Cκ0m:地面s.t. dγ m(in)[在(d)中。Ei]<$C,χ,κ<$−→<$$>(X<$i)[Eiγ]<$C,χγ,κ<$(out)(Xi)[ou t(m). Ei]<$C,χ,κ<$− <$→<$(X<$i)[EiJ]<$C,χ,κ<$m<$CJ=join(Ai,γ,C) A(X) [E]inew<$C,χ,κ<$− <$$> →<$CJ,χγ, κ<${Ai,A+}<$Fig. 1. 上下文归约语义(加入)在stance中,并且γ是从ov()Xn到kys的第0个集合的部分映射,则连接操作被定义为:join(An,γ,C)=(X<$n−dom(γ))[Enγ]<$(Y)[E']∈C(Y−dom(γ))[EJγ].直观地说,join(An,γ,C)是通过根据映射γ将主实例An连接到而获得的上下文。开放变量必须根据它们的用法(在主体的语法中是显式的)分配给对称或非对称密钥。一旦分配,它们就不再开放。注意,在连接操作之后,上下文可以保持打开,即它可以包含用于稍后连接操作的打开变量。语境语义学上下文的操作语义是根据与配置χ,κ相关的标记转换系统(LTS)给出的,其中是在上下文中,X是由于通信和连接执行而引起的绑定,并且κ是truderknor。在图1中记录了规定−<$→的规则。如果可以从κ,rule(in)导出适当匹配的消息m,则主体可以输入数据。主体的所有输出都记录在κ,rule(out)中,以及加入上下文的每个主体的名称和公钥,rule(join)。cIP的语义模型形式化了Dolev-Yao入侵者模型。所有的通信都发生在入侵者身上:它记录所有交换的消息和加入上下文的主体实例的名称,并将从其知识派生的消息发送给主体。在最简单的情况下,它只转发消息,允许协议的预期执行发生。示例3.2WMF协议的上下文的配置,由G. Baldi等人/理论计算机科学电子笔记121(2005)2331>33313K›→kzbs1,xas3›→k2B()[in({?s,?x,?w})]x3,v2›→B13请注意,即使不是有意的,这个上下文也模拟了A3、S2和B1共享相同密钥k的情况。一个可能的终止跟踪导致最终入侵者的知识κ={A3,{ta3,B1,kab3}k,{ts2,A3,kab3}k},和映射γ1=γ0{ta3,kab3,ta3,A3,kab3/t,r,s,x,w},这是当密码组{ta3,B1,kab3}k被环境检测到B1(匹配成立)时发生的。 ⬦cIP演算提供了用协议主体的新实例统一扩展上下文的可能性。它的意思是这种语言学机制使我们能够确定哪些实例起源于协议执行过程中使用的名称,以及区分扮演相同角色的不同主体。这里有几点值得一提连接不是演算的运算符 主体连接在一起的方式,即最初如何共享密钥,通常是预先给定的。由于这对于协议验证的目标是决定性的,因此它已经在语义级别上进行了描述,从而正式描述了新主体加入正在运行的协议的后果正如我们将在第4节中讨论的那样,这也为我们的方法提供了一种有效的手段来控制验证实验的条件,并将重点放在那些对我们想要证明的属性更重要的秘密的初始共享上。密码学加密和解密通过匹配的概念(规则(in))嵌入到通信中。这种语言选择与其他一些方法共享,如[1,6],然而,它们采用不同的验证方法。输入动作必须声明他们打算用来接收和解密密码的密钥,并且只有当输入和输出消息匹配时,即{m}λ<${n}λ−,其中m<$n,通信才能发生。这保证了密钥的正确使用。例如,{m}k›→A32G. Baldi等人/理论计算机科学电子笔记121(2005)23--PL匹配({?x}k),因为对称密钥k解密密码,而{m}k1和{?x}k2将不匹配,其中k1/= k2。在通信之后,用密码{m}k的内容m实例化变量x。符号分析。cIP的语义在消息m的选择中包含不完整性的来源,rule(in),在可以从k作为主体的输入消息导出的无限多个消息中(参见[13]关于协议分析中的不完整性)。这导致了一个无限状态空间问题,我们已经通过采用符号方法解决了这个问题;这种方法包括延迟消息的选择,并用当前κ的有限表示来注释输入变量,因此,可以从它导出所有消息。我们表示这一点,对于输入变量x,通过符号变量x(κ),因为这是k0m 符号上匹配的消息可以在结构上组合在符号变量和标准消息方面未来的演变上下文可以进一步指定x(k)的值,例如当它被用来代替键时。符号变量允许规则(in)的存在性量化器被可能的符号消息的有限集合的构造性生成所取代,其工作方式类似于统一。即使在一般情况下,一个变量可以有更多的赋值,它们的数量也是有限的(并且通常受到目前为止添加到知识中的消息数量的限制例如,考虑输入消息?xλ。匹配消息可以通过知道适当的密钥λ-1,或者通过每个合适的匹配消息,如{m}λ-1。这样的消息可能属于最初的知识或在以前的交流中获得,因此数量有限。一个符号迹表示所有具体的迹,通过实例化它的符号变量与可从相关知识导出的消息而获得。证明符号和具体迹线的对应性[9,35]保证了符号验证的正确性,这也与其他优化一起影响该方法的有效性。PL逻辑安全属性通过逻辑(协议逻辑)来表示,该逻辑对可从κ导出的消息、变量所假定的值以及它们与生成和通信它们的主体的关系进行断言。在我们的方法中,完整性被解读为固定一些值的可能性,推广了[1]中引入的方法,保密性被解读为κ中包含或不包含的值,并且通过主体变量之间的关系进行认证G. Baldi等人/理论计算机科学电子笔记121(2005)2333∀∈ ¬ ∧/∈设δ、σ是消息、变量或入侵者I的名称,PL的φ,φ是δ∈κ|δ=σ|A.i:φ|¬φ|φ=0,其中,被解读为消息的可推导性,=,,是相等,否定和合取,A.i:φ允许对实例进行量化:i是一个在实例索引范围内的变量,可能在φ中作为索引出现。例3.3WMF协议应该满足的一个性质是会话密钥kab的保密性,除非它是针对I:A.i:xi/=I→kabi/∈κ,即⬦公式的真实性取决于过去的计算,即取决于κ和赋值χ,因此公式是根据由终止迹产生的对κ,γ组成的模型来检查的,因为这些是公式必须成立的感兴趣的状态符号κ| = χφ意味着在变量分配χ下,κ是公式φ的模型。关系|=(对于封闭式公式)由以下演绎规则定义(以及省略的明显的一个):xiχ=δχ κ|=χ xi = δ(=)κ0δχκ|=χδ∈ κ(∈)κ |=χφκ|=χ<$φ(€)κ|=所有A j的χφ{j/i}:κ0Ajκ|=χA.i:φ(二)。索引量化的范围是参与会话的有限数量的实例,其名称以κ(k)表示。直觉,使用|=在规则(<$)的前提中,意图证明φ是不可能的,这是因为在每个规则中,前提中的公式总是“结构上小于”结论中的公式(因此递归定义|(定义明确)。最后,将逻辑提升到符号变量作为赋值的结果出现在公式中的情况是容易的,将符号变量视为相关κ的成员条件。例3.4再次考虑WMF协议,我们可能希望验证以其朴素形式写成的保密属性,如φ = A.i:kab iκ:“A生成的会话密钥不被入侵者知道”。让我们假设,我们想让我扮演一个正常的主要角色,即B。在这种情况下,34G. Baldi等人/理论计算机科学电子笔记121(2005)23/∈1,ya2›→kas一添加一个密钥就足够了,比如说ksi到κ。让我们考虑一下S与I共享ksi,并且A想与I通话:的1 ()[out(A1,{ta1, I,kab1}kas)]S2()[in(A 1,{?t 2,I,?r2}k).out({ts 2,A 1,r 2}ksi)]其中,初始时,γ0=yb2›→ksi第1卷,第2 节›→I很容易证实,κ1={A1,S2, I,ksi,{Ta, I,kab}kas,{Ts,A,kab}ksi}和γ={xas1,ya2<$$> →kas,yb2<$$> →ksi,x1,v2<$$> →I,t2<$$> →ta1,r2<$<$→kab1},这是由上下文的终止跟踪产生的,不是φ的模型。发现这种在这种情况下,公式的前提是假的,并且跟踪不被认为是攻击。这种逻辑的表现力将有助于将核查重点放在“预期”攻击类别上⬦4核查方法我们的验证允许用户直接控制和管理许多方面验证过程。该方法包括四个步骤:(i) 最初,协议的非正式描述在cIP中被具体化,并且相应地,安全性质通过PL公式被形式化(ii) 给出了一个指定主体连接上的不变量的公式;这样一个公式,以下称为连接公式,说明了连接操作必须满足的开放变量上的约束,以便显式指定秘密的共享;(iii) 根据验证者授予入侵者的权力来设置入侵者知识,例如可以将在协议的先前运行中获取的公钥/私钥或消息添加到κ;(iv) 核查的自动阶段开始。调用SPASyA,并根据结果迭代步骤2和3。G. Baldi等人/理论计算机科学电子笔记121(2005)2335关于步骤1,协议叙述的形式化不能自动化,但它需要专业知识,例如指定cIP主体的开放变量。然而,可以给出一些经验法则:• 发起者通常需要一个开放变量来连接到响应者;• 如果伙伴的身份是在通信中获得的,则不需要关于伙伴身份的开放变量(除非需要核查身份• 当主体必须与服务器交互以便共享密钥时,开放变量可能是必需的。此外,安全属性的形式化是一项复杂的任务,需要经验。逻辑PL可以形式化:• 当检查保密属性时,入侵者不可能知道协议运行中的特定数据d• 不同主体的变量之间的关系,必须在每次运行时保持,当更复杂的属性,如身份验证,必须验证。在步骤2中,指定连接公式,以约束允许的连接和主体之间的密钥共享。例如,考虑例3.1中描述的WMF协议的主体A和S;如果S是可信的,我们可能只对验证协议的执行感兴趣,其中A(的任何实例)与S(的相应实例)正确地共享秘密密钥。这可以通过以下连接公式表示φWMF<$A.i:<$S.j:xasi=yaj<$xasi/∈κ,这直观地表明入侵者不能像服务器那样工作。连接公式,连同连接操作,是我们的方法的一个显着特点。每当执行连接操作时,都会检查连接公式,如果连接公式不成立,则中止对该跟踪的分析。此外,公式构成了一个正式的设备,用户可以利用修剪状态空间。实际上,通过调整连接公式,用户可以正式地陈述通常隐含在协议的非正式表示中的假设(例如,WMF协议中的服务器的可信度)。验证会议的结果有时会显示,协议中的一些假设没有正确地形式化。通过完善关于主要连接的假设,可以过滤掉虚假攻击。基本上,可以利用连接公式将验证集中在验证者感兴趣的那些状态连接操作和连接公式也是一种协调机制,用于对36G. Baldi等人/理论计算机科学电子笔记121(2005)23→(4)B→A:{na,B,k}kas,{Tb,A,k}kbb,nc,{na}kab>K(1) A→B:na,A(2) B S:na,A,nb,BAB ABABAB9>=(3) S→B: {nb,A,k}kbs,{na,B,k}kas会话密钥交换(5) A→B:{nc}kab(6) A→B:ma,{Tb,A,kab}bb(7) B→A:mb,{ma}kab(8) A→B:{mb}kab图二. KSL的叙述>;9>=>>的;重复认证一个开放系统,其中组件通过连接到其他参与者来动态访问运行上下文。例如,考虑到Web服务,组件就是服务,新服务是通过正确连接现有组件构建在目前的实践中,这是由程序员静态完成的;而联接操作和连接公式将允许程序员指定其组件的动态连接上的约束。步骤3指定入侵者的初始知识,以便在较弱的条件下检查协议。这种知识主要用于两个目的:(i)让入侵者知道一些秘密(例如,泄露的密钥),从而增强其攻击能力,例如测试协议的鲁棒性,以及(ii)让入侵者知道一些关于主体之间过去的交互(在先前会话中交换的密码)。 后者在发现重放攻击时特别有用,其中入侵者利用了先前会话中出现的消息。可以迭代步骤2、3和4,以便根据在先前迭代中获得的结果来调整连接条件和初始知识。KSL协议为了解释该方法,我们将其应用于KSL协议的分析[19](对KSL协议的简化[20])。KSL的目标是在利用可信服务器的主体A和主体B之间进行重复身份验证S.该协议分为两个部分:一个初始的消息交换,建立一个主体之间的会话密钥,其次是重复认证部分。通过由B为A生成的过期票据来执行重复认证。在票证有效(未过期)之前,A可以向B重新验证自己,而无需向B请求新的会话密钥。S. KSL的非正式规格见图2。在线留言(1)是密钥交换部分,而消息(6- 8)是重复的au-G. Baldi等人/理论计算机科学电子笔记121(2005)2337------S(a,ak,b,bk)[in(?cna,a,?CNB,b)。out({cnb,a,kab}bk,{cna,b,kab}ak)]A(b,sk)[out(na,A). 在({na,b,?r}sk,?tkb,?bn,{na}r)。out({bn}r)]B(sk)[in(?cn,?u)。 out(cn,u,nb,B). 在({nb,u,?r}sk,?tka)。out(tka,{nt,u,r}kbb,nc,{cn}r). in({nc}r)]图三. KSL校长认证。也就是说,A和B之间的每个进一步的交互从消息(6)开始。服务器S与每个主体共享一个对称密钥。发起方A生成随机数na,并将其发送给B。然后B向S请求新的会话密钥,S生成kab,并在(3)中,将会话密钥加密为两个密码{nb,A,kab}kbs和{na,B,kab}kassentoB. 没有人会把它隐含在假设k为(相应地,kbs)仅由S和A(分别为B)。在解密nb,A,kabkbs之后,B假设kab是由S生成的新鲜会话密钥,并且意味着与A共享(kab的新鲜度由随机数nb强制执行)。消息(4)是相当复杂和关键的;B向A发送消息,AB(i)密码{na,B,k}k为 由S在消息(3)上生成,(二)“票”Tb,A,k abkbb,(iii)一个新的随机数nc和(iv)随机数na用KAB加密。票据是一个用密钥kbb加密的密码,只有B知道,并将在KSL的第二部分中使用;除了A的身份,它还包含一个通用的时间戳1和会话密钥,以便B可以检查票据的有效性。随机数nc将用于向B证明A确实要求会话密钥kab,而生成密码nakab以向A证明B已经获得kab。消息(5)关闭第一部分KSL:A发送回用kab加密的nc,这样B就被授权A获得了会话密钥。主体A知道kab和B发出的票据,可以重新验证自己执行消息(6-8)。在(6)中,B接收随机数ma和B先前为A生成的票据。如果票据是有效的,则B向A发送用kab加密的ma以及用于确保消息(8)中A的身份的新的随机数mbKSL我们方法的第一步规定提供协议的每个角色的cIP形式化和感兴趣的属性的形式化1通用时间戳报告B的本地时钟的当前时间,生命周期的指示和“epoch”标识符,我们参考[27]中与时间戳相关的问题。38G. Baldi等人/理论计算机科学电子笔记121(2005)23÷我们首先描述协议的第一阶段,即消息(1 - 5),其原理在图3中报告。稍后,我们将根据验证会话描述协议的其余部分。这使我们能够专注于这两个阶段的主要特征,并展示了该方法如何利用验证背后的直觉来完成。重要的是要指出开放变量所起的作用。 主要S具有变量a和b,分别表示发起者和响应者的身份。服务器还需要另外两个变量ak和bk,它们分别用于存储S与A和B类似地,A和B使用sk来存储它们与S共享的密钥。请注意,变量在不同的主体中是不同的。KSL试图实现重复的相互认证;非正式地说,这意味着每次B(连接到S)终止协议的运行,认为已经与A(连接到S)进行了交互,那么A最近与B执行了会话,A实际上是通信中的合作伙伴,反之亦然。下面的PL公式KSL形式化了KSL协议的A到BB. l:是的。i:A。j:(bi=Blul=Aj bj=Bl →(cnai=najcnbi=nblrj=kabirl=kabicnl=naj (l=bnj)公 式 BKSL 表 明 任 何 实 例 B1 都 被 附 加 到 服 务 器 模 板 S1 的 实 例(bi=B1)。此外,如果B1是作为发起者连接到S1(ai = Aj)的实例Aj(ul= Aj)的伙伴,则应该发生“正确的”数据交换,只要Aj旨在向B1(bj = B1)认证其自身。 如果:(i)服务器接收到正确的随机数(cnb i= nb i和cna i= na j),(ii)Bl和Aj两者获得由Si生成的相同会话密钥(r j= kab i和r l= kab i),则数据交换的正确性成立,(iii)由Bl接收到的随机数全部由Aj生成(nc l= bn j和cna i= na j)。我们方法的第二步需要指定一个连接公式φKSL,声明服务器与发起者和响应者共享私钥。在PL中,其呈现如下:φKSLS。i:A。j:(ai=Aj→aki=skj)B. l:(bi=Bl→bki=skl)。换句话说,需要对于每个Si(服务器的实例)存在连接的发起者Aj,使得aki和skj被分配给相同的值:Si和Aj共享相同的密钥。这也对发起者的身份和保存共享密钥的服务器的开放变量之间的对应关系进行了(TheφKSL的其余部分表示响应器的相同属性注意G. Baldi等人/理论计算机科学电子笔记121(2005)23393例以下基团4个实例加入真10240580–––φKSL55012013218四点二十一分0φJKSL59034015723五点零七分0表1KSL第一阶段的攻击报告φKSL排除了A的一个实例可以作为响应者。为了允许这种可能性,我们可以考虑以下公式:φJKSLS。i:A。j:(ai=Aj→aki=skj<$bi=Aj→bki=skj)<$B. l:(bi=Bl→bki=sklai=Bl→aki=skl),然而,我们坚持使用更简单的φKSL进行验证。表1报告了KSL第一阶段的验证结果。我们通过改变实例的数量和可能的连接公式来检查各种场景。 尽管在这个阶段没有发现攻击,但值得注意的是连接公式如何帮助减少状态空间的大小例如,在三个主体实例的情况下,与使用φKSL或φJKSL之一的情况相比,完全无约束设置(第一行)中的状态数量非常大这一点在考虑四种情况时更为明显;事实上,使用平凡连接公式进行验证需要不合理的时间(在2.4MHz Athlon处理器上需要一天),而φKSL和φJKSL都在几分钟内终止。由于协议的第一阶段不会产生任何攻击,因此我们通过关注协议的第二阶段来执行KSL的验证,即,在消息(6- 8)。我们考虑纠正会话密钥交换阶段,并检查是否可以在重复认证阶段建立攻击。在此假设下,在KSL的第5条消息结束时,我们可以安全地假设,• 由于入侵者知道会话的初始五条消息,因此票证处于初始知识中(在其他数据中);• A(相应地)B)认为B(resp. A)正在作为响应者运行会话协议(分别为发起人);• A和B在当前会话中共享一个密钥• 密钥是有效的,因为B颁发了证书。由于我们假设A和B与S的交互是可信的,40G. Baldi等人/理论计算机科学电子笔记121(2005)232 实例3 实例4个实例加入/了解真,κ01040.69038781.538–––true,kāo1040.85038781.898130870两点二十七分16φ<$KSL,κ0710.64032201.506–––φ<$KSL,κ<$0710.80032201.85652692一分十六秒12表2KSL重复认证部分在不妥协的情况下,我们只能考虑A和B的主体:A(b,sk,tk)[out(nma,{b,A,sk}tk).in(?mb,{nma}sk).out({mb}sk)]B(a,s k,t k)[in(?ma,{B,a,s k}tk).out(nmb,{ma}sk).in({nmb}sk)].注意,A在第一阶段获得的票的共享在这里通过使用A和B的开放变量tk来建模。实际上,A从不使用tk作为解密密钥(即,在输入动作中),因为加密票据的密钥只有B知道。事实上,A只在第一个输出中使用tk来将票据传递给B。关于A和B共享的秘密的假设,包括在协议的前一阶段中获得的数据的正确共享,通过以下连接公式形式化:φ<$KSL=φB。l:A。j:tkj=tkl→bj=altkj=skl,说明如果存在A和B共享票据的两个实例,则y_ai_t在e上进行通信(b_j=al)并且发送会话(sk_j= sk_l)。要检查的身份验证公式可以类似于对KSL所做的说明,但它比KSL简单,因为我们可以忽略与服务器的通信:我是KSLB。l:A。j:bj=Blal=Aj→mal=nmaj nmbj=nmbl.由于使用两个实例验证KSL不会产生任何攻击(如表2所示),因此我们描述了三个参与者的案例。根据我们方法论的第三步,我们必须明确入侵者的知识。我们已经指出,入侵者知道在第一阶段交换的那些消息。 因此,初始知识κ0包含以下消息:I,B1,B2,A3,即加入会话的实例,以及{B1,A3,sk1}tk1,即B1为A3发出的票证。这些-数据包含变量(例如, sk1,tk1,.. . ),它将在G. Baldi等人/理论计算机科学电子笔记121(2005)2341一通过连接操作生成初始上下文我们可以把κ0看作是一个知识的模板,它可以根据连接操作指定一组消息。 在这种情况下,SPASyA发现(和报告) 以下攻击(除其他外):(1)A3→I:nma 3,{B 2,A3,ks}kb 2(2)I→B2:nma 3,{ B2, A3,ks}kb 2(3)B2→I:nmb 2,{nma 3}ks(4)I→B1:nmb 2,{ B1, A3,ks}kb 1(5) B1→I:nmb1,{nmb2}ks(6) I→B2:{nmb2}ks(7) I→A3:nmb 1,{nma 3}ks(8) A3→I:{nmb1}ks(9) I→B1:{nmb1}ks在消息(1<$3)中,A3和B2开始认证阶段;由于κ0中的票据,通信是可能的。在消息(4- 5)中,扮演A3角色的I使用B1用ks加密nmb2。在这一点上,我可以匹配B2请求的输入数据,并且随后可以扮演B2的角色,使用A3作为加密oracle来获得{nmb1}ks,这是结束与B1一起运行的协议所需的。因此,入侵者能够让B1相信他正在与A3交互,而他正在与I交互,这违反了身份验证属性。值得注意的是,攻击是可能的,因为有一个跟踪是从一个上下文开始的,在该上下文中,连接为两个不同的票(一个在κ0中,另一个由(1)中的A3注意到没有任何东西阻止他的邻居KSL,也没有任何东西阻止KSL;因此,通过施加这一条件(实际上,这是KSL的非正式规范所要求的)进行验证。然而,这是在[21]中报告的KSL分析中强加的假设,其中首次报告了相同的攻击;无论如何,该分析的动机是考虑协议在存在较弱假设(两个包含相同会话密钥的票据)的情况下的鲁棒性,这些假设也是现实的。作为最后的尝试,我们
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 5
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
最新资源
- C++标准程序库:权威指南
- Java解惑:奇数判断误区与改进方法
- C++编程必读:20种设计模式详解与实战
- LM3S8962微控制器数据手册
- 51单片机C语言实战教程:从入门到精通
- Spring3.0权威指南:JavaEE6实战
- Win32多线程程序设计详解
- Lucene2.9.1开发全攻略:从环境配置到索引创建
- 内存虚拟硬盘技术:提升电脑速度的秘密武器
- Java操作数据库:保存与显示图片到数据库及页面
- ISO14001:2004环境管理体系要求详解
- ShopExV4.8二次开发详解
- 企业形象与产品推广一站式网站建设技术方案揭秘
- Shopex二次开发:触发器与控制器重定向技术详解
- FPGA开发实战指南:创新设计与进阶技巧
- ShopExV4.8二次开发入门:解决升级问题与功能扩展
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功