中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
基于串空间模型分析与验证密码安全协议
作者: 石昊苏
答辩日期: 2004
专业: 基础数学
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 安全协议 ; 形式化方法 ; 串空间模型 ; 理想 ; 秘密性
摘要: 随着网络的普及以及电子商务和电子政务蓬勃兴起,安全协议变得越来越重要,确保安全协议的安全性己经成为一项重要的研究课题。安全协议分析是一个很难解决的问题,20年来为了应对这一挑战,科学家们投入了大量的精力。在已有的理论和方法中,形式化分析方法的成果比较突出,其发展前景被专家们普遍看好,本文第二章对此进行了综述。串空间(STRAND SPACE)模型由F'abrega、Herzog和Guttman三人提出,它是分析安全协议的一种实用、直观和严格的形式化方法,它充分吸收了前人的研究成果,模型使用一种节点间存在因果关系的有向图来表示协议的运行。D.Song对串空间模型进行了扩展,并开发了安全协议自动验证工具ATHENA。在深入研究串空间理论的基础上,本文从理论和算法两个方面对串空间模型进行了扩展和完善。在理论上,本文引入了理想的语义,并首次使用了理想的概念对安全协议的秘密性进行严格的定义,同时使用理想的命题逻辑公式表示安全协议的秘密性;另外,本文修正了F'abrega、Herzog和Guttnan三人文献中的一个引理的证明,原有的证明是不完善的。在算法上,本文增设了一条状态删减规则,并进行了严格的证明;另外,对模型检测算法进行了修改,使得算法可以找出协议在限定搜索深度下所有攻击反例。我们使用JAVA语言对本文的模型检测算法进行了具体实现,开发了一个拥有自主知识产权的安全协议自动验证工具AVSP。对已经进行的实验结果分析表明,本文对一串空间模型的扩展是正确的和有效的;另外,利用AVSP我们发现了Woo-Lam~4认证协议的一个新的在现有的文献中没有公布的攻击。
英文摘要: With the popularization of network and flourishing of Internet applications, security protocols are becoming more and more important, furthermore, ensuring the security of cryptographic protocols has become an important research task. Scientists have been making great efforts to take the challenge for past 20 years, which in a sense shows the difficulty of security protocols analysis. Among all existing theories and methods, formal method is an outstanding one with promising developing prospect recognized by experts at large. This paper makes a summary of these methods in the second chapter. Having fully absorbed the former researching results, F'abrega^ Herzog and Guttman brought forward a kind of formal method named STRAND SPACE, which is a practical, intuitive and strict one for security protocols analysis. The model uses a kind of order graph between its nodes existing casual relationship to represent protocol executions. D.Song has made an extension to SSM and has developed an automatic verification tool, ATHENA. This paper does a further study on the SSM and makes an extension to the model in theorem and algorithm. About theorem, the paper introduces the syntax of ideal, also the first time uses concept of honest ideal to define secrecy goal of protocol and utilizes honest ideal logic to specify secrecy property. At the same time, this paper corrects one not so perfect lemma proving in a literature written by F' abrega Herzog and Guttman. About algorithm, the paper addes a new state pruning rule and makes strict proving. Additionally, the paper revises the model-checking algorithm so that it can find all available count-examples under the searching depth limitiation. We implemented the model-checking algorithm with Java and developed a new automatic verification tool named AVSP. We have done some experiments and the results showed that the paper's extension to the model is correct and effective. With AVSP, we found a new attack on the Woo-Lam4 authentic protocol, which hadn't been released by existing papers.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6780
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
LW014075.pdf(3492KB)----限制开放-- 联系获取全文

Recommended Citation:
石昊苏. 基于串空间模型分析与验证密码安全协议[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2004-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[石昊苏]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[石昊苏]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace