协议组合逻辑：证明网络安全协议的安全性和合理性

理论计算机科学电子笔记172（2007）311-358www.elsevier.com/locate/entcs协议组合逻辑（PCL）Anupam Datta1Ante Derek2John C.米切尔3Arnab Roy4斯坦福大学摘要协议组合逻辑（Protocol Composition Logic，PCL）是一种逻辑，用于证明使用公钥和对称密钥加密的网络协议的安全属性。 该逻辑是围绕进程演算设计的，其中包含可能的协议步骤的操作，包括生成新的随机数，发送和接收消息，以及执行解密和数字签名验证操作。该证明系统由关于单个协议动作的公理和推理规则组成，这些推理规则产生关于由多个步骤组成的协议的断言。虽然断言只使用协议的步骤来编写，但逻辑在很强的意义上是合理的：每个涉及一系列动作的可证明断言在任何包含以下内容的协议运行中都成立： 恶意对手的给定动作和任意附加动作。这种方法使我们能够证明协议的安全性受到攻击，同时只推理协议中诚实方的行为。PCL支持关于复杂安全协议的组合推理，并已应用于许多行业标准，包括SSL/TLS，IEEE 802.11i和IEEE V5。保留字：安全协议分析、逻辑、组成1引言网络安全协议，如密钥交换和密钥管理协议，很难设计和调试。例如，用于保护链路层通信免受窃听和其他攻击的802.11有线等效保密（WEP）协议有几个严重的安全漏洞[11]。在安全套接字层[76，60]、后来的802.11i无线认证协议[37，38]、GPRS [43，7，19，14]等的标准和建议标准中也发现了异常和短路。尽管这些协议中的许多看起来相对简单，但与更复杂的分布式系统1 电子邮件地址：danupam@cs.stanford.edu2电子邮件地址：aderek@cs.stanford.edu3电子邮件地址：mitchell@cs.stanford.edu4电子邮件地址：arnab@cs.stanford.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.012312A. Datta等人理论计算机科学电子笔记172（2007）311当任意数量的多个会话同时执行并且攻击者可以使用在一个会话中获取的信息来危害另一个会话的安全性时，协议必须实现某些目标。由于安全协议构成了现代安全网络系统的基石，因此开发信息丰富、准确且可部署的方法来发现错误并证明协议符合其安全要求非常重要。虽然模型检查已被证明有助于发现网络安全协议中的某些错误类别[59，60，66]，但需要逻辑方法和证明程序来证明协议是正确的，关于协议执行的精确模型和恶意攻击者能力的精确模型。在本文中，我们描述了一个特殊的逻辑，开发的目的是证明网络协议的安全性，并给出了一些使用的例子。协议组合逻辑（Protocol Composition Logic，PCL）[20，21，22，23，24，25，26，29，30，38，67，68]是一种用于陈述和证明网络协议安全属性的形式逻辑。该逻辑编码并支持对单个协议步骤的结果进行直接推理，允许将单个步骤的属性组合起来以证明复杂协议的基本断言类似于Hoare逻辑[40]和动态逻辑[35]，公式θ[P]X表示在线程X中执行动作P之后，从公式θ为真的状态开始，公式关于结果状态为真。虽然该公式只提到了线程X的操作P，但在X执行P之后达到的状态可能是这些操作和其他线程执行的任何附加操作的结果，包括攻击者的任意操作。PCL包括许多动作谓词，例如Send（X，t）、ReceiveTM（X，t）、New（X，t）、Decrypt（X，t）、Verify（X，t），它们断言命名线程已经执行了所指示的动作。例如，如果线程X将术语t作为消息发送，则Send（X，t）在运行中保持。一类保密属性可以用谓词Has（X，t）来指定，这直观地意味着t是由X生成（使用新动作）或接收的成分构建的，这些成分在加密时不会隐藏在X没有的密钥中。一个谓词是NoveltoPCLisHonest（X），它会使X的所有操作都已完成根据协议。诚实主要用于假设一方遵守了协议的规定步骤。例如，如果Alice发起与Bob的交易，并且希望得出只有Bob知道她发送的数据的结论，则她可以通过明确地假设Bob是诚实的来可证明地这样做。如果Bob不诚实，那么Bob可能会让攻击者知道他的私钥，从而允许攻击者解密截获的消息。PCL公理和推理规则分为几类。有一类简单但必要的公理断言，在执行某个操作之后，所指示的线程已经执行了该操作。另一类公理是那些陈述密码操作属性的公理。例如，一个反映数字签名不可伪造性的公理指出，无论何时代理人验证诚实代理人的签名，那么该代理人必须在该消息上生成签名并在先前的消息中发送。 PCL还使用了一种新的形式归纳，目前被称为A. Datta等人理论计算机科学电子笔记172（2007）311313由诚实代理执行的基本动作序列可用于导出关于存在对手动作时的任意运行的结论。为了以简单的形式了解这是如何工作的，假设在某些协议中，每当主体接收到形式为ENC K的消息{|甲乙丙|}，表示在密钥K下对（a，b）的加密，主体然后用ENC K{|B|}。进一步假设，这是协议规定消息包含以下内容的唯一情况：发送单个加密数据。使用诚实规则，可以证明如果主体A是诚实的，并且A发送形式为ENC K{|B|}，则A必须先前已经接收到形式为ENC K{|甲乙丙|}。对于某些协议，这种形式的推理使我们能够证明，如果一个协议的parti-Pant完成了规定的动作序列，并且在其中一个消息中指定的另一个主体是诚实的，则这两个参与者被保证了一种形式的认证。与上一代以BAN和GNY逻辑为例的协议逻辑一样，PCL最初也被设计为认证逻辑，涉及用断言注释程序，不需要对攻击者的行为进行显式推理，并使用新鲜度，发送和接收消息的公式与BAN和相关逻辑相反，PCL避免了对“抽象”阶段的需要，PCL也是使用标准逻辑概念（谓词逻辑和模态运算符）来制定的，不涉及PCL的一个独特目标是支持安全协议的组合推理，包括不同协议的并行组合和协议步骤的顺序组合例如，许多协议假设长期加密密钥已经被正确地分发给协议代理。PCL允许密钥分发协议的证明与使用这些密钥的协议的证明相结合。PCL的另一个方面是基于协议模板的组合方法，协议模板是 在模板方法中，可以在关于这些函数变量的某些假设下建立协议模板。然后，一个实际的协议的证明是通过使用满足证明条件的操作的组合替换函数变量来获得的PCL似乎可以很好地扩展到5到20条消息（或更多）的工业协议，部分原因是PCL证明似乎相对较短（对于正式证明），并且它已成功应用于许多行业标准，包括SSL/TLS，IEEE 802.11i和IEEE 802.11i。PCL合成定理在进行这些大规模的案例研究时特别有用。本文在前人研究成果的基础上，发展了314A. Datta等人理论计算机科学电子笔记172（2007）311A→B：mB→ A：n，SIG B{|n，m，A|}A→B：SIGA{|n、m、B|}图1.一、箭头-消息应答协议一个统一的符号和语义设置，改进了以前的一些技术定义和证明，并完成了以前的论文省略的一些细节。PCL的核心在[30，24]中较早制定。PCL [20，21，22，23，68]证明方法的后续工作以及使用PCL [5，38，68]的案例研究导致了对语法，语义和证明系统的扩展和修改。在本文中，我们统一的结果，在早期的文件，提出了一个定义的逻辑使用统一的符号。具体来说，本文将[30，24]纳入范围，并借鉴了[5]中的编程语言语法和时态运算符的处理。本文的其余部分组织如下。第2节描述了协议编程语言的语法第3节介绍了PCL的语法和语义，第4节给出了证明系统和可靠性定理。在第5节中给出了形式系统在认证协议中的应用。第6节提出了关于协议的顺序和并行组合的定理，并通过应用于密钥交换协议来说明它们的使用。第7节总结了与PCL相关的其他结果，本文未详细说明第8节讨论了相关工作，第9节给出了结论。2建模协议为了形式化地陈述和证明安全协议的属性，我们首先需要将协议部分表示为数学对象，并定义它们如何执行。常见的非正式的箭头和消息符号（例如，在[69，12]中使用）通常是不充分的，因为它只表示在没有攻击时发生的协议的执行。安全分析的一个重要部分涉及了解运行协议的诚实主体对来自恶意攻击者的消息的响应方式。此外，我们的协议逻辑需要更多关于协议的信息，而不是从诚实方和恶意方获得的协议执行集;我们需要对执行每个协议角色的每个主体执行的程序进行高级描述，以便我们不仅知道运行中发生了哪些动作（哪些没有），而且知道它们为什么发生。现在，我们用一个例子来展示协议是如何表示的。图1以非正式的箭头和消息表示法显示了标准的基于三向签名的质询-响应协议（CR）。协议的目标-A. Datta等人理论计算机科学电子笔记172（2007）311315在随机数上的签名和另一方的身份相同协议的角色在图2中的符号中列出，如下所示：ingX 和Y分别用于执行角色InitCR和RespCR的主体。我们的定义由两个优先级（由X、Y、. . . ）whhichcorrespondo协议参与者，并且可以在任何点和线程（由X，Y，. . .其指的是执行协议的一个特定会话的主体。在这个例子中，协议由两个角色组成，发起者角色和响应者角色。图2中的CordInitCR给出了启动器角色中的操作序列。在言语上，执行角色InitCR的主体的任务是：生成一个新的随机数;向该主体发送一个随机数和一个随机数;从该主体接收一个随机数addressY ;verifythemessage ecttisYs i g a t u rt注意到;并确定所有，并确保不会将其存储到Y轴 有发起人的签名在第一个时代，没有任何一个国家的情况下，没有任何一个国家的情况下，从Y和Y的身份。形式上，协议将由一组有限的角色给出，每个角色都有一个。议定书除了动作序列之外，cord还具有静态输入和输出参数，用于顺序组成角色。初始CR（Y） [新m;sendX，Y，m;接收Y，X，y，s;RespCR（）[接收X，Y，x;newn;r：=sign（n，x，X<$），Y<$ ;]X（）验证s，（y，m，X），Y;r：=sign（y，m，Y），X;sendX，Y，r;]Y（）发送Y，X，n，r;接收X，Y，t;验证t，（n，x，Y），X;图二. 应答协议2.1协议编程语言我们的协议编程语言是一种传统的过程演算，与CCS，CSP及其变体和后代[41，57]相同。然而，由于我们在本文中考虑的协议是一个并发组成的顺序角色，过程演算是针对这种形式。该形式主义最初在[29，30]中被描述为弦演算，引用了串空间形式主义[31]，它方便地形式化了通过“箭头和消息”描述协议的实践然而，虽然串空间提供了信息流的全局和静态视图，但我们需要分析分布式推理和计算的动态。为了形式化地捕捉主体的动作（例如，他们接收到什么）可能决定和改变他们以后的动作（例如，他们将发送什么）的方式代表316A. Datta等人理论计算机科学电子笔记172（2007）311（keys）K：：=k基本键N名称K逆键（基本项）u：：=x基本项变量n随机数N名称P螺纹K键u，u基本项（terms）t：：=yterm variableu基本项t，t项元组ENC K{|不|}使用密钥K SIG K加密的术语{|不|}用密钥K签名的项表1协议程序设计语言的定义.术语存储的消息被接收，我们使用过程演算变量，和一个简单的反应规则表示的替代机制，对应于基本的通信和计算操作。与传统的进程演算相比，我们需要一种机制来识别执行一系列动作的主体，以便可以识别和限制对密钥的访问。由此产生的进程演算提供了一个协议执行模型，接受的概念的基础上，从进程演算，串空间和化学抽象机。其正式组成部分如下。方面假设给出项t的基本代数。像往常一样，它们是由常量c和变量x通过一组给定的构造函数p构建的，在本例中，case至少包括元组、公钥加密ENC K{|不|}，签名SIG K{|不|}。 我们假设有足够的类型来区分密钥K和优先级A，N和S。这种类型的电子设备将不会有任何可用性。像往常一样，计算被建模为术语评估。封闭项是可以完全评估的，是在协议.包含自由变量的术语（即指针和引用）不能被使用。示例将X轴 、Y轴、m轴插入CR程序的初始值中（见图1），这意味着不存在X轴，Y轴是消息的一部分，缩进的发件人和收件人，而不是发送操作的参数出于技术目的，我们在不显式包含密码操作的基本项u之间进行区分（尽管它们可能包含A. Datta等人理论计算机科学电子笔记172（2007）311317（动作）a：：=删除null操作sendusend a termu接收x接收项到变量x中newxgenerate new termxmatchu/umatch a term to apatternx：= signu，K sign the termu验 证 u ， u ， K验 证 签 名 x ： =encu，K加密项u x：= decu，K解密项u（股）S：：= [a;. ;a]P（角色）R：：=（→x）S（→t）表2协议编程语言的定义-动作、链和角色其值例如是加密的变量）和可以包含密码原语的项T名称、密钥、会话和线程我们是A组B组.. . . Asnamesforproprotoco l parandompants. 我们将提供一个网络和一个使用A、B、.. . 为公共部门制定了一项政策，响应代理。 一个特定的参与者可能参与了不止一个会议一次。 例如，代理在CR准备过程中，采取主动行动，以避免因数据丢失而造成的损失和C作为一名急救员，没有任何一家公司是与D公司合作的。对于此，我们将提供一些损失和使用A，以确定由A执行的第四个目标。行动、环节和作用动作集包含随机数生成、加密、解密、签名生成和验证、模式匹配、测试和通信步骤（发送和接收）。模式匹配运算符用于构造和断开元组并执行相等性检查。我们经常省略模式匹配操作符，隐式地执行匹配。例如，在图1中给出的CR协议的描述中，匹配是在接收动作中隐式完成的，如果我们要完全写出动作，则会有一个接收x动作，后面跟着一个匹配动作，分析元组，并执行相等性检查。操作列表将只包含基本术语，这意味着加密不能隐式执行;必须使用显式enc操作。为了方便起见，我们假设任何变量最多被赋值一次，并且第一次出现的特定变量必须是赋值。这种单赋值语言的操作语义将明显更简单，因为我们可以用术语替换来建模赋值。318A. Datta等人理论计算机科学电子笔记172（2007）311(1) [接收x; S] X|[send t; T] Y−→ [S（t/x）] X|[T] Y(2)[matchp（t）/p（x）;S]X−→[S（t/x）]X(3)[newx;S]X−→[S（m/x）]X(4)[x：= enc t，K; S] X−→ [S（ENC K{|不|}/x）] X(5)[x：= dec ENC K{|不|}，K; S] X−→ [S（t/x）] X(6)[x：= sign t，K; S] X−→ [S（SIGK{|不|}/x）] X(7)[验证SIGK{|不|}，t，K; S] X−→ [S] X必须满足下列条件(1)FV（t）=Δ(2)m/∈FV（C）<$FV（S），其中C是整弦空间表3基本反应步骤一个串就是一个动作序列以及执行这些动作的线程的名称。角色是一个串，在执行顺序组合时使用输入和输出接口角色中的所有变量都必须由输入接口或其他操作绑定。 一条弦只是一条没有自由变量的链，也就是说，所有的基项要么是常数，要么被一个特定的作用所束缚。2.2执行模型线空间一个cord空间是一组cord，每个cord都在下标中标注了执行它的agent的名称多集并集表示为|，空的多集由[]。这个想法是，一个索空间代表了一组准备参与的过程，通信和分布式计算。它们的操作行为由表3中的反应规则定义。每个反应所需的副反应条件如下所示。置换（t/x）作用于左边的链。通常，假设没有自由变量在替换后成为绑定的，这是通过重命名绑定变量来实现的反应（1）是一个发送和接收的相互作用，表明第一根弦同时发送项t，第二根弦同时接收t到变量x我们称之为外部作用，因为它涉及两条弦之间的相互作用。其他的反应都发生在一条线上。我们称之为内部行为。反应（2）是基本的模式匹配动作，其中线将模式p（t）与期望模式p（x）匹配，并且用t代替x。反应（3）显示了绑定动作，其中cord创建了一个新值，该值的条件FV（t）=t的直观动机应该是清楚的：一个项不能被发送或测试，直到它的所有自由变量都被实例化，以便可以对其进行评估。此外，当通过新操作生成新的随机数时，A. Datta等人理论计算机科学电子笔记172（2007）311319结果常数在整个弦空间中是唯一的反应（4）和（5）分别是加密和解密动作。例如，解密动作匹配模式ENC K{|p（t）|}并且用t代替x。反应（6）和（7）是签名生成和签名分别进行验证。正如我们已经提到的，由于赋值是通过项替换建模的，因此单个变量只能赋值一次。协议协议Q是角色的集合{P1，P2，.，ρ k}，每一个在Q的任何运行中由零个或多个诚实主体执行。直观地说，这些角色可能对应于发起者、响应者和服务器，每个角色都由一系列要在单个角色实例中执行的动作指定。协议参与者被称为主体，并由A、B、· · ·等表示。由主体执行的特定用户执行的线程称为线程。单个主体的所有线程共享静态数据例如长期密钥。如上所述，这是使用静态绑定形式化的。作为一种旋转方式，我们将使用X来不与一个优先级的X对象相关联。私钥是形式X的密钥，它表示公钥密码系统中的解密密钥 私钥X只允许出现在主体X的线程中。更重要的是，它几乎完全不需要在指定的磁盘中进行复制（对应于参与者解密由其公钥加密的消息）和签名构造（对应于参与者签名消息）。这些限制防止在消息中发送私钥。虽然一些有用的协议可能会发送私钥，我们防止角色发送他们的私钥（在本文中），因为这使我们能够将私钥的保密性作为公理，缩短了协议属性的证明。入侵者角色攻击通常是通过将一个协议与另一个过程组合而获得的过程，以这种方式，结果运行，投影到协议角色，不满足协议要求。攻击者或入侵者是一组线程，它们在攻击中共享所有数据，并在一个或多个协议会话中扮演角色。这种直觉在下面的初始配置定义中得到了体现。可用于构建入侵者角色的操作通常包括接收和发送消息、将消息分解为多个部分、使用已知密钥解密消息、存储数据，甚至生成新数据。这是标准的布氏帘线正如我们所定义的那样，绳索反应是同步通信的模型由于真实的通信网络是异步的，我们需要引入一个缓冲器，在那里发送的消息可以被存储，直到有人准备好接收它们。为了用绳索模拟这一点，我们引入了一种布氏绳索，320A. Datta等人理论计算机科学电子笔记172（2007）311XX[receivex; sendx]，它对正在接收的消息进行建模，然后最终发送。我们将要求主体和入侵者的所有发送和接收操作都是通过总线执行的，并假设在每个协议中都有足够的总线实例来保证每个消息的传递。Buchener cords是基础设施的一部分，而不是协议的一部分，我们假设它们是由特殊的无名代理执行的除非另有说明，当我们提到线程时，我们指的是非缓冲线程，同样，当我们提到动作时，我们指的是由非缓冲线程执行的动作正如[6]所证明的那样，这种用缓冲器扩展的同步进程演算忠实地表示异步通信，并且对应于异步进程演算的通常定义。配置和运行协议Q的初始配置由以下决定：（1）一组主体，其中一些被指定为诚实的。(2)通过将Q的角色分配给诚实主体的线程而构建的cordspace。(3)一个或多个入侵者密码，可能使用不诚实主体的密钥（4）有限数量的缓冲线，以适应诚实线程和入侵者线程的每个发送操作。 运行R是从初始配置开始的一系列反应步骤，受到每个发送/接收反应步骤发生在一些缓冲器线和一些（非缓冲器）线程之间的约束。一个特定的初始配置可能会产生许多可能的运行。事件和痕迹由于协议逻辑推理是关于协议运行的，我们需要为它们引入事件是动作的地面替换实例，即，所有变量都被只包含常数的项所代替的一种行为事件代表了一个反应步骤的结果，从参与其中的单个连接线的角度来看。例如，如果线程A发送消息m（到接收缓冲器连接线），则事件sendm是A的发送事件。或者，我们可以将运行视为从初始配置开始的事件的线性序列我们使用以下元符号来描述索演算的反应步骤EVENT（R，X，P，→n，→x）.[PS] |C−→[S（→n/→x）]|CJ<$∈R<$当EVENT（R，X，P，→n，→x）在运行R中运行时，X和X在运行P中执行，将数据→n转换为变量→x，其中→n和→x是相同的。跟踪是运行中某个线程的事件列表。我们使用R|X表示在运行R中线程X发生的事件。对于一系列操作P、协议Q、运行R和线程X，我们说“P匹配R|X“，如果R|X精确地是σP，其中σ是变量的值的替换。如果P和R匹配|X使用置换σ，则σ称为匹配置换。A. Datta等人理论计算机科学电子笔记172（2007）3113212.2.1协议属性在本节中，我们收集了一些协议的属性，这些属性将在本文的其余部分引理2.1（无心灵感应）设Q是一个协议，R是一个任意运行，X是一个线程。设m是X作为cord ρ i的一部分发送的任何消息。那么项m中的每个符号要么在ρ i中生成，要么在ρ i中接收，要么在ρ i的静态接口中。证据这源于我们用来代表角色的连线的定义。每个角色都是一条闭合的绳索，因此所有的价值观都必须被绑定。符号可以由静态接口绑定，也可以由new、receive和pattern match操作绑定。Q引理2.2（异步通信）在每次运行中，任何希望发送消息的线程都可以发送消息。而且，所有外部动作之间有严格的线性顺序。证据根据定义，在初始配置中有足够的缓冲器线为非缓冲器线程的每个发送操作提供接收。由于“外部动作”指的是非缓冲器线程的发送或接收，因此从运行的定义可以得出，在运行的同一步骤中不能发生两个外部动作。Q引理2.3每个接收动作都有一个相应的发送动作。 更正式地说，如果在运行R中，线程X执行了动作receive x，将数据m接收到变量x中，那么存在线程Y，使得在同一运行R中，线程Y执行了send m动作。证据这是从基本索演算反应步骤的定义和缓冲索的定义得出的Q引理2.4对于协议Q的任何初始配置 C和任何运行R，如果当x∈HONE ST（C）时，x由环x变换，R|X是一个由X执行的Q个执行过程的一个过程。证据 这源于初始配置的定义，初始配置是通过将角色分配给诚实主体的线程来构建的。Q3协议逻辑3.1语法PCL的公式由表4中的语法给出，其中S可以是任何链。这里，t和P分别表示项和线程。我们用φ和φ来表示谓词公式，用m来表示我们称之为“消息”的通用术语。消息具有形式（源，目的地，协议标识符，内容），除了消息内容之外，还给每个消息源和目的地字段以及唯一的协议标识符。消息的源字段可能无法识别消息的实际发送者，因为入侵者可以欺骗源地址。同样，322A. Datta等人理论计算机科学电子笔记172（2007）311行动公式a：：= Send（P，t）|接收（P，t）|新（P，t）|加密（P，t）|解密（P，t）|符号（P，t）|验证（P，t）公式φ：：= a |a