网络安全协议的形式化分析与验证 作者 李建华 第四章 基于定理证明的安全协议分析方法.pptVIP

第4章 基于定理证明的安全协议分析方法 基于模态逻辑技术的安全协议分析方法存在规则不完善、语义不精确等问题， 基于状态检测的安全协议分析方法总是面临着状态空间爆炸问题的困扰。 为此，出现了多种基于定理证明的安全协议分析方法，包括归纳方法（Inductive Method）、串空间方法（Strand Space）等密码协议模型化方法，以及阶函数（Rank Function）、逼近法（Approximation）等安全属性的定理证明方法。 协议建模的主要过程就是将协议步骤表示为利用新的事件对迹所做的扩展。设服务器为常量S，A、B为主体名称（包括攻击者），则协议过程可依次描述为: 4.3.1 基本概念 在串空间模型中，主体间交换的所有消息组成了集合M，集合M中的元素称为项（Term），一个项可以包含多个子项（Subterm）， 表示t1是t的子项。 4.3.1 基本概念 定义 一个串空间为一集合∑，其迹映射为tr: ∑→(M)。其中，∑中的元素称为串。串空间?的构成包括以下几种情况。 1）节点是一有序对?s,i?， 且i为整数并满足 。节点的集合用N表示，节点 ?s,i?属于串s，每个节点只属于唯一的一个串。 2）如果n = ?s,i? ?N，则index(n) = i且 strand(n) = s。定义 ，即term(n)表示在s轨迹中的第i个带符号项。 3）如果 、 ，则表示 且 ，即节点n1发送一条消息a，该消息被节点n2接收。 表示两节点在各自的串之间产生了一条因果连接。 4）如果 ，则 表示n1 、 n2处于同一个串，且 。这表示是在串s中的直接因果前驱。 5）无符号项t在节点n?N中出现，当且仅当 。 6）无符号项t起源于节点n?N，当且仅当term(n)是正符号项；t ? term(n)；并且对于同一个串中节点n的所有前驱节点n’都有 。 7）无符号项t的起源是唯一的，当且仅当t起源于一个唯一的节点n?N。 8）无符号项t不生成，当且仅当不存在n?N，使得t在n中生成。 4.3.1 基本概念 如果项t唯一起源于一个特殊的串，则它可以被视为一个随机数或者一个会话密钥。 由上述定义可知，在串空间中，N 是包含边集合 和 的有向图。 串空间中的一个束（Bundle）是节点有向图的一个有限子图，其中的边用来表示节点间的因果依赖关系。 4.3.1 基本概念 4.3.1 基本概念 4.3.1 基本概念 4.3.1 基本概念 4.3.1 基本概念 4.3.1 基本概念 使用串空间模型构造简化的Needham-Schroeder公钥协议的串空间有向图 4.3.2 协议入侵者描述 4.3.4 协议分析举例 用基本的串空间模型分析密码协议的一般方法是： 首先，在束中根据需要构造一个节点集； 其次，考虑节点集的极小元属于哪一种串； 最后，分情况讨论其余的串，判断极小元是否属于这个串。如果极小元属于该串，则说明协议有缺陷。 以一个ISO候选认证协议为例，说明采用串空间的协议分析过程。 4.3.5 认证测试方法 认证测试方法是基于串空间模型的一种安全协议形式化分析与设计方法。 通过构造入测试、出测试和主动测试来验证协议的认证属性和特定消息的必威体育官网网址属性。 在认证测试中仍然使用到串空间模型中关于串、束的定义和性质，但是将必威体育官网网址数据作为构造测试的标准，构造测试分量，并根据测试分量的格式分别构造入测试、出测试和主动测试，从而证明协议能够满足的认证和必威体育官网网址属性。 其基本思想为：假设密码协议中的一个主体生成并发送了一条包含新数据的消息，而后在一个不同的加密形式中接收到，则可以断定某个拥有相关密钥的主体接收并转换了包含的消息；而且，在某种情况下，该主体一定是诚实主体，而非入侵者。 认证测试方法以其简单、严谨的证明方式为安全协议的形式化分析提供了更为科学准确的证明方法，因此被广泛应用于认证协议的安全性分析、自动化协议验证工具的开发，以及安全协议的设计等领域。 4.3.5 认证测试方法 4.3.5 认证测试方法 4.3.5 认证测试方法 认证测试规则是应用于协议分析中的方法，测试规则的使用能够简化协议分析的过程 4.3.5 认证测试方法 4.3.5 认证测试方法 3