中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
认证协议的形式化分析方法研究
作者: 丁一强
答辩日期: 1999
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 网络安全协议 ; 认证协议 ; 形式化方法 ; 模型检查
摘要: 网络安全协议目的在于运用加密技术保证开放网络的安全性。在安全协议中,加密技术是非常重要的因素,但另一方面,如果协议逻辑设计不当,则无异于在坚固的堡垒中留了个后门,攻击者根本不用费事去解密就可以达到其目的。为了保证安全协议设计的正确性,避免发生潜在的错误,就需要形式化的工具来精确地描述协议的行为以及协议所要达到的目标,并帮助分析此协议能否达到其预定目标。本论文中,作者使用模型检查(model checking)方法来形式化地分析安全协议中认证协议的性质,目的是帮助协议设计和分析人员发现认证协议中隐藏的漏洞。本论文中,作者的主要工作包括:1.给出了一个简洁的认证协议的模型,与其它模型检查方法不同之处是,在此模型中,攻击者的行为是隐式地被刻划的,这样便于协议的描述。2.定义了认证协议描述语言PEP(Principals + Environment = Protocol)。用于描述认证协议及其性质。3.给出了模型检查认证协议性质的算法,并用SML语言在Sun Solaris 2.5上实现。此算法可以自动检查认证协议的安全性质,并且当协议不满足安全性质时,可以自动找出攻击协议的途径。4.状态搜索过程中的状态爆炸是模型检查方法的关键难点之一,我们为此提出了PEP语言的惰性(lazy)语言,其中使用的符号化方法大大地提高了状态搜索的效率,并把一类协议的状态迁移树的无究分叉问题等价地化归为有穷分叉。5.认证协议的实例分析,发现了一些协议的安全漏洞。
英文摘要: Network security protocols are crucial for secure communications over open network environment like Internet. It is the cryptography techniques that make the network security possible. However, cryptography is not the whole story. The network security protocol design is also an important but error-prone task. One minor logic mistake may cause the entire protocol to fail, even without breaking the cryptosystem. In order to make the protocol design task manageable, formal techniques are required to precisely describe the protocols and their security properties, and to check whether protocols satisfy their properties. In this dissertation, the author uses model checking techniques to analyze the properties of security protocols, especially authentication protocols. This work is supposed to help protocol designers and analyzers to find subtle mistakes in security protocols. This dissertation includes the following work: 1. A succinct model of authentication protocol is proposed. Different from other model based approaches, actions of attacker can be implicitly specified in our model. So it is easier to specify protocols with our model. 2. A formal language PEP(Principals + Environment = Protocol) for the specification of authentication protocols and their security properties is defined. 3. An algorithm for model checking properties of authentication protocols is given. It is also implemented using SML language in Sun Solaris 2.5 environment. With this algorithm, one can automatically check security properties of authentication protocols. And attack traces would also be automatically reported if protocols fail to satisfy their properties. 4. The state-explosion problem is a critical problem in model checking approaches. A lazy semantics of PEP language is developed to improve the efficiency of model checking processes, and also eliminate infinite branches of state transition trees of one family of authentication protocols without missing any attack. 5. Some authentication protocols are analyzed and broken for example.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7224
Appears in Collections:中科院软件所

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

Recommended Citation:
丁一强. 认证协议的形式化分析方法研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 1999-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