学位论文 > 优秀研究生学位论文题录展示

基于计算机辅助证明的安全性保证方法研究

作　者: 石铠源
导　师: 庞建民
学　校: 解放军信息工程大学
专　业: 计算机软件与理论
关键词: 安全性保证机器辅助证明 Coq 归纳构造演算形式化方法协议验证程序验证
分类号: TP309
类　型: 硕士论文
年　份: 2007年
下　载: 60次
引　用: 0次
阅　读: 论文下载

内容摘要

随着计算机和网络的广泛应用,很多貌似安全和正确的协议或软件呈现出严重的安全问题,这些问题来自设计和实现等多个方面。因此,迫切需要合适的、系统化的方法来保证协议和软件的安全。本文深入研究了协议和软件的安全性保证方法,提出了基于计算机辅助证明的研究方案,并对其可行性和有效性进行了理论和实验验证。本文所做的工作如下;对形式化方法和计算机辅助证明工具进行了较为全面的分析比较,指出了各自的优点和局限性;选取了基于高阶逻辑的交互式辅助证明工具Coq作为本文研究工作的平台,在对Coq的元语言——归纳构造演算深入研究的基础上,剖析了Coq的强大功能,为基于Coq开展安全性保证工作提供了理论依据和技术保证;深入分析了各种协议验证方法,分别针对停止等待协议和Otway-Rees认证协议建立了形式化模型,对相关概念和性质给出了形式化描述,并进行了严格的计算机辅助验证。验证结果表明停止等待协议在设计上是正确无误的以及Otway-Rees认证协议存在类型缺陷;针对程序正确性问题,本文通过对Hoare逻辑、程序提取等技术的研究,利用Coq进行了大量的函数式和命令式程序的验证,探索出了一条系统地进行程序安全性保证工作的方法。文中的形式化和证明都经过严格的计算机验证,验证过程和结果表明,基于计算机辅助证明可以系统、有效地开展协议和软件安全性保证工作。

全文目录

表目录  7-8
图目录  8-9
摘要  9-10
ABSTRACT  10-11
第一章绪论  11-14
  1.1 研究背景  11
  1.2 研究现状  11-12
  1.3 本文的贡献  12-13
  1.4 本文的组织结构  13-14
第二章形式化方法和辅助证明工具的研究  14-21
  2.1 形式化方法  14-17
    2.1.1 形式化描述  14-15
    2.1.2 形式化验证  15-16
    2.1.3 形式化方法的优点  16-17
    2.1.4 形式化方法的局限性  17
  2.2 辅助证明工具  17-20
    2.2.1 辅助证明工具研究  17-18
    2.2.2 6种辅助证明工具的比较  18-20
  2.3 结论  20-21
第三章 Coq的元语言与功能分析  21-34
  3.1 理论背景  21-26
    3.1.1 直觉主义逻辑  21-23
    3.1.2 简单类型λ-演算  23-24
    3.1.3 Curry-Howard同构  24-26
  3.2 归纳构造演算  26-29
    3.2.1 CIC的项  26-27
    3.2.2 CIC的类型规则(typing rules)  27
    3.2.3 CIC的归约规则(reduction rules)  27-29
  3.3 Coq功能研究  29-33
    3.3.1 Coq作为逻辑系统  29-31
    3.3.2 Ceq作为编程语言  31-33
  3.4 结论  33-34
第四章协议安全性保证的研究与实现  34-52
  4.1 网络协议安全性保证问题的提出  34
  4.2 网络协议安全性保证的相关工作  34-35
  4.3 实例分析:停止等待协议的验证  35-42
    4.3.1 协议概述  35-36
    4.3.2 协议模型  36-37
    4.3.3 协议形式化  37-41
    4.3.4 正确性证明  41-42
    4.3.5 平台和工具  42
    4.3.6 小结  42
  4.4 安全协议安全性保证问题的提出  42-43
  4.5 安全协议安全性保证相关工作  43-45
  4.6 实例分析: Otway-Rees协议  45-50
    4.6.1 协议概述  45-46
    4.6.2 类型缺陷攻击  46
    4.6.3 协议模型  46-47
    4.6.4 协议形式化  47-49
    4.6.5 协议证明  49-50
    4.6.6 平台和工具  50
    4.6.7 小结  50
  4.7 结论  50-52
第五章程序安全性保证的研究与实现  52-61
  5.1 程序安全性保证问题的提出  52
  5.2 程序安全性保证相关工作  52-53
  5.3 基于CIC的函数式语言的验证  53-57
    5.3.1 直接定义ML函数  53-54
    5.3.2 程序提取  54-57
  5.4 基于CIC的命令式语言的验证  57-60
    5.4.1 Hoare逻辑  57-58
    5.4.2 工具Why  58-60
  5.5 结论  60-61
结束语  61-62
参考文献  62-65
作者简历攻读硕士期间取得的学术成果  65-66
  一、个人简历  65
  二、攻读硕士期间取得的学术成果  65-66
致谢  66

相似论文

有限元法在略阳电厂边坡稳定性分析中的应用与研究,TU43
Web服务事务协调协议WS-TX的形式化分析与验证,TP393.09
卡箱式高速公路联网收费通行IC卡管理系统的设计与实现,TP311.52
基于Z规格的软件缺陷形式化方法,TP311.53
基于Hoare逻辑的软件形式化验证技术研究,TP311.52
基于形式化方法的统一软件模型及其应用,TP311.52
面向软件复用的组件形式化开发,TP311.52
基于串空间模型的形式化方法的扩展与应用,TP393.08
UML建模的形式化方法研究和应用,TP311.52
电子商务安全协议的一种形式化分析方法,TP393.08
出具证明编译器中证明生成的研究,TP314
一种出具证明编译器中汇编级断言和证明的生成方法,TP314
基于着色Petri网的LDP协议验证研究,TN915.04
形式化方法的理论及其影响,B812
基于行为时序逻辑模型检测的研究与应用,TP311.52
基于SPIN/Promela的UML模型验证工具设计与实现,TP311.52
Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用,TP311.11
验证带有线程动态创建和退出多线程程序,TP311.53
THP事务协调协议的形式化分析与验证,TP311.52
基于PVS的自稳定算法形式化分析,TP338.8
关于密码协议的形式化分析方法的研究,TP393.08