基于串空间模型分析与验证密码安全协议
文献类型：学位论文
| 作者 | 石昊苏 |
| 学位类别 | 博士 |
| 答辩日期 | 2004 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 中国科学院软件研究所 |
| 关键词 | 安全协议 形式化方法 串空间模型 理想 秘密性 |
| 学位专业 | 基础数学 |
| 中文摘要 | 随着网络的普及以及电子商务和电子政务蓬勃兴起，安全协议变得越来越重要，确保安全协议的安全性己经成为一项重要的研究课题。安全协议分析是一个很难解决的问题，20年来为了应对这一挑战，科学家们投入了大量的精力。在已有的理论和方法中，形式化分析方法的成果比较突出，其发展前景被专家们普遍看好，本文第二章对此进行了综述。串空间（STRAND SPACE）模型由F'abrega、Herzog和Guttman三人提出，它是分析安全协议的一种实用、直观和严格的形式化方法，它充分吸收了前人的研究成果，模型使用一种节点间存在因果关系的有向图来表示协议的运行。D.Song对串空间模型进行了扩展，并开发了安全协议自动验证工具ATHENA。在深入研究串空间理论的基础上，本文从理论和算法两个方面对串空间模型进行了扩展和完善。在理论上，本文引入了理想的语义，并首次使用了理想的概念对安全协议的秘密性进行严格的定义，同时使用理想的命题逻辑公式表示安全协议的秘密性；另外，本文修正了F'abrega、Herzog和Guttnan三人文献中的一个引理的证明，原有的证明是不完善的。在算法上，本文增设了一条状态删减规则，并进行了严格的证明；另外，对模型检测算法进行了修改，使得算法可以找出协议在限定搜索深度下所有攻击反例。我们使用JAVA语言对本文的模型检测算法进行了具体实现，开发了一个拥有自主知识产权的安全协议自动验证工具AVSP。对已经进行的实验结果分析表明，本文对一串空间模型的扩展是正确的和有效的；另外，利用AVSP我们发现了Woo-Lam~4认证协议的一个新的在现有的文献中没有公布的攻击。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 64 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/6780]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 石昊苏. 基于串空间模型分析与验证密码安全协议[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2004. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。