安全协议组合性研究：形式化方法与安全性质验证

理论计算机科学电子笔记142（2006）99-110www.elsevier.com/locate/entcs安全协议的组合性研究Cas Cremers1埃因霍温理工荷兰埃因霍温摘要在过去的25年里，形式化方法在安全协议分析中的应用得到了广泛的研究。已经开发了几种用于验证安全协议的形式化和（半）自动工具。然而，它们的适用性仅限于孤立运行的相对较小的目前使用的许多协议无法使用这些方法进行验证其主要原因之一是这些协议由几个子协议组成。这样的协议组合在大多数形式主义中都没有得到解决。 在本文中，我们确定了一些相关的问题，应用正式的方法的安全协议组成的问题。此外，我们描述了需要做什么研究来迎接这一挑战。关键词：形式化方法，安全协议分析，组合性，安全性质。1介绍在互联网、电子商务和智能卡应用领域，使用密码原语现已成为标准做法。在过去的几十年里，许多研究已经涵盖了这些密码原语所涉及的数学问题，其中许多问题现在已经得到了很好的理解。然而，使用这种很好理解的密码原语来实现协议并不能保证协议本身满足安全要求（参见例如[10]）。这一观察指导了安全协议研究的一个分支，其中假设密码原语是1电子邮件：ccremers@win.tue.nl1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.12.047100C. Cremers/Electronic Notes in Theoretical Computer Science 142（2006）99完美，并且使用密码学的黑盒视图（cf. [8]）。使用形式化模型，可以证明安全协议在某些假设下是正确的（参见[16，6]）。此外，还有各种工具可以发现对安全协议的攻击，如[4，11，13]。虽然已经取得了很大的进步，已经调查的协议仍然是规模不大。可用的证明方法以及工具都不能很好地扩展。同样，形式模型假设了我们所谓的封闭世界。这意味着系统中的代理不会表现出协议中指定的任何其他行为这种封闭世界的假设并不适用于大多数应用程序。例如，互联网上的代理通常能够进行多种类型的行为，并同时使用多种协议。但是，即使封闭世界假设不成立，民间传说和共同的感觉表明，只要并行协议不共享公共数据，就不会造成伤害。许多设计依赖于这一假设，并为不同的协议使用不同的密钥。另一方面，在许多上下文中，期望具有在协议之间共享的密钥。当为智能卡应用设计协议时，诸如存储器和带宽之类的资源是有限的，因此重用密钥材料是有意义的即使在设计这样的资源充分可用的复杂系统时，为每个子协议引入密钥基础设施也可能非常昂贵我们认为在封闭世界假设下验证单个协议因此，我们开始扩大这个封闭的世界，并提高现有的形式化方法的可扩展性。此外，我们建议一个新的抽象层次的安全协议的组成我们确定了一些开放的问题，以解决未来的工作安全协议。本文其余部分的组织如下。在第二节中，我们研究了封闭世界假设，并给出了一些例子来指出问题所在。然后，在第3节中，我们将讨论如何建模一个更大的封闭世界，并指出这样一个世界的语义要求。我们在第4节中为这个问题专门设计了一个新的抽象层次。一些相关的工作在第5节中讨论，我们在第6节结束时给出结论性意见和一些开放的研究问题。C. Cremers/Electronic Notes in Theoretical Computer Science 142（2006）991012安全协议正如在引言中所述，有几种形式化的方法来确定一个安全协议实现了某些安全目标。由这些方法所作的假设之一是封闭世界假设，即所涉及的代理没有表现出比协议所描述的行为这个假设，结合一个显式的入侵者模型（如Dolev-Yao，见[8]），使我们能够描述系统的所有可能状态，这是代理和入侵者的组成。该系统的每一种可能的行为都被建模，这一事实允许证明该系统的一些属性如果我们在同一环境中执行多个（可证明正确的）协议，则入侵者可以使用协议的某些部分来生成他无法以其他方式构造的消息。当多个协议同时执行时，入侵者可以伪造的消息数量呈指数级增长。这可能导致攻击协议的新方法。在[1]中描述了对SSL早期版本的这种攻击的示例另一个对组合协议的攻击可以在[15]中找到。可以通过将这些协议集合建模为单个更大的协议来验证它们，但是所得到的协议通常非常大，因此超出了当前方法的范围。这样做的结果是，有一些已知的小协议，可证明实现安全目标，如保密或认证，在某些假设下，如封闭世界假设。孤立地说，这些协议不是很有用。在现实世界的应用程序中，它们将被同时使用或附加到其他协议中，从而使证明的封闭世界假设因此，所产生的系统不一定符合安全目标。目前的做法是，大型或组合协议没有正式验证。验证工具可以验证小型协议，但没有指导方针如何将它们组合成更大的协议而不引入新的攻击。我们希望纠正这种情况，使形式化的方法appli-cable到现实生活中的系统。为了促进这一点，并使正式的方法可用于更大的系统，需要解决一些挑战。在接下来的两节中，我们将简要介绍两种可能的解决方法。102C. Cremers/Electronic Notes in Theoretical Computer Science 142（2006）993提高可扩展性安全协议分析的形式化方法的一个主要缺点是缺乏可扩展性。我们发现，可以分析的安全协议的大小，与在网络中使用的协议相比，仍然相当小。例如SSL等互联网协议。目前使用的许多协议都一般来说，这样一个更大的，组成的协议不能使用当前的形式化方法进行验证我们认为，由于三个主要原因，目前的许多方法不能很好地扩展这些协议。(i) 状态空间爆炸。如果一个协议扩展了许多消息，系统的状态空间呈指数增长。请注意，这个问题并不特定于安全协议分析。(ii) 缺乏对正式模型的支持，无法捕获子协议组成。(iii) 缺乏形式化模型对子协议安全目标的支持.为解决这些问题，已经进行了一些尝试。状态空间爆炸问题并不是安全协议特有的，它发生在许多并发进程模型中。有时可以使用符号表示，或通过为模型的特定实例提供不变量或其他状态空间限制来补救，但这些技术通常需要（创造性的）用户输入。然而，处理这个问题不在本文的范围内，我们建议读者参考例如。[2]的文件。第二个问题，缺乏对（子）协议组合的支持，已经在[16]的StrandSpaces框架中得到了解决。在原始的串空间框架中，不可能对并行协议进行这导致了对串空间模型的一个小修改，称为混合串空间模型（见[15]）。在这个模型中，初级和次级链的概念被引入，这允许在存在其他协议的情况下分析协议。然而，在这种混合模型中，第三个问题是指定子目标，这留给了对系统进行建模的用户。在组成两个子协议时必须非常小心，因为最终的目标集可能不一致。一个可以处理协议和目标的并行组合的较新的形式化模型是安全协议的操作语义，如[6]中所定义的。在这个模型中，协议角色的概念被认为是建模的基本单位。简单协议的模型由一组角色组成，在这些语义中，C. Cremers/Electronic Notes in Theoretical Computer Science 142（2006）99103通过简单地向系统添加更多角色来捕获协议。安全目标被建模为协议中的事件，代表本地声明，并且可以毫无问题地组合。还有许多工作要做。我们确定了一些仍然需要克服的障碍。3.1运行界限的确定一般来说，基于工具的安全协议验证假设攻击中涉及的运行或协议角色实例的数量。这样的界限用于限制问题的状态空间，并使自动验证可行。有时这个界限是显式确定使用手证明[10]，但在大多数情况下，一个下界是简单地假设。这意味着大多数工具可以证明存在攻击，但它们不能证明协议在所选范围之外是安全的。这是因为没有证据可以证明任何协议都有可用的理论界。到目前为止，使用工具进行验证是基于一些经验法则（例如，每个角色的两个任意实例）或经验（文学中的攻击最多涉及三到四次运行）。当我们验证组合协议时，这样的边界再次变得相关，因为即使每个角色有两个实例也可能导致一个太大而无法探索的状态空间。如果可能的话，我们正在寻找一种自动程序，在给定特定协议和安全目标的情况下，它可以确定攻击所涉及的运行的上限3.2支持协议组合大多数安全协议模型不支持组合协议分析。验证这些协议的第一步是调整形式模型的语义。可能有些模型不容易适应这样的任务，因此需要进行研究模型语义的适应也是工具所必需的。如果某个模型不支持协议组合，那么基于该模型的工具也不会支持。例如，Casper/FDR工具集就是这种情况（参见[11]）。Athena工具（参见[13]）支持协议的并行组合，但需要专家用户提供合适的输入。Scyther工具（参见[4]）通过简单地连接协议描述，以直观的方式支持组合104C. Cremers/Electronic Notes in Theoretical Computer Science 142（2006）993.3对安保需求构成的安全需求的组成之所以重要，主要有两个原因。第一个原因是安全属性通常只考虑简单的协议。许多安全属性被定义为两方属性，例如Alice验证Bob，Alice与Bob共享密钥。这样的属性可能会在组合协议上下文中引入歧义例如，考虑两个并行协议P1和P2，它们都使用相同的基本身份验证协议。假设Alice启动了协议P1的一个实例. 因为基础协议是一样的，她最后说到Bob的响应者实例。她可以证明她正在与Bob交谈，但她不能确定他使用的是哪种协议。假设协议P1使用来自基础协议的随机值来创建会话密钥，而P2使用这些随机值来创建公开的会话标识符。Alice根据该值创建了一个会话密钥，但是正在执行协议P2的Bob实际上公开了这些随机值。因此，随机值的不同语义可能导致严重的安全问题。请注意，在这两种情况下，Alice和Bob都同意他们使用的随机值可以安全组合的强认证属性是同步，如[7]中所定义的。然而，根据需求组合，其他属性也需要重新审视。这种组合之所以重要的第二个原因是，许多形式主义认为安全需求是与协议规范分离的实体，例如在串空间模型中。一方面，我们有一个协议规范，另一方面，有单独的逻辑公式的要求。当我们组合两个协议时，我们还需要组合这些逻辑公式。这样的组合是否产生有效的安全要求是一个悬而未决的问题。在我们的安全协议操作语义中采用了另一种方法，其中安全属性声明被建模为协议中的事件。因此，需求被集成到协议规范中。如果组成两个协议，则也组成需求。安全性要求已经建模，考虑到并行协议的可能性。3.4证据的合成性虽然提到的混合串空间和操作语义学看起来都很有前途，但它们的有用性受到以下事实的限制：一般来说，协议证明不是组合的。因此，对于两个prov的组成，C. Cremers/Electronic Notes in Theoretical Computer Science 142（2006）99105正确的协议，必须构造新的证明。在某些情况下，我们可以避免这一点：混合串空间模型的一个结果表明，如果两个协议非常不相似（参见[9]），则一个协议的安全目标的正确性这些结果对协议的设计有一定的参考价值。然而，我们需要更多的这类结果来推理协议的组成3.5安全协议当一个安全协议被正式指定时，通常在它独立运行时指定它的要求。这与核查的进行方式有关。然而，在设计一个协议时，我们已经可以指出在哪些假设下，它与其他协议组合时仍然是正确的作为一个例子，考虑一个旨在生成和分发秘密会话密钥的协议，该密钥将用于验证消息序列，并保持其内容的秘密。在所涉及的代理知道密钥之后，正式协议通常结束。该协议隐含地假设会话密钥然后以正确的方式使用，例如，这样它就保持秘密。 这在密钥交换协议中没有表达，它的目标只是建立密钥。然而，这样的协议只有在我们实际上在其他协议中使用会话密钥时才有意义，因此必须始终如此。保密目前的大多数协议并不意味着孤立地执行。此外，许多设计决策是因为这些协议意味着与其他协议组合而做出的。因此，必须明确这些环境假设。然而，目前的协议规范形式主义不适合表达这一点。我们需要表达协议的确切要求的方法对于这个例子，我们需要强制一些关于如何使用会话密钥的规则此外，协议可能会对现有的公钥/私钥基础设施做出假设，并为最终的组合系统引入一些证明义务。一个重要的研究问题是找到表达这些要求的简洁方法。一旦对协议上下文的这种要求可以具体化，我们就可以开始考虑将这些小协议作为更大的组合协议的构建块如果我们固定一组小协议作为构建块，我们可以将它们视为另一个抽象层次的原语。我们将在下一节探讨这个选项。106C. Cremers/Electronic Notes in Theoretical Computer Science 142（2006）994另一个抽象黑盒安全协议的标准Dolev-Yao模型依赖于加密和签名等密码原语。研究黑盒安全协议的一个原因是，即使存在完美的密码原语，协议仍然可以被攻击，如[10]中的Needham-Schroeder协议的常见示例所示。安全协议分析工作在与加密原语不同的抽象级别。在协议级别，我们有安全目标，如保密和认证，这与加密级别上的对应目标不同。此外，引入了新的概念，如内射性。这一抽象层实现了安全协议的形式化分析和自动验证。然而，并行协议组合似乎正在扩展协议模型的限制，一种解决方法是另一个抽象级别。我们建议引入一个新的抽象层，专门为安全协议的组成量身定制。这样的抽象将需要在协议组成级别制定安全目标。与此相对应，将必须制定一组新的原语，包括例如安全协议和消息封装。请注意，这样的抽象层不会帮助验证现有协议，而是用于构建和设计新协议。因此，基本问题将是选择一组适当的原语和相关概念。例如，考虑一个身份验证协议。这样的协议实现了例如协议或同步（如[12]和[7]中所定义的）。在实践中，在协议组合设置中，我们希望用另一个消息交换来扩展这样的认证协议，这样新消息也会被认证。我们相信这样的消息扩展是认证协议的一个组成部分。因此，用于身份验证的组合原语将充当消息交换序列的封装。给定一个消息交换，我们将应用这样一个认证原语，并且所得到的协议将满足同步。对于标准库中的协议，例如[14]中的安全协议开放库，我们发现消息序列图具有很强的表达力。然而，对于诸如允许代理在子协议之间进行选择的协议之类的组成问题，我们预计将需要诸如高级别消息序列图之类的图形形式。C. Cremers/Electronic Notes in Theoretical Computer Science 142（2006）991074.1开发概念和原语在协议组成层，我们希望安全目标，如保密性，是他们的协议对应的直接扩展。 对于认证、隐私和不可否认性等目标，我们预计必须对概念进行重大修改，以便应用于协议组合。Fig. 1. 由两个协议考虑图4.1中两个协议的组成。消息m2在协议1中被要求是秘密的。然而，它也发生在协议2中。像保密这样的目标对于协议的组成来说是全局性的，并且可能对系统中发送的每个消息都有影响。因此，我们希望保密原语不包含子协议，而是作为全局需求，或者更确切地说，作为所有消息的转换规则诸如会话认证之类的其他目标可以被构造为协议，该协议可以封装其他消息或协议。如图中协议2中的灰色区域所示，我们可以准确地指出协议的哪些部分需要认证。 因此，如果我们将某些数据的发送封装在会话身份验证协议中，则数据本身也将被身份验证。这种原语的实现可能涉及设置会话密钥，并用该会话密钥加密数据（以及序列号）。108C. Cremers/Electronic Notes in Theoretical Computer Science 142（2006）994.2原语分析一旦选择了合适的基元，我们需要分析它们的组成特性。希望具有尽可能简单的组合属性的原语。 在复杂性和复杂性之间有一个权衡，组成特性和效率/尺寸。例如，当原语之间没有数据共享时，组合性比共享密钥基础设施更容易。在设计原语时，我们希望出现依赖关系。例如，在Dolev-Yao模型中，身份验证需要某些数据项的保密性。因此，相对于特定的入侵者模型，在这种认证概念和保密概念之间建立了依赖性。研究这些依赖关系将有助于证明基元的性质，也有助于使描述更加简洁。5相关工作存在处理安全协议组合的其他尝试。我们简要讨论一些尝试。虽然大多数的安全协议形式主义不处理协议的组合，已经有很多工作，以提高目前的方法，更大的协议的可扩展性。 我们认为这有助于为组合协议的验证铺平道路。我们提到两个这样的方法。首先，[16]中的Strand Spaces模型已经取得了许多进展，从而在[13]中产生了高效的Athena工具。其次，我们开发的Scyther工具已经能够处理并行协议。该工具基于[6]中安全协议的操作语义，并使用[5]中解释的偏序约简技术最近的发展是Canetti在[3]中提出的通用可组合性概念。这种方法的根源在于安全多方计算，并且是针对构建实现其目标的（子）协议而定制的，而不管它们所处的环境如何。这导致对协议以及对环境的一些严格要求。由此产生的协议在两个重要方面与我们提出的原语类型不同。首先，它们允许特定的组合属性（通用可组合性），而我们允许更多类型的原语，这些原语可能共享信息或封装其他协议。其次，在通用可组合性框架中，有一个固定的入侵者模型，而我们建议制定概念，目标和抽象原语，而不管入侵者模型。另一种方法是修改Strand Spaces模型，使其C. Cremers/Electronic Notes in Theoretical Computer Science 142（2006）99109适用于处理协议组成，在[15]中。这种混合链空间模型已被用来推导理论结果。最初的结果显示了如何攻击协议组成是可能的。后来的结果包括在[9]中可以安全地组合协议的情况，其中也给出了固定协议的建议。这种方法有助于扩展当前的方法，但它缺乏更合适的抽象级别。6闭幕词过去几十年的安全协议研究在相当小的协议的形式化验证以及工具支持方面都取得了令人印象深刻的进展。下一步是处理由几个子协议组成的更大的协议。要进行任何形式的分析，都需要对模型进行一些假设，这总是意味着某种形式的封闭世界假设。然而，鉴于该领域的进步，应该有可能推理出一个更大的封闭世界。在这里，我们已经提出了我们的想法的研究是必要的，形式化的方法是适用于安全协议的组成。我们还为另一个抽象层勾画了初步的想法此外，我们还讨论了可以作为未来研究起点的具体研究主题我们自己已经完成的工作包括支持协议合成的安全协议操作语义的开发。基于这些语义，我们开发了一个验证工具Scyther，它可以发现对组合协议的攻击然而，仍有许多工作要做。我们总结了主要的开放研究问题：(i) 调整现有语义和工具以支持协议组合。(ii) 在给定协议的情况下，确定攻击所涉及的运行的最小上界。(iii) 调查证据的组合性。(iv) 扩展安全协议的规范，以包括确切的使用条件，在这些条件下，它们在与其他协议组合时是正确的。(v) 开发另一个用于安全协议组合的抽象层，并抽象出协议细节。(vi) 为这个抽象级别开发诸如安全目标和原语之类的概念110C. Cremers/Electronic Notes in Theoretical Computer Science 142（2006）99(vii) 确定这些概念和入侵者模型之间的关系。我们打算就这些研究问题开展工作，我们也想邀请其他人对这些问题进行引用[1] Benaloh，J.，B. Lampson，D.西蒙，T.间谍和B。Yee，私有通信技术协议（1995），draft-benaloh-pct-00.txt.[2] Burch ， J.R. ， E.M. Clarke ， K.L.McMillan ， D.L. 迪 尔 和 L.Hwang ， Symbolic ModelChecking：1020States and Beyond，in：Proceedings of the Fifth Annual IEEE Symposium onLogic in Computer Science（1990），pp.1citeseer.lcs.mit.edu/burch90symbolic.html。[3] 卡内蒂河Universally composable security：A new paradigm for cryptographicprotocols，Cryptology ePrint Archive，Report 2000/067（2000），eprint.iacr.org/.[4] Cremers，C.， Scyther文档，www.win.tue.nl/www.cycremers/scyther。[5] 克雷默角和S. Mauw，通过偏序约简检查保密性，在：D。Amyot和A. Williams，editors，SAM2004：Security Analysis and Modeling，4th Workshop on SDL and MSC（2004），pp. 177-194。URLhttp://www.win.tue.nl/下载/cm secondary reduction.pdf[6] 克雷默角和S.杨文，安全协议的操作语义，载于：北京大学出版社，2004年，待出版.[7] Cremers，C.，S. Mauw和E. de Vink，在跟踪模型中定义身份验证，在：T。Dimitrakos 和 F. Martinelli ， editors ， FAST 2003 ， Proceedingsofthefirstinternational Workshop on Formal Aspects in Security and Trust （ 2003 ） ， pp.131 www.win.tue.nl/authentication.ps。[8] Dolev ， D. 和 A.Yao ， On the Security of Public Key Protocols ， IEEE Transactions onInformation Theory IT-29（1983），pp.198-208.[9] Guttman，J. D. 和F. J. Thayer，《通过不相交实现议定书独立性》 PCSFW：Proceedings ofThe13thComputerSecurityFoundationsWorkshop（2000），citeseer.ist.psu.edu/guttman00protocol.html。[10] Lowe，G.，使用FDR打破和固定Needham-Schroeder公钥协议，Proceedings of TACAS 1055（1996），pp.147-166,URLweb.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Papers/NSFDR.ps网站。[11] Lowe，G.，Casper：A compiler for the analysis of security protocols，in：Proc. 10thComputer Security Foundations Workshop（1997），pp. 18比30[12] Lowe，G.，A hierarchy of authentication specifications，in：Proc. 10th Computer SecurityFoundations Workshop（1997），pp. 31比44[13]Song，D.， 雅典娜： 一个新 高效自动 检查器 安全 议定书 分析，在：1999年IEEE计算机安全基础研讨会论文集（1999年），p. 192.[14] 安全协议开放存储库，www.lsv.ens-cachan.fr/spore。[15] Thayer，F. J.，J. C.赫尔佐格和J. D. Guttman，Mixed strand spaces，in：Proceedings of the1999 IEEE Computer Security Foundations Workshop（1999），p. 72.[16] Thayer，F. J.，J. Herzog和J. Guttman，Strand spaces：Proving security protocols correct，Journal of Computer Security 7（1999），pp.191-230