复杂密码协议的形式化MSR语言框架

理论计算机科学电子笔记40（2001）网址：http://www.elsevier.nl/locate/entcs/volume40.html44页安全协议Iliano Cervesato1，2ITT工业公司亚历山大，弗吉尼亚州22303-1410 -美国摘要MSR语言在过去已经成功地用于证明根据Dolev-Yao抽象建模的安全协议的不可判定性结果。 在本文中，我们将这种形式主义修改为复杂密码协议的灵活规范框架。更具体地说，我们为它配备了一个可扩展的类型基础设施，该基础设施基于具有子排序的依赖类型，可以优雅地捕获和执行对象之间的基本关系，例如公钥及其逆之间的关系。我们还介绍了内存谓词的概念，其中主体可以存储角色终止后仍存在的信息。这些谓词允许指定结构化为子协议的协调集合的复杂协议。此外，它们允许使用与任何其他角色相同的语法来描述不同的攻击者模型。我们证明了这种可能性和我们的类型系统的精度，提出了两个形式化的Dolev姚入侵者。我们讨论了两个执行模型，这个修订版的MSR，一个顺序和一个并行，并证明后者可以模拟前者。1介绍MSR语言[8，15，9]是一种形式主义，旨在给出计算机安全的Dolev-Yao抽象中的身份验证协议的简单规范[20，14]。它将协议建模为一组参数化的多集重写规则，并将存在量化作为一种设备来保证新生成数据的新鲜度。事实上，MSR是MultiSet Rewriting的缩写。通常，多集（也称为包）是一种代数结构，它通过不折叠对象的多次出现（它们可以1部分由NSF基金INT 98 -15731“形式验证的逻辑方法”支持of2电子邮件地址：iliano@itd.nrl.navy.mil2000年1月，出版社dbyElsevierScienceB。 V.操作访问和C CB Y-NC-ND许可证。切尔韦萨托2或者被视为无序序列）。角色，即由参与协议运行的每个主体发送或接收的消息序列，被表示为通过专用角色状态谓词进行通信的多集重写规则，该谓词将控制和数据传递给序列中的下一个规则。规则对状态进行操作，定义为对传输中的消息建模的一阶原子公式的多个集合，当前存在的角色状态谓词，以及建立不可变关系的持久信息，例如键与其逆之间的关系。MSR已成功地用于证明认证协议的正确性通常是不可判定的[8，15]。此外，我们还证明了它在表达能力上与安全协议的流行规范语言的扩展（如串空间[16]）的实质等同在实践方面，MSR以底层CIL中间语言的形式为CAPSL认证协议验证工具提供了动力[13]。尽管取得了这些成就，MSR是一种非常低级的语言，不适合直接指定安全协议。特别是，规则中存在的持久信息谓词上的松弛约束使得设计自动化支持过程变得困难，并且关于规范的推理容易出错。这些谓词与基本类型一起描述了对象之间的关联，例如密钥与拥有它的主体之间的关联;可以想象，这可以用来捕获诸如试图访问未经授权的密钥之类的错误。另一个缺点是其严格的规则格式，这导致了冗长的规范（以及随之而来的模型检查开销[12]）。最后，[8，15，9]中定义的语言缺乏描述所需的表达能力，但却是最简单的身份验证协议。特别是，任何由子协议集合构成的协议都不在这种语言的范围之内。在本文中，我们提出了一个彻底的重新设计MSR旨在建立它作为一个可用的规范框架复杂的安全协议。主要的创新包括采用了一种灵活而强大的类型化方法，该方法包含了持久信息谓词，并引入了记忆谓词，大大拓宽了这种形式主义的适用范围。这种语言的详细定义也允许精确描述其执行语义。我们称这种形式主义为类型化的MSR，或者当不可能出现歧义时就称之为MSR它完全包含了我们以前对这种语言的介绍[8，15]。我们的新语言的类型注释，从具有子排序的独立类型的理论中得出，例如，通过根据它们所属的主体或根据它们的预期用途区分键，可以实现精确的对象分类。因此，任何两个主体的公钥都可以被分配不同的类型，而这又与它们的数字签名密钥不同。协议规范，在MSR中称为协议理论，是强类型的，我们已经设计了静态捕获类型违规的算法切尔韦萨托3例如使用共享密钥执行公钥加密[4]。我们的类型基础设施可以指出更微妙的错误，例如主体试图用不属于他的密钥加密消息。在[3]中分析了实施这种访问控制策略的过程。内存谓词允许主体在角色执行过程中记住信息。它们的存在为协议的规范化打开了大门，这些协议被构造为协调子协议的集合。这种新的可能性在[5]中得到了体现，在那里我们形式化了Neuman-Stubblebine重复认证协议[21]，它超出了我们以前版本的MSR的范围。内存谓词的一个特别有趣的应用是它们在入侵者模型的具体化中的作用，协议将根据入侵者模型进行分析。事实上，我们的增强版MSR允许将攻击者表示为通过专用内存谓词进行通信的分布式协议。我们通过给出通用Dolev-Yao入侵者的两个规格来验证这种技术。我们应该强调，这些规范完全在我们目前版本的语言范围内。的MSR，而攻击者对应于一组规则，没有完全遵循[8，15，9]中的协议语法。本文给出了MSR的详细定义，使其执行语义得到了统一的描述。我们提出了两个模型：一个基于规则的顺序应用，而第二个允许独立的规则并行触发。我们证明，后者模式可以模拟顺序执行。虽然这一结果并不特别令人惊讶就其本身而言，给出完全形式化证明的能力进一步确立了我们语言精确定义本文的组织如下：在第二节中，我们定义了MSR的术语语言。第3节介绍了状态及其组件，第4节介绍了规则，角色和协议理论。在第5节中讨论了MSR的顺序和并行执行模型，并进行了相关分析。第6节用我们的语言形式化了Dolev-Yao入侵者模型的两个变体。最后，第7节对本文进行了总结，并提出了今后的工作方向2键入的消息在2.1节中，我们描述了构成MSR核心的消息或更一般的术语。然后在2.2节中，我们将介绍类型基础设施，使我们能够理解这些术语。我们将在第4节中定义协议规则时需要它们 我们在第2.3节中总结，指出了与MSR[8，9]上以前工作中使用的消息有关的主要差异。切尔韦萨托42.1消息通过将下面讨论的多个消息形成构造应用于各种原子消息来获得消息。我们将在本文中考虑的原子消息我们通过以下语法产生式来形式化原子消息的概念：原子消息：a：：=A（主体）| k (Key)| n (Nonce)| m (Raw datum)在这里和本文的其余部分，A，k，n和m将分别覆盖主体名称，键，随机数和原始数据。我们有时也会用B来表示一个主体。 虽然我们将在本文中的讨论限制在这些类型的原子消息，但应该注意的是，通过扩展适当的定义可以容纳其他类型的原子消息。我们将考虑的消息构造函数包括串联、共享密钥加密和公钥加密。总之，它们产生了以下信息的定义，或者更恰当地说，是一个术语。消息：t：：=a（原子消息）| x(Variables)|t1t2(Concatenation)|{t}k(Symmetric-key encryption)| {{t}}k(Asymmetric-keyencryption)我们将使用字母t，可能是下标和/或上标，以涵盖术语。注意，我们对共享密钥和公钥加密使用了不同的语法。我们可以识别它们，就像在许多方法中所做的那样。相反，我们选择区分它们，以显示我们技术的灵活性和精确性。同样，其他构造函数，例如数字签名和散列函数，可以通过扩展适当的定义来轻松容纳。我们没有这样做，因为列入这些问题会延长讨论时间，而不会引入实质性的新概念。类型元组（在第3节中讨论）和协议规则（见第4节）依赖于可能包含变量的对象，这些变量分别在类型检查（这方面在[4]中进行了形式化）和执行期间被实例化。参数信息允许变量，其中条款可能出现在第2.1节的信息中。我们将A（或B），k，n和m，不同的装饰，分别为原子常数或变量，分别是主体，键，随机数和原始数据。每当我们想要引用的对象不能是常量时（通常在切尔韦萨托5第5节的执行规则），我们将使用相应的串行字母：A（或B），k，n和m。相反，字母x、y和z将代表必须是可变的项。在某些情况下，我们需要引用可以是变量或原子消息常量的对象，但不能引用复合项。我们称这些项为初等项，用字母e表示，并作各种修饰。由于我们将在本文的其余部分中处理的大多数对象都包含变量，因此我们将使用“术语”（或“消息”）来指代到“参数项”（或“消息”）。每当我们处理不包含变量的术语时，我们将讨论2.2类型虽然类型在MSR的原始定义中扮演了非常温和的角色[8，9]，但它们是本文所提出的扩展的核心。 通过键入，我们可以强制执行基本的格式良好性条件（例如，如[4]中详细描述的，用于加密消息）。类型还提供了一种静态可检查的方式来确定复杂的需求，例如，没有主体可以获取他/她无权访问的密钥。这方面在[3]中进行了深入的分析。在我们目前的方法中，类型的核心作用可以通过它们继承并完整地取代原始MSR的最适合我们目标的类型机器是基于类型理论的概念，即依赖产品类型与子排序。我们将只介绍我们将使用的方面，并且只介绍我们需要它们的程度，而不是深入研究这种形式主义的定义和性质。特别是，我们不对这种类型理论进行深入的讨论;我们甚至将远离其语法的最奇特的方面。希望进一步理解这种形式主义的读者请参考[11，18，1，22]。类型是用于对其他语法表达式（如术语）进行分类的语法结构。通过这样做，他们给了它们一个含义，例如，我们解释为键的对象不是nonce。 每当在期望随机数的情况下使用密钥，由于该术语的含义被违反，所以出现了错误。我们将在本文中使用的类型总结在以下语法中：类型：τ：：=principal（Principals）|随机数（Nonce）|shK AB（共享密钥）| pubKA（公钥）| privKk（私钥）| ATM（Atomic Messages）| msg（消息）切尔韦萨托6在 续 集 中 ， τ ， 可 能 有 不 同 的 装 饰 ， 将 代 表 一 个 类 型 。 不 用 说 ，“principal“和“nonce“类型接下来的三个产生式允许区分共享密钥、公钥和私钥。依赖类型提供了一种简单而灵活的方式来表达键与其所有者或其他键之间的关系。给定主体这里，密钥的类型取决于特定主体类似地，常量我们再次使用依赖类型来表示公钥与其逆密钥之间的关系。继续最后一个例子，“k“的逆“atm“类型例如，这个语句意味着一个nonce我们通过在类型之间施加子排序关系来适应这种形式的分层多分类。我们通过下面的判断来形式化这个关系：τ：：τJτ是τJ本文中，子排序关系要求主体，现时值和键的类型是atm的子类型。就原子术语而言，它的扩展是通过以下规则来表达的：ss prss nnncprincipal：：atmnonce：：atmshKAB：：atmSSSHKpubKA：：atmss pbKprivKk：：atm党卫军pvK这些规则是参数化的，因为例如ss shK建立了atmmsg类型用于对一般消息进行分类。由于随机数、密钥和主标识符通常是消息的一部分，我们将atm作为msg的一个子类：atm：：msgSS ATM同样，上面的类型和子排序规则应该被认为是这是我们方法的合理实例，而不是方法本身。其他模式可以通过定义适当的类型以及它们如何相互关联来指定。例如，可以采用类似于“pubK A“和“privK k“的专用从属类型来容纳数字签名在另一种情况下，应用程序可能会发现将上面的每个键相关类型视为通用键类型的子类型（例如“key“），进而视为msg的子类型是很方便的作为最后一个例子，我们可能想要定义不同的类型，切尔韦萨托7·我们的优势长期密钥，并使它们不是MSG的子类别，以这种方式禁止 这些可能性在[4，5]中有举例说明。在本节的第一部分，我们介绍了术语和用于对其进行分类的类型。现在我们将介绍类型规则，这些规则将允许我们确定根据术语语法构建的表达式是否可以被视为基础消息（更一般地说，给定的无变量表达式是否具有某种类型）。下面的规则系统地将复合术语的可类型性降低到其子术语的有效性。这对于构造函数来说已经足够了，但是原子消息需要被特殊对待，除非我们愿意在每次为协议建模时为它们编写新的规则。规则与实际原子消息的独立性是通过签名的概念实现的。签名（签名）是将原子消息映射到其类型的有限声明序列。更正式地说，签名：：：=·（空签名）|Σ, a: τ (Atomic message declaration)| （...））的方式最后一行中的点表示这个定义是不完整的：我们将在下一节中扩展它。我们假设签名中的每个原子消息只声明一次。我们还经常从非空签名中省略前导只有当结果序列本身是一个签名时，这个操作才被定义（特别是它不应该包含对同一个常量的多个声明考虑到目前为止介绍的概念，为消息和我们描述的其他类型定义一个有意义的类型系统是相当容易的。为了实现这一目标，我们将依靠以下消息类型判断：Σ►t:τ Term t has type τ in signatureΣ所有复合术语都有msg类型，前提是它们的组成子消息类型正确。这意味着串联（t1t2）的子项本身就是消息。另一方面，加密消息{t}k的明文部分t应该具有msg类型，但是k应该是两个主体之间的共享密钥。使用公钥加密的项（形式为tk）的处理方式类似。这种直觉在下面的消息类型规则中得到了正式的体现：留言1：留言2：留言mtp cnc留言1t2：msg切尔韦萨托8留言：msg留言：shKABmtp ske联系我们留言：msg留言：pubKAmtp pke登录{{t}}k：msg这些规则是参数化的，正如它们所包含的众多元变量所证明的那样，但也是假设性的，因为结果的有效性依赖于前提的有效性。下一条规则将检验项t是否具有类型τ简化为检验它是否对于τ的某个子排序具有类型τJ。通过这种方式，我们可以使用一个nonce或一个key，其中需要一个msg类型的对象。正式规则是如下所示：时间：τJτJ：：τmtp ss时间：τ最后一个术语类型规则处理基本消息组件。如果手头的签名包含声明“a：τ“，则原子消息a具有类型τ类型τ的有效性通过验证签名的有效性来独立检查[4]。MTP A（，a：τ，J）a：τ这就结束了本文所需的打字规则的介绍。应该注意的是，这些规则并不保证签名声明遵守类型化策略：例如，没有任何东西强制规则mtp ske的最右边前提中的类型的参数A和B成为主体。虽然良好类型的签名是正确规范的重要组成部分，但我们不需要在本文中要求它们。这些省略的类型规则可以在[4]中找到，同时还有设计用于验证MSR协议规范的每个元素的过程。为了方便读者，我们将本文中提出的所有规则收集在附录A中。2.3变化我们现在将比较上面的术语基础设施与早期版本的MSR[8，9]中使用的消息概念主要的分歧涉及类型和它们的使用方式。(i) 在结构上，MSR的原始表示涉及所谓的简单类型，即不依赖于术语的类型。这些类型将允许将对象区分为键、随机数、消息等（分类法是开放式的），但不允许任何精细分类[7]。子分类引入了一些可扩展性。现在通过类型捕获的大部分信息，特别是它们对术语的依赖性，都是通过“持久谓词”来表达的切尔韦萨托9具体化和复杂的推理。这些实体已被删除。(ii) 类型在[8，9]中扮演了一个相当不重要的角色：常量被赋予了类型，但规则本身并不携带这样的信息。 此外，没有明确提出类型系统来验证术语或规则。 类型化是本文中提出的语言的核心：每个对象都是类型化的。事实上，我们的方法不仅允许验证基本的格式良好条件（例如，没有消息是用随机数加密的）[4]，而且类型提供了一种静态可检查的方式来执行复杂的要求，例如，没有主体使用他/她无权访问的密钥[3]。(iii) 在本文中，我们做了共享密钥和公钥加密之间的语法区别。虽然在[8，9]中没有出现，但我们可以很容易地区分MSR早期版本中的两种加密形式。3消息谓词和状态正如我们很快就会看到的，状态是专门的原子一阶公式的集合。国家是MSR中的一个基本概念。事实上，它们是协议执行快照的中心组成部分。它们是通过重写规则转换的对象，以模拟消息交换和信息更新。最后，与执行跟踪一起，它们是协议分析所基于的假设场景。在本节中，我们将形式化MSR中状态的概念，以及实现它所需的结构。在3.1节中，我们将介绍消息元组和它们的类型概念。然后在3.2节中，我们讨论出现在状态中的消息谓词，并在3.3节中定义状态。3.1消息元组和依赖类型我们很快就会看到，消息谓词是原子一阶公式，其参数为零或多个项。在这一节中，我们关注的是元组概念的形式化，并为它们提供合适的类型消息元组是一个有序的术语序列。它被简单地定义如下：消息元组→t：：=·（空元组）| t,→t(Tupleextension)我们通常会在元组不为空时省略前导·将元组的类型定义为它的组件的类型的序列是很诱人的。因此，如果A是一个主体名，kA是A的公钥，元组（A，kA）的类型为这种结构切尔韦萨托10××××允许我们将一个通用主体与A的公钥相关联：如果B是另一个主体，那么（B，k A）也将具有此类型。我们通常需要更严格的关联，例如主体和它自己的公钥之间的关联。 为了实现这一点，我们将依赖于依赖类型元组的概念。在这个例子中，元组（A，kA）将被属性化为类型3通过收集每个组成消息的类型，我们确实将一个类型归属于一个术语元组，但是我们用变量来标记这些对象，以便在以后可能依赖于它们的类型因此，依赖类型元组是一个有序的类型序列，参数化如下：Type元组→T：：=·（空元组）| τ(x)×→τ(Ty petupleextension)在这个定义的第二行中，笛卡尔乘积系统左边的符号（x）将ty pe元组→τ中的变量x绑定到它的rig ht。与quantifier类似，τ（x）是binder。 中未绑定的变量 据说这条路是免费的。我们经常会对封闭类型元组感兴趣，它的所有变量都是绑定的。绑定的作用域是绑定操作所跨越的表达式。 类型元组组件的范围扩展到其右侧的整个类型元组Giv enadepnttupletypeτ（x）当变量x在→ τ中不发生时，我们将丢弃标签（x）。由此产生的简化符号τ×→τ将有助于在可能的情况下写出更清晰的描述。 至于术语元组，我们将在方便的时候省略前导“·”。3.2消息谓词可以进入状态或重写规则的谓词有三种：• 首先，谓词N（）以分布式方式实现公共网络的内容：对于当前正在传输的每个（基础）消息t，状态将包含形式为N（t）的组件• 第二，活动角色依赖于多个角色状态谓词，通常一个谓词对应于其中的每个规则，其形式为L1（，.，），其中L是唯一的识别标记。 这个谓词的参数记录了到当前点为止角色执行的3我们的依赖型元组在类型论中通常称为弱依赖和社区，我们写为“principal（A）pubK A“的依赖类型元组的标准表示法是“principal A：principal。pubKA“。我们相信，我们的语法可能会更清楚，本文的目标受众切尔韦萨托11·• 第三，主体A可以将数据存储在形式MA（，.，），它在角色终止后仍然存在，并且只要主体保持不变，就可以在不同角色的执行中使用。熟悉我们以前关于MSR的工作的读者会注意到与[8，9]中给出的定义有关的许多分歧。内存谓词确实是新的。它们旨在对需要在角色执行过程中保持数据私有的情况进行建模：例如，这允许主体记住其身份证，或公平交换协议的受信任第三方，以避免从中止的交易中进行欺诈性恢复。与早期工作的另一个不同之处是没有保留入侵者知识的专用谓词。然而，这可以很容易地使用内存谓词实现，正如我们将在第6节中看到的那样每个协议都依赖于公共网络。因此，我们将在我们的语言中硬连接网络谓词N（）。本地状态和内存谓词是不同的：它们是在每个协议的基础上定义的。这类似于主体和键。因此，我们保持一般性，宣布它们为签名的一部分。我们现在可以完成签名的定义如下：签名：：=·（空签名）| Σ, a: τ(Atomic message declaration)| Σ,Ll:→τ(Localstatep redi cated ecla ration)| Σ,M:→τ(Memoryp redi cated ecla ration)3.3国多重集是一个对象的集合，其多重性很重要，但其顺序无关紧要。我们可以将它们看作无序的序列，或者看作允许同一元素的多个实例共存（并且禁止折叠它们）的集合。状态是基态谓词的有限多集。状态的语法通过以下语法部分地形式化状态：S：：=·（空状态）| S, N (t)(Extension with a network predicate)| S,Ll(→t)(Extensionwitharolestatep redi cate)| S,MA(→t)(Extensionwithamemoryp redi cate)至于签名，我们将省略前导“ 打破上述语法产生式所强加的严格格式，抽象出一个状态的成分谓词的顺序，把它们当作一个多重集合来处理，这将是很方便的。协议规则转换状态。它们通过识别一些组件谓词，从状态中删除它们，并添加其他通常相关的状态元素来实现。重写规则的前件和后件切尔韦萨托12因此嵌入子状态。但是，为了适用于各种状态，规则通常包含在应用时实例化的变量。这需要状态和消息谓词的参数化概念在大多数情况下，这简化为在嵌入项中承认变量。然而，角色状态谓词需要在现场创建，以避免干扰。我们通过引入变量（记为L）来实现这一点，这些变量在应用过程中被实例化为实际的角色状态谓词。这使得我们的语言是弱二阶的，尽管我们可以通过将角色状态谓词Ll解释为由标签l索引的符号L来轻松地将其降低到一阶，该标签l在规则中被保持为变量。 然而，我们选择更直接的解决方案，因为它没有任何缺点，并且允许稍微简单的定义。3.4变化在本节的最后部分，我们将分析国家概念和上面定义的相关概念与MSR最初定义中的类似实体之间的主要区别[8，7]。类型化在这个层面上构成了一个微小的区别，因为MSR的两个版本都依赖于类型化的谓词名称，尽管在[8，7]中很少使用这个方面我们目前使用的依赖类型元组主要是我们采用依赖类型来分类术语的结果。主要的分歧在于内存谓词的引入和的持久信息和区分入侵者的知识谓词的状态。(i) 在MSR的早期版本中，主体无法在角色执行过程中记住数据：角色状态谓词是角色实例的本地谓词，并且网络消息不用于存储私有信息。内存谓词在角色终止后仍然存在。如前所述，这在建模需要记住跨角色执行的信息的场景时很有用：例如，这允许主体记住其身份验证票证，或公平交换协议的受信任第三方，以避免从中止的事务中进行欺诈性恢复。内存谓词的另一个新的重要用途是在由许多子协议组成的协议建模中：这些谓词允许子协议相互调用并共享数据。(ii) 在上述定义中，没有任何持久信息的痕迹，这些持久信息形成了[8，7]中MSR状态的不可变部分。这些谓词的功能现在由我们更新的框架的强类型策略执行，特别是我们对依赖类型的依赖。(iii) 最后，我们应该指出缺少一个专门的谓词来保存入侵者我们早期工作的这一方面现在可以通过内存谓词透明地实现，我们将看到切尔韦萨托13→∀ ∀→在第6节。4多集重写理论在过去，密码协议经常被呈现为在“正常”运行期间传输的消息的时间序列。最近的支持者拥护一种将有关各方置于前台的观点。一个协议是一个独立角色的集合，这些角色通过交换消息进行通信，而不涉及任何类型的运行。 一个角色一个所有者，执行它的主体，并指定他/她将发送的消息序列，可能是为了响应接收到某种预期形式的消息因此，角色可以被看作是一个反应系统。MSR采用并正式化了这一观点。 它将协议表示为一组我们也称之为角色的语法实体。一个角色本身就是一个多集重写规则的参数化集合，这些规则对预期的消息接收和相应的传输进行编码。规则触发模拟接收（和接受）消息和/或发送消息，这是最小的执行步骤。本节定义了规则、角色和协议理论。更具体地说，在4.1节中，我们介绍了规则及其组成部分。角色定义见第4.2节。然后，在4.3节中，我们将注意力转向协议理论，这是我们对协议的表示。最后，在第4.4节中，我们预见了积极角色的动态概念。角色和协议理论将在第5节中进一步讨论，重点是执行。第4.5节研究了这些定义与我们最初提出的MSR的不同之处。4.1规则规则的核心具有“lhs rhs“的形式规则是将一个状态转换为另一个状态的基本机制，因此也是协议执行的模拟机制：只要前件使协议规则参数化是很方便的，这样相同的规则可以用于许多稍微不同的场景（例如，不固定中间人或随机数）。因此，一个典型的规则将提到变量x1，...，在执 行 期 间 将被实例化为实际项的 。类型通用量化器可以方便地表达这一事实，以便规则采取以下形式：“x 1：τ 1。...x n：τ n。（lhs rhs）"。 下面的语法更准确地表达了这个想法：规则：r：：=lhs→rhs（规则核心）| ∀x : τ. r（参数闭包）规则中使用的通用量化器绑定它们所应用的变量切尔韦萨托14自由变量可以出现在规则的构造中，但是角色本身应该绑定所有的变量（这是由类型规则强制执行的）：它们是封闭的。上述产品中所有绑定器的作用域跨越整个规则。如果我们把变量看作占位符，那么绑定器规定哪些占位符必须用相同的术语（或谓词名称）实例化。变量名实现了这种关联。除了可能的助记功能外，变量名本身并不重要，只要不引入与自由变量的冲突，变量名可以被任意字符串替换（一种称为变量捕获的效应：重命名会导致自由变量成为绑定）。 方便的是（例如，当应用替代时）允许 谓词序列中绑定变量的隐式无捕获重命名（这在类型理论界称为α转换规则的左侧或先行项是参数消息谓词的有限集合，因此由以下谓词序列语法给出：谓词序列：lhs：：=·（空谓词序列）| lhs, N (t)(Extension with a network predicate)| lh s,L(→e)(Extensionwitharolestatep redi cate)| lh s,MA(→t)(Extensionwithamemoryp redi cate)注意到规则前件和一般的谓词序列与状态（见3.3节）的区别主要在于角色状态谓词的有限实例化：在规则中，这些对象由一个角色状态谓词变量组成，该变量应用于由其类型指定的尽可能多的基本术语。回想一下，基本项要么是变量，要么是原子消息常量。网络和内存谓词通常包含参数项，但不一定是原始变量作为参数。规则的右边，或后件，由一个谓词序列组成，该序列可能由一个有限的新数据声明字符串（如随机数或短期键）前缀。我们依靠存在量化符号来表达数据生成。我们有以下语法：右侧：rhs：：=lhs（消息谓词的序列）| ∃x: τ. rhs（新数据生成）前面讨论的新鲜和绑定变量的概念在这里也适用。请注意，这些量化器的范围仅限于当前规则的右侧。后面的规则可以通过引入适当类型的通用量化器来引用这些变量创建的值：同步通过它们在角色状态谓词中的出现来确保。我们在[6]中已经表明，当在逻辑中编码MSR时，我们的新数据标记确实由存在量化呈现。切尔韦萨托15∃4.2角色角色状态谓词记录规则访问的信息。 它们也是一种机制，通过这种机制，一个规则可以在同一角色中执行另一个规则。 依赖于一组固定的协议范围的角色状态谓词是危险的，因为它可能会导致同时执行的角色的不同实例之间的意外干扰。相反，我们通过要求每次执行角色的新实例时使用新名称，使角色状态谓词成为角色的本地谓词。与规则结果的情况一样，我们通过使用存在性量化器来实现这一效果：我们通过形式为“L：→ τ“的声明来预先定义应该共享相同的角色状态谓词L的规则p的集合，其中yped存在性量化器表示L应该使用ype→τ的新角色状态谓词名称来安装的事实。同样，MSR在逻辑中的翻译将这些声明解释为存在性量化[6]。有了这种见解，下面的语法定义了规则收集的概念：规则集合：ρ：：=·（空角色）| ∃L:→τ. ρ（随机状态预分配）|r，ρ（带规则的扩张）应该注意到，该定义允许角色状态谓词参数声明和规则在规则集合中交错。 我们 然而，通常将集合划分为声明所有角色状态参数的前导和列出构成角色的规则的主体一个角色是角色所有者A和规则集合ρ之间的关联。有些角色，例如实现服务器或入侵者的角色，本质上绑定到几个特定的主体，通常只有一个。我们称之为锚定角色，ρA在这里，角色所有者A是一个实际的主体名称，一个常量。其他角色可以由任何主体执行。在这些情况下，A必须作为绑定到角色的参数。我们使用以下语法来表示这些通用角色：ρα其中隐式类型的通用量化符号意味着A应该在ρ中的任何规则执行之前被实例化为主体，并将绑定的范围设置为ρ。注意，在这种情况下，A是一个变量。我们有时会用字母ρ来表示这两种角色，但会有不同的下标。切尔韦萨托164.3协议理论一个协议理论，写作P，是一个有限的角色集合协议理论：P：：=·（空协议理论）| P，ρA（具有通用作用的扩展）| P，ρ A（具有锚定角色的扩展）应当注意到，我们并没有为闯入者作出任何特别规定。攻击者被表示为一个或多个角色，其方式与协议中更合法的消息交换相同。我们将在第6节说明如何对标准的Dolev-Yao入侵者和它的一个变体实现这一点。4.4积极作用正如我们将在第5节中看到的，给定角色的几个实例，可能在不同的规则中停止，可以在执行过程中的任何时刻出现。我们记录当前正在使用的角色实例、每个实例停止的点以及在活动角色集中执行它们的主体。这些对象是活动角色的有限集合，即部分实例化的规则集合，每个都用主体名称标记。以下语法描述了它们的宏观结构：活动角色集：R：：=·（无活动角色）| R, ρA(Extension with an instantiated role)符号ρA让人想起锚定角色。主动角色实际上更自由，因为一些角色状态谓词符号以及它们的参数可以被实例化。直观地说，ρA是实例化某个角色的内容的结果，A是它的当选所有者。4.5变化应该注意的是，上述规则的语法比MSR的原始定义要自由得多[8，9]。我们将在本节的其余部分我们首先注意结构变化（第一至第三项然后，我们继续讨论一些关于角色状态谓词的评论（项目(i) 协议理论在[8，9]中被定义为规则的集合，对于这些规则，由其角色状态谓词生成的图是非循环的（参见下面的x项以了解更多细节）。 每个连接的组件对应一个角色。除了这个约束，角色内的规则是独立的。我们目前的提法基本上保留了这一方面，但切尔韦萨托17我们对角色的定义通过使用角色状态谓词声明作为排序设备来允许线程规则。此选项很少使用，因为通过适当地使用角色状态谓词可以更简单地实现此效果。(ii) 在[8，9]中，所有变量都在规则的头部隐含地普遍量化，除非在结果中标记为新数据。这里，这些变量由类型化的通用量化器显式地引入。就类型检查[4]和访问控制[3]而言，显式量化简化了规则分析。更重要的是，它声明了变量的类型，这是正确执行协议所必需的（在5中有更多关于这方面的内容）。(iii) [8，9]中唯一的量化器出现在规则结果中，目的是引入变量，用新数据实例化。依赖类型的采用使这种机制更加强大。例如，我们当前的模式允许服务器生成在两个特定主体之间共享的密钥。(iv) 正如已经观察到的，我们目前的公式没有使用[8，9]的持久谓词。正如我们所说的，这些对象曾经传递的信息并没有完全被MSR的类型系统捕获。(v) 内存谓词是一个新特性。如前所述，它们在需要跨角色执行记住数据时非常有用，例如，当一个子协议可以在某个初始化阶段后重复执行时。(vi) 任何数量的网络谓词都可以出现在规则的前件和后件中。最初的定义允许每个规则最多一次这样的谓词，要么在左手边（在“接收”规则中），或在右手边（用于“发送”规则）。Denker等人[12]表明，只要满足一些简单的条件，一系列连续的消息接收规则，然后是一系列连续的传输规则，就可以完全折叠成一个单一的规则。这显然是对我们先前建议的保守扩展。除了减少协议规范的长度外，合并规则的优点在于它在模型检查协议时产生了巨大的开销减少。(vii) 在[8，9]中，除了激活角色的单个“角色生成规则”之外，每个规则在每一侧都包含一个角色状态谓词。相反，上面的产生式在任何一方都允许零个、一个或多个这样的谓词。这种定义简化了角色的语法规范。然而，我们将非常有限地使用这种额外的表达能力。在规则的左侧或右侧具有多个角色状态谓词似乎并不特别有用，因为这些谓词的参数收集角色的当前执行线程中的主体已知的的先行词切尔韦萨托18角色中的第一个规则不能合理地提及任何角色状态谓词，因为它的左侧不能匹配任何状态。 的先行词其它规则通常将具有用于同步的这种谓词，尽管这不是强制的。出于同样的原因，规则的结果通常包含角色状态谓词。这种做法的自然例外是角色的最终规则，它不需要为进一步的同步做出规定。(viii) [8，9]中允许的角色状态谓词符号是常量而不是变量。我们现在倾向于使它们对于规则的每个实例化都是唯一的，以避免干扰的可能性（尽管我们没有这样的现象是有害的例子(ix) 除了[7]之外，我们以前的工作没有提到任何角色状态谓词作为区别角色所有者的参数。这些早期版本的MSR不需要积极依赖于角色所有者来实现其目标，即研究发现攻击的可判定性，一个协议。因此，没有特别强调这一概念。当试图实施访问控制时，这些信息变得至关重要，如[3]所述。(x) 对于任何给定的角色，研究这样一个图是很有趣的，它的节点是它的角色状态谓词，它的边将每个规则的左侧谓词链接到右侧谓词。在[8，9，6]中，我们要求这个图是一个上半格，特别是它有一个单一的入口点，是非循环的。这是研究协议复杂性的关键假设[8，15]。在这里，我们从角色的语法中删除了这个条件，但是我们的触发规则实际上会在执行时实现类似的约束(xi) 我们以前的工作[8，9]没有积极作用的概念： 以来角色状态谓词符号是常量，规则不能在角色内串接，每个规则都必须是一个独立的对象，只要它的前件与当前状态匹配，就可以应用。本章中提出的更复杂的模式需要记住当前使用的角色，以及它们是如何实例化的。这就是主动角色集的目的。必须注意到，这些实体与[9]中研究的剩余链的概念密切相关，作为安全协议链规范的执行模型的一部分[16]。5方案执行在本节中，我们将定义MSR的执行模型。更确切地说，我们首先在5.1节中概述了普遍存在的替代概念的定义然后，我们将在第5.2节中介绍基本的一步规则应用及其顺序迭代。在5.3节中，我们扩展了这个概念，允许并发规则触发。我们在5.4节中证明了并行发射的可容许性我们切尔韦萨托19在第5.5节结束时，讨论与先前版本的MSR相比的主要变更。5.1取代在本节中，我们将介绍在下面的执行规则中使用的替换概念我们主要关注这个操作的语法。其相当标准的定义见附录A.3。给定一个变量x和一个对象O，该对象可以将x作为参数，我们将O中的项t替换为x表示为[t/x]O。就执行规则而言，实例化项t将始终是基础，因此替换的实现不需要采取旨在避免变量捕获的特定规定（即t中的自由变量可能意外地成为O中的绑定的风险）。 参数对象O我们将在其他项stJ，项元组→t，typesτ，typ e元组中进行测试→τ，谓词序列lhs，right-手边rhs，规则r和规则集合ρ.总之，我们将遇到以下形式的替换：[t/x]tJ[t/x]→t[t/x]τ[t/x]→τ[t/x]lhs [t/x]rhs [t/x]r[t/x]ρ请注意，为了简单起见，我们重载了方括号表示法来表示替换操作对属于不同句法范畴的对象的应用。我们只需要定义在可能将x作为自由变量的对象中用t替换x。这就是为什么我们不包括协议理论，状态和主动角色在上面的列表中。除了术语变量，规则集合还包含第二种参数，即角色状态谓词符号，我们用字母L表示，有不同的装饰。在执行过程中，我们需要将它们实例化为Ll 形 式的常量，其中l是一个标签。我们扩展了我们的语法，写[Ll/L]O，用于在对象O中用Ll替换变量L。该操作适用于左侧lhs、结果rhs、规则r和规则集合ρ：[Ll/L]lhs[Ll/L]rhs[Ll/L]r[Ll/L]ρ应该注意到，虽然L代表谓词符号，但它永远不需要被实例化为比常数更复杂的东西。我们的符号的更高或更小的值只是显而易见的。同样，这些操作的定义可以在附录A.3中找到5.2连续击发执行涉及使用协议理论从状态S描述的情况移动到状态SJ建