自动证明PCL不变量的逻辑程序方法及其在传输层安全协议中的应用

理论计算机科学电子笔记234（2009）93-113www.elsevier.com/locate/entcsPCL不变量的自动证明方法John C. 米切尔1Arnab Roy2 Mukund Sundararajan3美国斯坦福大学计算机科学系摘要协议组合逻辑PCL是一种形式化的方法，用于证明一类网络协议的安全性。PCL涉及在不需要对攻击者动作进行显式推理的设置中直接推理协议步骤所实现的属性。该方法依赖于协议不变量来组合协议的不同角色的属性。虽然一些协议不变量可能很难识别和证明，但许多有用的PCL不变量是协议中涉及的代理执行的程序（角色）的相对直接的结果。我们提出了一个逻辑程序为基础的方法，自动化证明的不变量，出现有效的不变量，需要几个标准化的，广泛部署的协议。我们使用著名的传输层安全协议（TLS/SSL）来说明这种方法。保留字：安全协议逻辑、Prolog、自动证明、传输层安全1介绍协议组合逻辑（ProtocolComposition Logic，PCL） [10，11，3，5，4，7，15]是一个不断发展的形式逻辑框架，用于证明网络协议的安全属性。PCL解决的中心问题是，是否有可能证明实质性的安全协议组成的属性，使用推理步骤，不明确提到攻击者的行动。为了从组成上推理协议，一个代理对一个动作序列的属性的证明不仅涉及对该组件的安全目标的本地推理，而且还涉及防止来自可能使用相同证书或密钥材料的其他动作的破坏性干扰的环境条件。这些环境条件通常被声明为协议不变量，即对于协议的所有角色都为真的属性。1电子邮件地址：mitchell@cs.stanford.edu2电子邮件地址：arnab@cs.stanford.edu3电子邮件地址：mukunds@cs.stanford.edu1571-0661/© 2009 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2009.02.07494J.C. Mitchell等人/理论计算机科学电子笔记234（2009）93以及在相同环境中运行的任何其他协议可能需要的属性。在过去的工作中研究的各种版本的PCL已经被证明是合理的协议运行，使用任何数量的主体和会话，在符号模型和（目前的逻辑子集）在更传统的密码学假设[8]。PCL证明方法使用一阶逻辑的扩展，其中包含用于协议动作、时间推理、知识的公理和证明规则，以及称为诚实规则的特殊形式的不变性规则。在攻击者存在的情况下，诚实规则对于将关于一个角色的事实与其他角色的推断动作相结合至关重要。直观地说，如果Alice收到了一条发送给Bob的消息的响应，诚实规则捕获Alice使用Bob角色的属性来推理Bob如何生成他的回复的能力。粗略地说，诚实规则是说，如果一个属性φ被协议的所有角色所保持，那么如果鲍勃只执行协议的角色，φ被鲍勃的行为所保持PCL的一个基本特征是，不变量只通过推理协议指定的动作来证明，这些动作是协议诚实方执行的唯一动作;逻辑的形式避免了考虑攻击者动作的需要。因为诚实的主体不会被攻击者滥用他们的私钥（根据定义），所以诚实规则不涉及对私钥被泄露的情况进行推理。正如我们在第2.2节和第2.3节中讨论的那样，虽然不变量很容易计算，但检查它们是否成立是一个繁琐的过程，这使得不变量检查成为自动化的完美目标。这一点也被独立观察到[13]。在本文中，我们描述了一种自动建立一些不变量的方法，使用协议动作的逻辑编程公式，不变量本身，以及建立所述不变量的充分条件。因此，对于每个协议和不变量，我们的方法创建一个逻辑程序，限制使用否定，搜索可能违反不变量的协议属性。这样做的方式是，如果逻辑程序未能证明某个目标，那么不变量在PCL中是可证明的。因为我们的工作条件保证了PCL证明，并且PCL不需要对攻击者的行为进行显式推理，所以我们的逻辑程序不需要考虑攻击者的任何可能行为。我们主要感兴趣的不变量，写为逻辑的影响，因为这些经常出现在实际协议的案例研究。然而，这种形式的不变量提出了几个挑战。一是效率和正确终止我们最初的方法产生了小的逻辑程序，这些程序搜索违反充分条件的情况，但执行时间长得不合理。 对于可靠性，我们需要确保对于满足蕴涵的前件的所有可能方式，后件都成立。这导致我们使用逻辑编程与否定作为失败，这进一步加剧了效率问题。 我们仍然取得效率的主要原因如下。我们使用SLD-resolution[17]作为决策过程的基础。在PCL中，每个程序变量只定义一次。这就在我们的逻辑程序的规则之间产生了互斥;在目标搜索的任何一点上，至多有一条这样的规则是适用的。 此外，我们的J.C. Mitchell等人/理论计算机科学电子笔记234（2009）9395PCL证明系统的编码确保不成功的搜索路径快速终止。因此，我们之所以获得计算效率，与PCL程序的结构和建立不变量所需的PCL证明系统密切相关。虽然在有用的情况下是有效的，但我们的方法并不完整，因为它使用了PCL证明存在所不必要的充分条件。此外，如上所述，关于许多重要不变量的推理不涉及密码学性质，因此我们的技术适用于密码学的符号和计算模型。虽然我们在这里不试图解决最近在[2]中提出的所有批评和概念上的误解，但我们确实注意到，在将PCL的一部分翻译成逻辑编程的过程中，本文确实澄清了一些涉及PCL项代数和隐式类型限制的语法问题。2预赛我们首先简要描述了协议组合逻辑（PCL），以帮助不熟悉PCL的读者阅读本文。然后，我们讨论了著名的传输层安全（TLS）协议，我们使用它作为一个运行的例子在整个文件。熟悉PCL和使用PCL分析TLS的读者可以跳到第3节。2.1PCL概述协议组合逻辑（Protocol Composition Logic，PCL）[10，3，5，7]的框架包括用于定义协议角色的协议编程语言，用于建立协议属性的证明系统，以及将证明规则与协议程序和逻辑的语义相关联的可靠性定理。PCL中的证明在标准符号模型中是可靠的;在这个模型中，所有的加密原语都被假设为完美的，例如攻击者只有在拥有适当的密钥时才能解密加密的消息。协议由一组角色定义，每个角色指定一系列由诚实代理执行的动作。在PCL中，协议角色使用基于[ 10 ]的简单可能的协议动作包括随机数生成、签名和加密、通信步骤以及通过模式匹配的解密和签名验证。程序还可以依赖于输入参数（通常由上下文或设置操作的结果确定），并为后续操作提供输出参数。线程是协议角色的实例。协议在给定时间的执行状态是在该时间之前发生的序列事件。事件可以是通信步骤（发送/接收）或内部操作（加密、签名、散列等）。大多数协议证明使用形式为θ[P]Xφ的公式，这意味着从公式θ为真的状态开始，在线程X执行动作P之后，公式φ在96J.C. Mitchell等人/理论计算机科学电子笔记234（2009）93结果的状态。 公式φ通常对动作的时间顺序（用于声明认证）和/或各种主体可访问的数据（用于声明保密性）进行断言。 作为一种符号约定，执行此操作的时间（操作的序列）X是写X的时间。在这场比赛中，我们列出TLS身份验证的证明。证明系统用公理和证明规则扩展了一阶逻辑，这些公理和证明规则用于协议操作、时间推理、密码原语的属性，以及一种称为诚实规则的程序不变性规则的特殊形式，在2.3节中描述。我们在下面列出我们在本文中使用的公理。对于公理和规则的可靠性的证明，我们请读者参考[6，11，7]。AA1T[a]XaAA2Start（X）[]X<$a（X）AA3<$Send（X，t）[b]X<$Send（X，t）如果σSend（X，t）AA4T[a;· ··;b]Xab所有替换的σbAN1New（X，x）<$New（Y，x）<$X=YAN2T[newx;]XHas（Y，x）<$（Y=X）AN3 T[newx;]XFresh（X，x）AN4新鲜（X，x）再生（X，x）VERH ones t（X）X. Sign（X，x）P1Persist（X，t）[a]XPersist（X，t），对于Persist∈{Has，FirstSend，a，Gen}。P2Fresh（X，t）[a]XFresh（X，t），whee re t/della.J J JFresh（X，t）[senddt;]XContains（t，t）FirstSend（X，t，t）JJ JJ JJFirstSend（X，t，t）<$ a（Y，t）<$X/=Y<$ Contains（t，t）<$ Contains（t，t）JJJ>发送（X，t）

下载后可阅读完整内容，剩余1页未读，立即下载