μCRL语言对双边密钥交换安全协议的分析及验证

理论计算机科学电子笔记139（2005）49-90www.elsevier.com/locate/entcs分析BKE安全协议，μCRLStefan Bloma，1，2 Jan Friso Grootea，b，3SjoukeMauwa，b，4 AlexanderSerebrenikb，5一CWI，阿姆斯特丹，邮政编码Box 94079，1090 GB Amsterdam，荷兰B软件质量实验室（LaQuSo），计算机科学埃因霍温理工大学P.O. Box 513，5600 MB埃因霍温，荷兰摘要μCRL语言及其相应的工具集为分布式系统的验证提供了强大的方法。我们证明了它的使用，将其应用到著名的双边密钥交换安全协议。关键词：安全协议验证，μCRL，模型检测1引言用于分析通信过程的当代工具基本上都基于显式状态空间表示[6，9，11，17，26，30]。在某些情况下，特定的数据类型具有显式编码（例如，时间[9]），在其他情况下，压缩技术已被应用于状态的表示[6，17]。这些工具已经成熟到可以在相对较小的过程描述中发现系统错误的程度应用工具1本研究的一部分由荷兰BSIK/BRICKS项目资助2 电子邮件：Stefan. cwi.nl3 电子邮件：J.F. tue.nl4 电子邮件：S. tue.nl5电子邮件：A. tue.nl1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.00550S. Blom等人理论计算机科学电子笔记139（2005）49更大的和现实生活中的系统是一个持续的战斗与所谓的状态空间爆炸问题。其本质是，基本上每一个被分析的通信过程都有比这些工具所能表示的更多的状态其结果是，行为分析必须限制在有限的通信场景下的小实例。通过扩展这种基于状态的方法，可以预期会取得稳步进展计算机变得更大更快，更好的状态空间压缩和分析技术将被发明出来。然而，我们相信，为了向前迈出实质性的一步，必须有更根本的发展我们相信，使用μCRL工具集[12]，我们通过引入线性过程的概念使用[32]中描述的技术，可以将所有μCRL过程转换为线性形式。这样做的工具能够为由数百个并行进程组成的系统执行此操作。线性过程允许容易自动化的各种操作。关键的一点是：（a）人类的聪明才智可以决定必须应用哪些操作在工程数学中可以找到非常相似的情况，Maple，Mathlab和Mathematica已经成为交互式操作大型数学公式的工具。我们认为，一套工具必须以健全的理论框架为基础。对于μCRL，[13]中给出了最新技术在本文中，我们将展示μCRL在一个流行的应用领域的使用，即。安全协议的验证形式化方法在安全协议分析中的重要性在开发正确的安全协议是众所周知的困难这一事实中显而易见已经发现许多这是因为很难预测入侵者可以用来破坏安全性的所有可能的攻击Dolev-Yao入侵者模型（见[10]）是最广泛接受的入侵者建模方法在这个模型中，入侵者完全控制网络。他可以拦截消息，并从代理发送的消息中推断出所有信息，然后构造新的消息入侵者知识的增长，以及入侵者可以构建的不同消息的数量，是系统可能行为数量呈指数增长的主要原因模型检验和定理证明是验证安全协议最常用的形式化方法。定理证明需要开发用于安全属性的证明逻辑（参见例如， [4]），并且通常需要用户交互。模型检查（参见[18]）支持状态空间爆炸S. Blom等人理论计算机科学电子笔记139（2005）4951问题，但可以自动完成。我们将通过分析双边密钥交换（BKE，见[5]）协议的变体来展示μCRL模型检查器的强大状态约简技术该协议的目的是在两个代理之间建立一个新的加密密钥，该密钥应该对可能的入侵者保密为了使我们的重点放在安全协议的建模上，而不是安全属性的建模上，我们将只集中在保密要求上认证属性的扩展，例如协议（参见例如[19]这超出了本文的范围然而，我们相信μCRL中的形式化可以很容易地遵循[28]中的处理。安全协议的形式化验证是一个研究课题已经有二十多年了。Burrows，Abadi和Needham开发了一种模态逻辑，即所谓的BAN逻辑[4]，它允许对安全协议中交互的代理的知识进行推理这种方法比目前大多数验证方法所认可的入侵模型BAN逻辑的开创性工作促进了许多更复杂方法的发展，这些方法基于逻辑、进程代数、操作语义等。一种众所周知的进程代数方法基于CSP，并利用模型检查工具FDR和Casper编译器[28]。该工具使用过程包含，而我们的方法使用互模拟来表达过程属性。另一个被广泛应用于安全协议的通用模型检查工具是Murtool [25]。串空间方法[31]提供了一个比进程代数方法更抽象它使用执行事件的偏序来描述一组运行某种安全协议的代理安全性能通过分析所谓的穿透线得到证明这种方法与保罗-森[27]的归纳方法有许多共同点 后者使用定理证明器Isabelle进行安全协议的计算机辅助验证。另一种基于定理证明的方法可以在Athena工具中找到（参见[29]）。Brutus工具[7]和我们的工具一样，是一个模型检查器。 Brutus专门针对安全协议，基于特定的偏序约简，而μ CRL工具集是一个工具链，其中一个工具基于更一般的偏序约简技术（连续消除）。Millen和Shmatikov [23]设计了一种算法来分析正在执行的安全协议的所有可能状态，同时推迟变量的实例化并定义每个变量的约束。这种技术提供了一个显着减少的状态空间。NRLPro- tocol Analyzer [22]是一个模型检查器，它试图通过从不安全状态向后工作来定位安全漏洞本文的结构如下。在第2节中，我们将解释μCRL52S. Blom等人理论计算机科学电子笔记139（2005）49语言及其工具集。双边密钥交换协议及其规范将在第3节中讨论。第4节讨论了对手的建模。优化是第5节的主题。最后，在第6节中对结果进行了评价。确认我们感谢Cas Cremers对BKE协议建模进行了富有成效的讨论。我们也感谢裁判们非常有用的评论。2μCRL中的短引物语言μCRL（micro Common Representation Language，微通用表示语言）[12，13]在1990年被定义。当时，人们已经认识到，进程代数是描述系统行为的一种非常合适的方法。然而，进程代数并没有将数据作为一等公民，而是以一种相当机会主义的方式对待它。例如，在[24]中，要传达的数据只能来自有限域（特别参见[24]中的第2.8节），数据作为过程参数使用无界过程变量处理，并且语言缺乏显式的数据定义机制。为了与过程行为规范语言（如PSF [21]和LOTOS [3]）平等地处理数据。语言μCRL为此增加了对数据和进程的完整和对称的公理化处理这些语言允许从无限域进行数据通信，具有更高阶的过程变量，而不是无界集合，并且包括适合于定义所有相关数据集的完整定义语言其结果是一种具有足够表达力的裸语言，具有精确定义的语义、基本公理、证明方法和全方位的分析工具。在本节中，我们将简要解释验证方法和工具背后的语言和主要思想对于更广泛的治疗，我们参考[13]。2.1数据语言基本上，μCRL由数据部分和过程部分组成。数据部分由非常简单的等式抽象数据类型构建。所有在规范中使用的数据排序都必须声明。排序可以通过以下方式声明：sort BoolNList这说明了三种类型。所有类型都不是空的。Bool排序是特殊的，因为它必须恰好有两个不同的元素，分别用t和S. Blom等人理论计算机科学电子笔记139（2005）4953F.这是因为在进程术语中的条件中使用了排序术语Bool注意，t和f的不同可以导致其他项也必须不同。如果假设t和u相等，则得出f=t的结论，那么t和u一定是不同的。这种技术是反证法的一种形式，是μCRL数据部分中唯一可用的技术，可以证明项必须是不同的。每个排序的构造函数可以声明如下：funct，f：→布尔0：→N成功：N →N我们让t表示真，f表示假。构造函数0表示零，succ表示自然数的后继函数。如果一个排序D有一个以D作为其目标排序的构造函数，那么该排序的所有元素都可以使用构造函数来表示。给定上面的声明，t和f表示所有布尔值，N的每个元素都可以写为succ（.） （succ（0）.. . ）），即应用零次或多次，应用succ为0。辅助函数可以使用关键字map来定义。例如，Bool排序的标准函数可以声明如下：地图Bool×Bool →Bool<$：Bool →Bool在文本的阐述中，我们使用符号，如和，并以正常的数学方式使用这些符号工具可以处理的语言μCRL假设所有这些函数都是用标准ASCII符号编写的，都是prefix。因此，项tu被写为辅助函数不会破坏排序的结构一个没有构造函数的定义域D原则上可以有任意数量（>0）的元素，甚至是不可数的。这意味着不可能用一个术语来表示这种类型的所有元素函数的性质可以由简单的无条件方程确定一个众所周知的布尔函数的特征如下所示varb：布尔REWtb=bfb=ftb=tfb=b54S. Blom等人理论计算机科学电子笔记139（2005）49t=ff=t使用关键字var声明变量将在方程中使用关键字rew来自动词rewrite，选择它是因为重写技术被认为是证明μCRL中数据项相等的方法。这个术语有点误导。尽管工具中大量使用了重写技术，但关键字rew之后的方程必须被视为一组简单的无序方程。它的意义不会改变，如果一个方程的左边和右边被交换，或者如果每个方程在rew部分的相对位置被改变。这基本上是所有关于μCRL的数据部分的知识。尽管它很简单，但这种语言已经证明自己完全适合于所有可能的数据类型的规范。它的简洁性有几个优点，即数据规范语言可以快速轻松地理解，并且为其构建工具相对容易，可以集中精力使工具非常有效。也有缺点，即必须为每个规范定义基本数据类型它引起的额外工作并不是真正的问题。真正的问题是缺乏标准化，也就是说，在理解一个过程的复杂性之前，首先必须研究为这个规范定义数据类型的特定方式。这也阻碍了关于数据类型的Meta知识的发展和专用工具的使用。2.2过程语言μCRL的进程语言基于ACP语言，通信进程代数[1]，这与其他进程规范语言非常相似，例如CCS，通信进程演算[24]。这些语言中最重要的概念之一是动作。动作是进程的原子事件，它指示与外部世界或另一个进程的通信。在最后一种情况下，这种通信同步发生，也称为交互。动作通常写为a、b、c，但也可以有更全面的名称，如超时、发送和接收。使用两个主要的操作符，即一个点的顺序组成和一个加号的替代组成，系统的行为可以表示。过程序列a·b·c表示这些过程具有强制性的一致性a、b和c。过程a·b+c·d表示可以在两者之间进行转换的过程动作a之后是动作b，或者动作c之后是动作d。S. Blom等人理论计算机科学电子笔记139（2005）4955两者之间的选择是由第一个动作发生时的环境做出的顺序组合运算符的约束力最强，如果从上下文中可以清楚地看出其含义，则通常可以省略使用替代复合算子可以描述不确定性过程。对于这种情况，a·b+a·c最初可以执行一个操作。但它是否能够做b或c的行动后，还不确定-病房表达非决定论是很有价值的。它允许抽象地描述过程，其实际行为取决于不能充分、简洁或方便地描述的因素一种特殊的作用，用τ表示。叫做内部作用。这是一个不能直接观察到的动作，例如，因为它发生在计算机内部，或者因为它代表了两个进程之间的通信，为了指示动作被屏蔽，可以使用隐藏运算符τI，其中I是动作的集合的公式sτ{a，c}（a·b·c）等于公式sτ·b·τ。 选项a和c是隐藏的。有一个特殊的过程称为不作为或死锁，记为δ。这是不能执行任何活动的进程。它用于几个目的。例如，如果一个进程表现为死锁，这通常表明进程之间的交互存在严重的错误。为了声明动作不能发生，使用了封装操作符H，其中H 的将s∈{a，c}（a·b·c）equalsδ·b·δ.并且由于eδ满足了概率方程，δ·x=δ，其值等于δ。这一部分是语言的另一部分。a·b·c·d的过程是指，a·b和c·dc可以按任意顺序执行（只要a在b之前，c在d之前）。这称为交错。一般来说，如果p和q是进程，则pq表示p的动作可以以交错方式与q的动作并发发生的进程使用通信声明可以指示操作如何通信。如果a，b，c是动作拉瓜|B = c表示两个并行进程中的动作a和b可以同步发生，结果称为c。因此，为了明确起见，过程abbehavesa·b+b·a+c。 在这种情况下，可以增强同步时钟，即，不希望在同步时钟中，动作a和b上面解释的封装操作符CNOH可以用来阻止动作a和b。更具体地说，<${a，b}（a<$b）表现为c。虽然我们还没有解释流程与数据的结合，但知道操作可以携带数据参数是很有用一个社区-56S. Blom等人理论计算机科学电子笔记139（2005）49只有在数据参数完全相同的情况下，操作之间才能发生转换此外，对于多方通信，通信声明必须是可交换的和关联的。[15]详细内容请参阅。为了指定迭代行为，使用过程方程。一个过程方程的形式X=a·X表示进程X可以执行操作a，然后再次表现为X。换句话说，进程X可以执行无限序列的动作。可以写出更复杂的方程。过程方程Y=a·Y·b+cc表示一个过程，它可以满足任意多个a当它表现出A的时候，A也会表现出方程Z=a·（b<$Z）特征在于可以连续地执行A和B的过程被执行的b的数量2.3流程与数据相结合μCRL的本质是数据和流程的结合。这归结为过程语言的四个扩展第一个扩展是动作可以有数据。必须声明操作，假设存在数据排序Bool和N，这可以如下完成法a：布尔值×Na、b：NC这里声明了三个动作。动作a必须携带两个Bool和N类的参数，或者一个N类的参数。动作b有一个N类参数，而动作c没有参数。第二个扩展是数据可以用于过程方程。换句话说，过程变量现在变成了高阶变量，这给语言带来了整个数学世界的复杂性然而，从实际的角度来看，这些方程类似于标准编程语言中的过程声明，并且它们的使用不会带来任何问题。数据只是简单地添加到过程变量。因此，一个简单的计数器可以描述如下：PRocCo un t（n：N）=up·Co un t（succ（n））第三个扩展是为了让数据与事件的流程保持因此，条件运算符then-if-else（用d表示）被添加到S. Blom等人理论计算机科学电子笔记139（2005）4957语言为了展示它的用途，我们可以将上面的计数器扩展为也向下计数。函数pred减去1。PRocCout（n：N）=up·Cout（succ（n））+down·Count（pred（n））an>0d δ这个过程有两个被加数，用+分隔。两个被加数都表示可以独立发生的条件的else分支处的δ表示如果n= 0，则在第二个被加数中不能执行任何操作最简单的方法是，在特定的情况下，如下所示n：Na（n）。 这表示在动作a（n）之间的选择，所有的;这是一个由a（0）+a（succ（0））+a（succ（succ（0）+· ··构成的简单算法。但是，使用二元运算符+不能表示选择在无限多的选择之间。这正是求和运算符的设计目的。作为一个例子，我们可以用一个set操作来扩展上面的计数器，它允许将计数器设置为任意值。procCount（n：N）=up·Count（succ（n））+dωwn·Count（pred（n））an>0dδ+m：Nset（m）·Count（m）观察求和运算符的作用类似于lambda演算中的λ，或逻辑中的量化器λ，λ除了一些很少使用的结构，我们已经看到了μCRL语言的所有语言一个有用的特性，还没有指出，是init关键字，使用它指示初始状态。对于计数器，这可以如下工作：init计数（0）2.4理论和工具μCRL工具集由许多工具组成我们将自己限制在那些用于转换和优化BKE协议的μCRL规范并生成状态空间的工具上。工具名称以斜体字表示。最重要的工具mcrl检查一个规范是否是一个格式良好的μCRL表达式。此外，它将规范转换为线性过程格式。从本质上讲，这种格式由一个数据参数向量（对流程状态进行编码）和一组条件-操作-结果规则组成。这些规则说明了在数据向量上的哪些条件下可以执行操作。规则的执行部分指示在执行操作时必须如何更新数据。58S. Blom等人理论计算机科学电子笔记139（2005）49只有单个数据参数d类型D由下式给出：ΣΣX（d：D）=i∈ I ei：Eiai（fi（d，ei））·X（gi（d，ei））ai（d，ei）dδ.Σ这里，I是一个有限索引集，第一个i∈I必须被看作是一个有限数量的被加数。第2.3节中的过程是线性过程分别为1、2和3个后缀。Ineachsummandthereecanbeasum运算符ei：Ei，操作ai，参数fi取决于d和ei，e i，e i ∈gi和条件Ci.线性过程可以有多个数据参数，每个被加数中有多个求和运算符，每个操作有多个参数线性过程格式不包含任何并行性。并行操作者可以被移走，而不会大大增加线性过程的规模。在[32]中，已经详细描述了任意μCRL过程到线性过程的转换一个线性过程的状态向量可以很大，并且可以包含无限数据类型的变量这意味着具有非常大的甚至在有限状态空间中的过程可以转换为线性形式。标准化的线性形式使定义和实施简化和分析工具以转换和分析过程变得容易这大大提高了过程分析例如，一个具有巨大或无限状态空间的线性过程可以首先转化为一个具有小的有限状态空间的线性过程因此，有限状态空间分析是一种可行的技术，否则将是不可能的。具体例子如下。工具mcrl生成一个扩展名为.tbf的文件，其中包含压缩格式的线性过程。可以使用一台打印机pp以可读格式查看线性过程。mcrl工具有很多选项。我们只解释表4中使用的那些。使用每个工具的-help标签可以很容易地找到其他选项这个参数表示在转换为线性形式时必须避免栈数据类型（详见[20]）。ag-nocluster表示具有相同操作的被加数不能转换为单个被加数。newstate表示约简工具被公式化为滤波器，可以通过标准输入（stdin）读取线性过程，并通过标准输出（stdout）提供结果示例见表4。这允许链接归约工具，而不必保存所有中间结果。在一系列减排措施中，有些减排手段必须使用不止一次，以最大限度地发挥可能的效果。其中一个简单但非常有用的工具叫做constelm。 它消除S. Blom等人理论计算机科学电子笔记139（2005）4959参数在任何过程中都是恒定的。 例如应用constelm到PRocX（n：N）=a（n）·X（n）初始化X（0）将标识n是始终具有值0的常数参数。因此，它将上面的线性过程简化为下面的强双相似线性过程procX=a（0）·X初始化X一个类似的工具parelm可以删除不影响系统性能的参数。例如，在以下定义procX（n：N）=a·X（succ（n））参数n对行为没有影响并且可以被去除。结果是双相似过程：procX=a·X这是一个最简单的例子，一个无限状态空间的过程被简化为一个有限状态空间的过程。工具parelm在研究不依赖于某些数据类型的进程属性时特别有用。工具rewr通过使用数据类型的方程重写线性过程中的数据项来工具rewr有许多选项，可以通过使用适当的标签来打开。例如，选项-case添加重写规则以移动case函数C（s，t1，. ，tn）到外部一个术语。case函数是一个选择器，即 C（s，t1，. ，tn）等于ti，如果s =i。我们不用于BKE安全协议但在其他地方非常有用的其他标记如下。BDD-prover调用一个prover，将术语转换为具有等式的BDD结构[15]。重写规则随后应用于此结构。对于boolean类型的项，使用带有等式的BDD的优点其他选项包括-hash和-no-hash，用于选择在重写期间是否使用哈希表，以及-jitty，用于使用即时解释重写器[33]而不是标准编译重写器。sumelm工具将由求和约束的变量替换为如果可变的数据与该数据集是一致的，则该数据集是可变的。Consider，例如，以下表达式：f：Fread（f）·X（f）a f = e d δ。它表示如果f=e，则执行read（f）·X（f）;否则，不执行任何操作。满员你然而，由于f=e，表达式可以简化为（e）·X（e）。60S. Blom等人理论计算机科学电子笔记139（2005）49此外，由于如果fe不采取任何行动，条件可以被丢弃，并且由于f不再出现，因此也可以省略对f的求和。因此，表达式被转换为read（e）·X（e）;求和运算符被删除。工具tbfupdate根据转换文件将线性过程中的动作标签替换为其他标签。在附录B中可以找到这样一个文件，例如，规定任何项t的动作c1（t）被无参数的动作ctau 可以根据操作的值进行重命名。工具状态图根据假设为状态变量的多个变量从线性过程计算控制流程它还应用控制流分析来去除不可达的被加数，并将数据参数与控制流图相关联。工具状态图还尝试改变虚拟参数的值，并尝试猜测更好的初始值。特别是最后一步通常允许constelm删除更多的参数，因为这些参数现在已经变成常数。工具structelm将构造函数排序的变量，即用func定义的构造函数排序，替换为指示所使用的构造函数的变量和指示该构造函数的参数的变量其优点是，constelm和parelm等工具只对变量而不是子项进行操作，因此也可以消除subex的一部分典型的例子如下。考虑由两个自然数的乘积组成的数据类型Tuple，以及一个可以显示此对的左元素的虚构过程排序帧funcframe：N×N→Framemap left，right：Frame→Nvarl，r：Framerewleft（frame（l，r））=lright（frame（l，r））=rprocX（f：Frame）=a（left（f））·X（f）将structelm -expand Frame应用于此过程会产生以下过程（其中变量的名称已被简化以便于阅读）：procX（l：N，r：N）=a（l）·X（l，r）parelm的应用允许删除参数r，这在应用structelm之前是不可能的。工具confcheck和confelm旨在检查线性过程的τ-连续性，并使用τ-优先级减少这些过程的状态空间[14]。一S. Blom等人理论计算机科学电子笔记139（2005）4961一S// \a/// \// \LsJsJJ- -- -τ/a- -\/ssJJJFig. 1. τ-连续的典型图τ-连续性可以用标号跃迁系统给出简单的解释转移系统是τ-连续的，如果对于每个状态s和输出跃迁s−→sJ和s−τ→sJJ，其中ea是可以成为τ的任意实验，它是caset，t在这里是状态sJJJ和跃迁sJ−τ→图1是τ-连续性的典型图。sJJJ和sJJ−→asJJJ。如果一个转移系统是τ-连续的，并且没有无限序列的τ-步骤（τ-收敛），那么可以应用τ-优先级。这意味着在任何具有传出τ阶跃的状态中，所有其他传出跃迁都可以被移除。在某种意义上，优先考虑τ。因为转换系统的许多部分可以通过这种方式变得不可达，所以状态空间的大小可以大大减小。更重要的是，这种操作保留了分支互模拟[35]，这意味着简化的转移系统在行为上等价于原始转移系统。检查转换系统的一致性是相对无用的，因为必须首先生成转换系统，这是由于状态空间爆炸而难以在线性过程中，连续性可以用符号来检验，并在生成状态空间时使用（参见instantiator-conciliuentbe- low）。必须验证的精确公式可以在[13，14]中找到。工具confcheck验证哪些τ在BKE协议中，我们使用Meta配置来理解哪些通信是连续的，并使用tbfupdate将这些内部操作重命名为ctau。工具confelm使用ctau动作满足连续性的事实，通过在线性过程上象征性地应用τ有许多工具我们在分析BKE协议时没有使用，但对于其他目的可能非常方便。使用invcheck和invelm工具来检查线性过程上的不变量的有效性并简化线性过程。工具二进制用于将线性过程中的有限数据类型的参数转换为Bool类型的参数序列。这在调用相等BDD时非常有用/62S. Blom等人理论计算机科学电子笔记139（2005）49prover，它对布尔型数据比其他数据类型更有效使用absint和absLoader工具进行抽象解释。可以精确地确定线性过程的参数并从中提取例如，自然数n可以抽象为布尔值b，其中b的含义为b：=n >0。其优点是减少了状态空间，但减少并不保持互模拟。在[34]中，通过引入必须和可能的转换，证明了约化保留了许多模态性质decluster工具用显式求和替换求和运算符。例如，被加数将替换为b：布尔a（b）·X（b）a（t）·X（t） +a（f）·X（f）。此工具通常也适用于无限数据类型的求和，前提是条件将有效值限制为有限个数字。例如Σ将替换为n：Na（n）·X（n）an3d δa（0）·X（0）+a（1）·X（1）+a（2）·X（2）。此外，还有可视化数百万状态的转换系统的工具[36]和符号验证模态公式的工具[16]。上述简化的主要目的是提高实例化器的速度，实例化器是从线性过程生成转换系统的工具减少实例化器的执行时间是必要的，因为它占用了总执行时间的大在我们的测试中，实例化器是用以下标记调用的：-monitor，允许我们跟踪实例化器的进度，-trace NOT SECRET，报告是否执行了对应于安全违规的操作NOT SECRET每一个测试都被执行了两次：有-连续的ctau标记和没有它。这个标记表示转换系统是ctau-连续的。因此，它允许实例化器对ctau进行优先级排序，删除每个状态中的其他转换以及传出的ctau。在表3中，这被称为动态连续消除。在一台具有2GB内存的机器上，instantiotor可以生成大小约为的转换系统。3107个州。对于较大的transi- tion系统的分布式版本的实例是必要的状态空间超过1 - 10- 9状态已产生。为了减少这些状态空间，分布式和独立（ltsmin，bsim）互模拟减少，S. Blom等人理论计算机科学电子笔记139（2005）4963有可用的工具[2]，但这些工具尚未用于验证BKE协议。生成的状态空间也可以由Caesar/Aldebaran工具集[11]处理，该工具集为状态空间提供了大量的约简3公钥双向密钥交换协议正如介绍中所解释的，双边密钥交换协议的目标在本节中，我们将详细解释该协议，并讨论该协议的μCRL图2在消息序列图中显示了该协议两个垂直轴表示协议的两个角色，即发起者角色I和响应者角色R。我们将每个角色的初始知识因此，发起方具有非对称密钥对（SKi，PKi）并且知道响应方PKr的公钥。同样地，响应者具有非对称密钥对（SKr，PKr）并且知道某个发起者PKi的公钥。这种最初的知识是如何建立起来的，并没有明确说明。发起者通过创建新的随机数ni来开始。这是一个随机的、不可预测的值，用于使交换的消息唯一，从而有助于对抗重放攻击。由发起者发送的第一个消息由ni，i对组成 i对用发起者的公钥加密预期响应者，由{ni，I}PKr表示。加密用于保证只有预期的接收者才能解包消息。响应者接受的唯一消息具有形式{ni，I}PKr，即，它们由他的公钥加密，并且它们包含一个现时值和发起者的身份在接收到消息后，响应者创建他自己的新的noncenr以及他想要与发起者共享的新的对称密钥Kir该协议的目标是以秘密的方式将该密钥传输给发起者。因此，响应者用消息{h（ni），nr，kir}PKi进行回复。 通过这个消息，他证明他能够解包先前的消息（通过显示他知道nonce ni，通过发送这个的散列h（ni）来证明）。nonce）。此外，该消息包含密钥kir和询问nr。完整的消息用发起者的公钥加密，以确保只有我可以解包消息。如上所述，这是发起者接受的唯一类型的消息。最后，发起者通过发送用密钥kir加密的随机数nr的散列来响应R他在此确认收到了先前的信息。在这两个角色的末尾，我们将安全声明列为一种特殊的事件。 两个参与者64S. Blom等人理论计算机科学电子笔记139（2005）49阿勃克SKi、PKi、PKrSKr、PKr、PKiI R农塞尼{ni，I}PKr临时编号基基尔{h（ni），nr，kir}PKi{h（nr）}kir密基尔密基尔声称每当他们到达协议的末尾时，不能让入侵者知道请注意，此协议仅保证新生成的密钥的保密性如前所述，我们在本文中将不关注认证。事实上，BKE协议的上述概述版本不保证通信方的认证它可以防止类似于著名的Needham-Schroeder公钥协议的中间人攻击但是，这种攻击不会危及密钥的Lowe对Needham-Schroeder公钥协议提出的修复也可以修复BKE协议在认证方面的这种变体。应该注意的是，其中一个被认为是诚实的代理人可能会与入侵者一起运行在这种情况下，显然，我们对他的保密声明不感兴趣。然而，如果与代理A的受损运行将允许入侵者冒充A并获得A与某个其他诚实代理B之间的通信的秘密密钥，则这将是非常不希望的。图二. 公钥双向密钥交换协议执行此协议的系统由许多代理组成，每个代理可以执行两个角色的一个或多个实例（并行）。当一个代理从协议中执行一个角色时，我们称之为运行。因此，一个系统是由一系列相互交换消息的运行组成的。μCRL中的协议规范见表1。我们需要数据排序Agent，自然数（N），Nonce和Key。代理商可以玩S. Blom等人理论计算机科学电子笔记139（2005）4965procI（self：Agent，n：N，a：Agent）=sI（{nonce（n），addr（self）}PK（a））·Σnr：N〇nce，key：KeyrI（{h（nonce（n）），nr，key}PK（seIf））·sI（{h（nr）}key）·密钥（Key）procR（self：Agent，n：N，a：Agent）=Σni：Nonce，a：AgentrR（{ni，addr（a）}PK（self））·sR（{h（ni），nonce（n），K（n）}PK（a））·rR（{h（nonce（n））}K（n））·表1启动者和响应者角色不同的角色同时为了区分这些角色，每个角色都有一个唯一的自然数n。此外，两个角色都有一个初始代理a，角色希望与他建立对称密钥。我们使用sI（sR）和rI（rR）分别表示发起者（响应者）发送和接收消息。具体说明非常简单，直接遵循消息序列图。4入侵者为了验证协议的正确性，我们需要通过添加入侵者来扩展上面的μCRL规范。如前所述，我们假设所谓的Dolev-Yao入侵者模型（见[10]），这被认为是最一般的对手模型这个模型意味着入侵者完全控制了网络，他可以从他的初始知识和从诚实的代理人收到的消息中获得新的消息因此，我们假设入侵者只有在拥有适当的密钥时才能解密消息。此外，我们假设一些代理人可能与入侵者合谋，并试图误导诚实的代理人，以了解他们的秘密。由于入侵者的能力，拦截任何发送的消息，并插入任何消息，可以从他的知识构建，我们可以模拟存在的阴谋代理，假设他们的秘密密钥是在入侵者的初始知识66S. Blom等人理论计算机科学电子笔记139（2005）49现在我们回到双边密钥交换协议。如果对于任意数量的代理，执行任意数量的运行，在Dolev-Yao入侵者存在的情况下，每当诚实运行在与诚实代理通信时进入保密声明时，对应的密钥kir永远不会暴露给入侵者，则图2为了验证协议，系统并行执行发起者的多次运行、响应者的多次运行和入侵者的一次运行。每次运行都由执行它的代理和编号标识。各方之间的通信沿着四个通信信道进行：从发起者到入侵者（1），从入侵者到发起者（2），从响应者到入侵者（3）以及从入侵者到响应者（4）。换句话说，发起者（响应者）通过执行动作sI（sR）发送消息，并通过执行动作rI（rR）读取消息（参见表1）的说明。与它们不同的是，入侵者向所有代理广播消息（动作sE），并读取所有存在的消息（动作rE）。只有在sE和rI，sE和rR，sI和rE，以及sR和rE之间才可能进行通信。特别是，这意味着入侵者可以访问网络中传播的所有消息我们还假设入侵者总是可以计算哈希函数h但给定h（x）的值，他无法找到x。为了启动双边密钥交换协议，每个参与的运行都应该知道它打算与之共享秘密的预期合作伙伴的名称。为了实现这一点，我们需要执行以下准备步骤：入侵者为每次运行选择合作伙伴的身份，并将其发送给相应的代理。代理使用此信息来选择用于加密的公钥。应该指出，一般来说，这一决定可以由代理人自己作出然而，将此任务委托给入侵者使过程τ-连续[14]，并显着减少了状态的数量因此，表1中列出的规格通过读取预期合作伙伴的名称的初步步骤进行了最后，我们回顾了入侵者可以执行的不同操作首先，他监听传入的信道，每次消息到达时，入侵者入侵者维护两个列表：获得的未加密信息列表和等待解密的未决消息列表最初，第一个列表包含所有代理的地址，它们的公钥，入侵者自己的秘密密钥，一个随机数和一个对称密钥。我们可以证明，一个随机数足以模拟一个拥有无限多个随机数的入侵者。第二个列表最初是空的。每次读取新消息时，入侵者都会检查它是否有相应的密钥进行解密。如果是这种情况，则消息被解密，其内容是S. Blom等人理论计算机科学电子笔记139（2005）4967添加到未加密信息的列表中，并且入侵者试图使用该内容来解密其他未决消息。如果消息不能被解密，则简单地将其添加到待处理消息列表为了简化给定解密密钥的消息的检索，我们将待处理消息列表组织为（key，lom）对列表，其中lom是需要解密密钥其次，如果入侵者拥有一些被其他方之一声称是秘密的信息，则为了做到这一点，他听取了其他代理人的保密要求，即，执行与发起方和响应方的保密声明秘密通信的动作秘密当一个密钥被声称是秘密的，入侵者验证密钥是否在他的手中，如果答案是肯定的，他就报告违反了保密性。最后，他可以发送一些不同的信息：(i) 一个自然数p和一个自然数p的关系。此消息用于为由p标识的运行建立伙伴。(ii) 在前面的某个步骤中收到的未更改的消息(iii) 模仿发起者的第一个消息的消息它加密一个随机数和一个地址。(iv) 模仿应答者的信息的信息它加密一个随机数、一个随机数和一个对称密钥的散列(v) 模仿发起者的第二消息的消息。它包含由对称密钥加密的随机数5优化和状态空间生成回想一下，为了验证协议，我们需要生成状态空间。为了减小状态空间的大小，已经执行了许多优化。第一个优化包括类型的使用，即，我们假设随机数总是可以与地址等区分开形式上，我们引入了四种类型的实体（数据排序）：随机数、地址、对称密钥和功能密钥。后一组包括非对称密钥和散列。这意味着入侵者在每一时刻都必须记住六个不同的列表，而不是两个列表（未加密的信息和待处理的消息）：四个对应于四种不同类型的（未加密的）实体和两个待处理的消息列表：那些由对称密钥加密的和那些由功能密钥加密的。其次，仔细检查协议，我们观察到散列函数只应用于nonce，并且安全声明仅在68S. Blom等人理论计算机科学电子笔记139（2005）49对称密钥第三，如果响应者与受损代理通信，则可以省略最后一个事实上，它既不会改变对手的知识，也不会导致响应者的额外安全要求。第四，我们跟踪入侵者可以执行的一些步骤每个发起者或响应者运行最多可以在原始双边密钥交换协议中执行三个读取和发送动作，并且在预备步骤期间再执行一个读取动作换句话说，给定进程数n，入侵者不需要发送超过4n条消息。最后一组优化考虑初始步骤。首先，在该步骤期间的消息的数量受到participating进程的数量的限制因此，我们在入侵者的实现中添加了一个新的参数p我们通过参与进程的数量来初始化p，并在每次迭代中递减它。接下来，回想一下，为了进行保密声明，运行的通信者应该与入侵者不同。由于我们对发现违反保密性的行为感兴趣，因此我们要求至少一次运行的通信者不是入侵者。我们通过要求最后考虑的运行（p= 1）与受信任方通信来强制执行这一点最后一个优化利用了验证测试的特定形式我们的第一个假设是有三个不同的代理：一个