基于串空间的KryptoKnight协议分析及与逻辑化方法.PDF

基于串空间的KryptoKnight协议分析及与逻辑化方法的比较 荣昆 李益发 (信息工程大学 河南 郑州 450002) 摘要: 网络安全在信息时代非常重要，而网络安全的关键问题之一是安全协议. 本文通 过串空间模型对KryptoKnight协议进行了分析, 得出该协议是安全的. 并对串空间模型和 BAN逻辑方法进行了比较. 关键词: KryptoKnight 串空间 安全协议 中图分类号：TP309 文献标识码：A 1 引言 随着科学技术, 特别是因特网的迅猛发展, 数字化﹑电子化的趋势已经波及社会生活的 几乎所有方面.安全协议是使用密码技术的网络通信协议. 随着网络时代的发展, 特别是各 种安全协议的不断出现, 如何准确的分析协议变得尤为重要. 目前, 采用形式化方法来分析 安全协议, 这些方法分为3类[2] ：推导构造法, 利用逻辑推理来分析协议主体的知识和信任的 演化情况, 比如BAN 逻辑[3];攻击构造法,利用协议的代数属性建立可能的攻击集合, 比如文献 [4] [5] ;证明构造法,证明协议满足其安全性要求, 比如文献 . 在文献[5] 中, Thayer, Herzog和Guttman提出了分析协议的串空间(Strand Space)模型, 并 且证明了Needham-Schroeder-Lowe协议的正确性, 随后在文献[6] 中, 作者又对串空间进行了 拓展, 给出了理想(Ideal)的概念, 并对Otway-Rees协议进行了分析. KryptoKnight协议是用 Hash 函数进行身份认证的一个安全协议, 在文章的第3节将给出对其的分析. 本文第2节本文简介Strand空间模型和认证协议的正确性概念, 确定协议证明的目标. 第3节给出用Strand空间模型证明KryptoKnight协议的过程. 第4节对串空间方法与逻辑化方 法进行了比较. 第5节总结全文. 2 串空间(Strand Space)模型[5] 2.1 项(term)和子项(subterm) 定义2.1 设A 表示协议的所有参与者之间传送的消息的全体组成的集合, 称A 为消息空间, A 中的元素称为消息项. 项可由原子项经过级连和加密得到, 原子项可分为文本项T和密钥项K. A 可由下面三种 运算生成: 加密运算encr: K×A →A 级联运算join : A ×A →A 密钥的逆运算inv: K→K 对信息的压缩hash: A → A 密钥逆运算将公私钥对中的一个映成另一个, 把对称密钥映成自己. 为了方便, 把encr(K,m) 记为{m} , inv(K)记为K-1,join (a,b)记为ab, hash(a)记为H(a). 把encr 的像空间encr(K× A)记作 K E, 称为密文空间，hash 的像空间hash(A)记为H ，而把K∪T∪E∪H 中的消息项称为A 上的简 单项. 在消息空间中, 可以定义A 中元素的包含关系⊏如下: 定义2.2 设A 是一信息空间, 递归的定义A 中元素的包含关系⊏如下: (1) 若a ∈T, 则a⊏a; (2) 若a⊏g或a⊏h, 则a⊏gh ; (3) 若h⊏g, 则b⊏{g } ; K (4) a⊏gh iff a ⊏g or a⊏h or a =gh (5) 若h⊏H(g), 则h⊏g . 其中 h,g ∈A , k ∈K. 显然, ⊏是一种传递﹑反身的关系. 2.2 串, 串空间和丛(Bundle) 串是协议角色的一个实例. 串空间定义如下: 定义2.3 符号项是一个有序对〈 σ ,t〉, t ∈A , σ 为+或−, 记作+t或−