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

加密协议的一种分析方法

作　者: 吕晓冬
导　师: 刘根成
学　校: 郑州大学
专　业: 计算机软件与理论
关键词: 加密协议 CPAL 形式话义最弱前置条件
分类号: TN918.9
类　型: 硕士论文
年　份: 2001年
下　载: 60次
引　用: 0次
阅　读: 论文下载

内容摘要

在本论文中我们提出了一种通用的，可扩展的分析和检查加密协议的方法。我们的方法就是用CPAL（Cryptographic Protocol Analysis Language）语言来表示协议，将Hoare和Dijkstra在形式语义方面的理论应用到该语言，分析该语言的形式语义，定义每种语句的最弱前置条件。我们定义协议的失败条件作为后置条件，对加密系统的有关公理进行扩展，并用来对最弱前置条件进行推理证明，如果证明成功说明该协议会受到某个攻击。

全文目录

中文摘要  4-5
英文摘要  5-6
第一章引言  6-17
  1．1 计算机安全  6-8
  1．2 网络安全  8
  1．3 加密  8-12
    1．3．1 一个古典加密系统  8-9
    1．3．2 密码和编码  9-10
    1．3．3 现代加密系统  10-12
  1．4 加密协议  12-15
    1．4．1 什么是加密协议？  13-14
    1．4．2 加密协议的问题  14-15
    1．4．3 协议检查的重要性  15
  1．5 我的协议分析方法  15-16
    1．5．1 方法概述  15-16
  1．6 论文结构概要  16-17
第二章相关工作  17-28
  2．1 非形式化技术  17-22
    2．1．1 Denning和Sacco  17-18
    2．1．2 Simmons  18-20
    2．1．3 Abadi和Needham  20-22
  2．2 逻辑分析  22-27
    2．2．1 Burrows，Abadi，Needham  22-27
  2．3 小结  27-28
第三章 CPAL加密协议分析语言  28-36
  3．1 标准伪代码表示法  28
  3．2 CPAL语言  28-34
    3．2．1 CPAL环境  29
    3．2．2 语法  29-31
    3．2．3 语义  31-34
  3．3 小结  34-36
第四章自动程序合成  36-42
  4．1 背景  36
  4．2 程序性方法  36-37
  4．3 演绎方法  37-38
    4．3．1 概述  37
    4．3．2 演绎方法的例子  37-38
  4．4 转换方法  38-42
    4．4．1 概述  38
    4．4．2 转换方法的例子  38-41
    4．4．3 总结  41-42
第五章加密协议分析  42-56
  5．1 概述  42
  5．2 Step 1—用CPAL表示协议  42-43
  5．3 Step 2—定义失败条件  43
  5．4 Step 3—搜寻攻击  43-55
    5．4．1 计算最弱前置条件  45-46
    5．4．2 搜索推理证明  46-51
    5．4．3 最弱前置条件命题的证明  51-54
    5．4．4 使用证明结果修改协议  54-55
  5．5 总结和讨论  55-56
第六章总结与展望  56-60
  6．1 总结与回顾  56
  6．2 未来工作  56-59
    6．2．1 增加代数公理集合  56-57
    6．2．2 增加协议公理集合  57-59
    6．2．3 证明的形式化实现  59
  6．3 总结  59-60
附录对协议的分析  60-67
  附录1 对一个简单加密协议的分析  60-64
  附录2 对TMN协议的分析  64-67
总结  67
致谢  67-68
参考文献：  68-69

加密协议的一种分析方法

内容摘要

全文目录

相似论文