串空间理论及其对公平交换协议的分析
文献类型:学位论文
作者 | 卢凤清 |
学位类别 | 博士 |
答辩日期 | 2007-06-05 |
授予单位 | 中国科学院软件研究所 |
授予地点 | 软件研究所 |
关键词 | 串空间理论 认证测试 公平交换协议 可追究性 公平性 |
其他题名 | The Research of Strand Spaces Theory and Analysis of Fair Exchange Protocols |
中文摘要 | 串空间理论是近年来提出的一种新的形式化分析方法。但是已有的串空间理论只适用于一些简单协议当中对于秘密性和认证性的分析,对于一些复杂情况下的协议安全性的描述与分析(例如协议交叉运行情况下的安全性或者群组协议当中动态情形下的安全性)仍然没有有效的方法。2000年Guttman和Fabrega提出了Authentication Tests的思想,该思想使得我们无需考虑协议的动态执行情况。我们对Guttman等人提出的三种测试中的输入测试(incoming test)进行扩展,使其能够用来分析使用签名和验证的协议,如CCITT X.509协议等。使用扩展后的输入测试来分析CCITT X.509协议的正确性,发现了它的不足之处。在使用串空间理论对Otway-Rees协议进行分析时发现协议的双方不能保证收到的会话密钥的一致性。针对这一点,我们提出了一种改进方法。改进后的方法不仅保证了会话密钥的一致性,而且使双方的认证性得到了改善。由于互联网应用的越来越普遍,对公平交换协议的研究变得越来越重要。公平交换协议是电子商务和电子交易成功的关键的理论基础。公平交换协议的目标是保护客户、商家彼此互不欺骗,保护互不信任的合作伙伴互不侵犯并公平完成商业交易。我们介绍了现有的公平交换协议并最后分析了它与传统安全协议的差别,考察了目前对公平交换协议的形式化分析的研究情况及串空间理论在公平交换协议研究方面的成果。我们对串空间理论进行扩展使其可以分析公平交换协议的安全性质,例如可追究性和公平性。我们引入了知识集等概念,与原理论中的认证测试中的主动测试相结合,对Deng等提出的在线挂号电子邮件协议进行了形式化分析,得出了与以往文献相同的结论。 |
语种 | 中文 |
公开日期 | 2011-03-17 |
页码 | 81 |
源URL | [http://ir.iscas.ac.cn/handle/311060/6584] ![]() |
专题 | 软件研究所_中科院软件所_中科院软件所 |
推荐引用方式 GB/T 7714 | 卢凤清. 串空间理论及其对公平交换协议的分析[D]. 软件研究所. 中国科学院软件研究所. 2007. |
入库方式: OAI收割
来源:软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。