计算机科学与技术专业毕业论文计算机科学与技术专业毕业论文 精品论文精品论文 复杂安全协议的建复杂安全协议的建模与验证模与验证关键词：互联网关键词：互联网 安全协议安全协议 不停机性预测不停机性预测 网络安全网络安全 自动构造算法自动构造算法 验证方法验证方法摘要：随着网络的发展，互联网络的安全问题变得越来越棘手，越来越重要， 安全协议的安全性质也受到越来越多的挑战。安全协议是解决互联网络安全问 题最有效的手段之一，使用安全协议在开放的互联网络上可以实现身份认证等 多项安全功能。由于在计算机网络中，相互通信的双方不能通过生物特征识别 对方，因而彼此的认证需要建立在密码体制的基础上。安全协议是建立在密码 体制基础上的一种通信协议，它运行在计算机网络或分布式系统中，借助于密 码算法为在网络环境中实现密钥分配、身份认证、电子商务交易等任务的各方 约定任务的执行步骤和执行规则。安全协议的正确性对网络应用的安全至关重 要。然而，设计并投入实际应用的安全协议在运行时不一定能够真正实现它所 声明的安全性质。许多协议在应用了很长一段时间后被发现存在安全漏洞。 设计和开发高效的安全协议建模与验证的方法和工具是安全协议形式化研究领 域的一个研究热点，也是验证复杂安全协议的关键环节。本文以 BrunoBlanchet 提出的 Horn 逻辑模型为基础，对反例构造算法和复杂协议验证 方法进行了系统、深入的研究，主要工作包括以下几个方面： 1.基于 Horn 逻辑的安全协议反例的自动构造算法。 BrunoBlanchet 提出了基于 Horn 逻 辑的安全协议模型，该模型可高效地验证安全协议。为了将消息的角色信息保 留在模型中，本文设计了相关的数据结构，给出了反例自动构造的算法实现， 使验证工具能从不满足安全性质的消解序列中自动地构造出标准形式的反例， 从而方便人们使用基于 Horn 逻辑的验证工具验证协议。 2.不动点计算的不 停机性预测。 安全协议验证的不停机性源于不动点计算的不停机性。通过研 究安全协议逻辑程序解形式不动点计算不终止的特征，本文给出了不动点计算 不终止的预测方法。基于此方法，可以在协议验证时自适应地选择(精确或抽象)验 证方法验证(停机或不停机的)安全协议。 3.抽象与精化迭代验证框架。 安全协议的正确性验证问题是不可判定的，使用抽象解释理论能够有效地验证 安全协议。通过研究 Horn 逻辑模型中协议验证的特点，给出了安全协议基于抽 象-精化的迭代验证理论框架。抽象验证保证停机，而精化过程可有效地去除虚 假反例。因此，抽象-精化迭代框架可对 Horn 逻辑模型中验证过程不停机的安 全协议进行有效验证。为了提高抽象模型的精度，本文进一步提出了局部抽象- 精化迭代验证的理论框架。局部抽象可以提高整个验证过程的验证效率，为复 杂协议的验证提供了有效的途径。 4.时间敏感安全协议的建模与验证。 通过将描述时间的事件加入到进程代数模型中，使得时间戳能方便有效地在协 议模型中描述出来。将时间元素的线性约束加入到基于 Horn 逻辑的安全协议模 型中，使得 Horn 逻辑模型能有效地处理时间约束信息。通过研究规则中各时间 元素与消解的关系，找到了确定时间相关元素的时间先后关系的办法，提出了 两阶段验证方法。 一条规则是否可用，此时还需考察其所对应的约束系统是 否可满足。因此，本文对该模型下的约束系统进行了研究，提出了一个高效判 断其可满足性的判定算法，并证明了该算法是多项式时间算法。由于约束系统 中存在大量冗余的不等式，本文还深入研究了该系统，针对其本身的特性，提出了约束的抽象理论简化约束系统，该方法能有效地降低时空开销。 5.设计 并实现了一个高效的安全协议验证工具 SPVT-II。 本文提出了不停机性预测 和抽象一精化迭代验证框架的实现算法，在安全协议自动分析工具 SPVT 的基础 上，结合抽象一精化迭代验证框架，设计并实现了一个自适应选择验证方法的 高效的协议验证工具 SPVT-II。该工具既能发现协议中可能的反例，也能尽可 能地减少虚假反例的产生。 6.Kerberos 协议协议的分析与验证。 本文通 过对 Kerberos 协议进行分析，将公钥 Kerberos 协议的认证服务交换阶段进行 了建模，并用 SPVT-II 对协议模型进行了自动化的验证。实验结果表明 SPVT- II 能自动发现 PKINIT-26 中认证服务阶段的攻击。正文内容正文内容随着网络的发展，互联网络的安全问题变得越来越棘手，越来越重要，安 全协议的安全性质也受到越来越多的挑战。安全协议是解决互联网络安全问题 最有效的手段之一，使用安全协议在开放的互联网络上可以实现身份认证等多 项安全功能。由于在计算机网络中，相互通信的双方不能通过生物特征识别对 方，因而彼此的认证需要建立在密码体制的基础上。安全协议是建立在密码体 制基础上的一种通信协议，它运行在计算机网络或分布式系统中，借助于密码 算法为在网络环境中实现密钥分配、身份认证、电子商务交易等任务的各方约 定任务的执行步骤和执行规则。安全协议的正确性对网络应用的安全至关重要。 然而，设计并投入实际应用的安全协议在运行时不一定能够真正实现它所声明 的安全性质。许多协议在应用了很长一段时间后被发现存在安全漏洞。 设计 和开发高效的安全协议建模与验证的方法和工具是安全协议形式化研究领域的 一个研究热点，也是验证复杂安全协议的关键环节。本文以 BrunoBlanchet 提 出的 Horn 逻辑模型为基础，对反例构造算法和复杂协议验证方法进行了系统、 深入的研究，主要工作包括以下几个方面： 1.基于 Horn 逻辑的安全协议反 例的自动构造算法。 BrunoBlanchet 提出了基于 Horn 逻辑的安全协议模型， 该模型可高效地验证安全协议。为了将消息的角色信息保留在模型中，本文设 计了相关的数据结构，给出了反例自动构造的算法实现，使验证工具能从不满 足安全性质的消解序列中自动地构造出标准形式的反例，从而方便人们使用基 于 Horn 逻辑的验证工具验证协议。 2.不动点计算的不停机性预测。 安全 协议验证的不停机性源于不动点计算的不停机性。通过研究安全协议逻辑程序 解形式不动点计算不终止的特征，本文给出了不动点计算不终止的预测方法。 基于此方法，可以在协议验证时自适应地选择(精确或抽象)验证方法验证(停机 或不停机的)安全协议。 3.抽象与精化迭代验证框架。 安全协议的正确性 验证问题是不可判定的，使用抽象解释理论能够有效地验证安全协议。通过研 究 Horn 逻辑模型中协议验证的特点，给出了安全协议基于抽象-精化的迭代验 证理论框架。抽象验证保证停机，而精化过程可有效地去除虚假反例。因此， 抽象-精化迭代框架可对 Horn 逻辑模型中验证过程不停机的安全协议进行有效 验证。为了提高抽象模型的精度，本文进一步提出了局部抽象-精化迭代验证的 理论框架。局部抽象可以提高整个验证过程的验证效率，为复杂协议的验证提 供了有效的途径。 4.时间敏感安全协议的建模与验证。 通过将描述时间 的事件加入到进程代数模型中，使得时间戳能方便有效地在协议模型中描述出 来。将时间元素的线性约束加入到基于 Horn 逻辑的安全协议模型中，使得 Horn 逻辑模型能有效地处理时间约束信息。通过研究规则中各时间元素与消解 的关系，找到了确定时间相关元素的时间先后关系的办法，提出了两阶段验证 方法。 一条规则是否可用，此时还需考察其所对应的约束系统是否可满足。 因此，本文对该模型下的约束系统进行了研究，提出了一个高效判断其可满足 性的判定算法，并证明了该算法是多项式时间算法。由于约束系统中存在大量 冗余的不等式，本文还深入研究了该系统，针对其本身的特性，提出了约束的 抽象理论简化约束系统，该方法能有效地降低时空开销。 5.设计并实现了一 个高效的安全协议验证工具 SPVT-II。 本文提出了不停机性预测和抽象一精 化迭代验证框架的实现算法，在安全协议自动分析工具 SPVT 的基础上，结合抽 象一精化迭代验证框架，设计并实现了一个自适应选择验证方法的高效的协议验证工具 SPVT-II。该工具既能发现协议中可能的反例，也能尽可能地减少虚 假反例的产生。 6.Kerberos 协议协议的分析与验证。 本文通过对 Kerberos 协议进行分析，将公钥 Kerberos 协议的认证服务交换阶段进行了建 模，并用 SPVT-II 对协议模型进行了自动化的验证。实验结果表明 SPVT-II 能 自动发现 PKINIT-26 中认证服务阶段的攻击。 随着网络的发展，互联网络的安全问题变得越来越棘手，越来越重要，安全协 议的安全性质也受到越来越多的挑战。安全协议是解决互联网络安全问题最有 效的手段之一，使用安全协议在开放的互联网络上可以实现身份认证等多项安 全功能。由于在计算机网络中，相互通信的双方不能通过生物特征识别对方， 因而彼此的认证需要建立在密码体制的基础上。安全协议是建立在密码体制基 础上的一种通信协议，它运行在计算机网络或分布式系统中，借助于密码算法 为在网络环境中实现密钥分配、身份认证、电子商务交易等任务的各方约定任 务的执行步骤和执行规则。安全协议的正确性对网络应用的安全至关重要。然 而，设计并投入实际应用的安全协议在运行时不一定能够真正实现它所声明的 安全性质。许多协议在应用了很长一段时间后被发现存在安全漏洞。 设计和 开发高效的安全协议建模与验证的方法和工具是安全协议形式化研究领域的一 个研究热点，也是验证复杂安全协议的关键环节。本文以 BrunoBlanchet 提出 的 Horn 逻辑模型为基础，对反例构造算法和复杂协议验证方法进行了系统、深 入的研究，主要工作包括以下几个方面： 1.基于 Horn 逻辑的安全协议反例 的自动构造算法。 BrunoBlanchet 提出了基于 Horn 逻辑的安全协议模型， 该模型可高效地验证安全协议。为了将消息的角色信息保留在模型中，本文设 计了相关的数据结构，给出了反例自动构造的算法实现，使验证工具能从不满 足安全性质的消解序列中自动地构造出标准形式的反例，从而方便人们使用基 于 Horn 逻辑的验证工具验证协议。 2.不动点计算的不停机性预测。 安全 协议验证的不停机性源于不动点计算的不停机性。通过研究安全协议逻辑程序 解形式不动点计算不终止的特征，本文给出了不动点计算不终止的预测方法。 基于此方法，可以在协议验证时自适应地选择(精确或抽象)验证方法验证(停机 或不停机的)安全协议。 3.抽象与精化迭代验证框架。 安全协议的正确性 验证问题是不可判定的，使用抽象解释理论能够有效地验证安全协议。通过研 究 Horn 逻辑模型中协议验证的特点，给出了安全协议基于抽象-精化的迭代验 证理论框架。抽象验证保证停机，而精化过程可有效地去除虚假反例。因此， 抽象-精化迭代框架可对 Horn 逻辑模型中验证过程不停机的安全协议进行有效 验证。为了提高抽象模型的精度，本文进一步提出了局部抽象-精化迭代验证的 理论框架。局部抽象可以提高整个验证过程的验证效率，为复杂协议的验证提 供了有效的途径。 4.时间敏感安全协议的建模与验证。 通过将描述时间 的事件加入到进程代数模型中，使得时间戳能方便有效地在协议模型中描述出 来。将时间元素的线性约束加入到基于 Horn 逻辑的安全协议模型中，使得 Horn 逻辑模型能有效地处理时间约束信息。通过研究规则中各时间元素与消解 的关系，找到了确定时间相关元素的时间先后关系的办法，提出了两阶段验证 方法。 一条规则是否可用，此时还需考察其所对应的约束系统是否可满足。 因此，本文对该模型下的约束系统进行了研究，提出了一个高效判断其可满足 性的判定算法，并证明了该算法是多项式时间算法。由于