认证协议的形式化分析方法研究
文献类型：学位论文
| 作者 | 丁一强 |
| 学位类别 | 博士 |
| 答辩日期 | 1999 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 中国科学院软件研究所 |
| 关键词 | 网络安全协议 认证协议 形式化方法 模型检查 |
| 学位专业 | 计算机软件与理论 |
| 中文摘要 | 网络安全协议目的在于运用加密技术保证开放网络的安全性。在安全协议中，加密技术是非常重要的因素，但另一方面，如果协议逻辑设计不当，则无异于在坚固的堡垒中留了个后门，攻击者根本不用费事去解密就可以达到其目的。为了保证安全协议设计的正确性，避免发生潜在的错误，就需要形式化的工具来精确地描述协议的行为以及协议所要达到的目标，并帮助分析此协议能否达到其预定目标。本论文中，作者使用模型检查（model checking）方法来形式化地分析安全协议中认证协议的性质，目的是帮助协议设计和分析人员发现认证协议中隐藏的漏洞。本论文中，作者的主要工作包括：1．给出了一个简洁的认证协议的模型，与其它模型检查方法不同之处是，在此模型中，攻击者的行为是隐式地被刻划的，这样便于协议的描述。2．定义了认证协议描述语言PEP（Principals + Environment = Protocol）。用于描述认证协议及其性质。3．给出了模型检查认证协议性质的算法，并用SML语言在Sun Solaris 2.5上实现。此算法可以自动检查认证协议的安全性质，并且当协议不满足安全性质时，可以自动找出攻击协议的途径。4．状态搜索过程中的状态爆炸是模型检查方法的关键难点之一，我们为此提出了PEP语言的惰性（lazy）语言，其中使用的符号化方法大大地提高了状态搜索的效率，并把一类协议的状态迁移树的无究分叉问题等价地化归为有穷分叉。5．认证协议的实例分析，发现了一些协议的安全漏洞。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 102 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/7224]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 丁一强. 认证协议的形式化分析方法研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 1999. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。