中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
网络安全协议形式化分析及支撑工具研究
作者: 肖美华
答辩日期: 2008-01-18
授予单位: 中国科学院软件研究所
授予地点: 软件研究所
学位: 博士
关键词: 安全协议 ; 形式化分析 ; 模型检测 ; 算法知识逻辑 ; 偏序归约
其他题名: Research on Formal Analysis of Cryptographic Protocols and Supporting Tool
摘要: 保护通信系统信息安全的核心技术包括密码系统和密码协议(也称安全协议)。系统的安全性不仅依赖于所采用的密码算法强度,而且与算法所使用的环境(安全协议)密切相关。密码系统相对比较成熟,攻击的代价是相当大的。相对密码系统而言,密码协议是比较脆弱的,很容易受到攻击。安全协议是通讯和网络安全体系、分布式系统和电子商务的关键组成部分,是安全系统的主要保障手段和工具。由于安全协议运行在复杂的分布式网络环境中,设计出的安全协议难免会存在安全漏洞,许多安全协议在使用多年后都被发现存在很严重的安全漏洞,例如著名的 Needham-Schroeder公开密钥协议在公开17年后,它存在的入侵者攻击漏洞才被Lowe发现。如果使用存在漏洞的安全协议,势必会形成严重的安全威胁。因此,网络安全协议的研究具有很强的理论价值和现实应用背景。 形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段。多年来人们采用的安全协议分析与验证方法主要是形式化方法,形式化方法主要有模型检测和定理证明。模型检测是一种重要的形式化自动验证技术,以其简洁明了和自动化程度高而倍受注目,模型检测使用状态空间搜索的办法自动地验证系统是否满足其设计规约,此技术的成功应用归功于有效验证工具的开发和支持。SPIN是一种著名的分析验证并发系统逻辑一致性的模型检测工具,2002年被ACM授予最具声望的“系统软件奖”(System Software Award)。 本文使用模型检测方法,基于算法知识逻辑形式化分析安全协议,在分析和比较常用安全协议形式化分析方法及对应支撑工具优劣的基础上,设计网络安全协议验证模型生成系统,目的是发现安全协议中隐藏的漏洞并对协议加以改进。研究成果表现为: 1. 形式化描述了安全协议的组成要素,包括消息、动作(迹)、消息状态及修改、协议运行及消息构造规则等,设计了协议描述语言PDL(Protocol Description Language),PDL中初步体现了协议安全构建块(Security Building Blocks)抽象建模机制。 2. 提出了基于算法知识逻辑的网络安全协议模型检测分析方法,用于显式地刻画入侵者模型能力,从理论上分析了其知识完备性。 3. 开发了网络安全协议验证模型生成系统,能将安全协议的PDL描述自动转换为对应协议的Promela语言描述,调用SPIN模型检测器,自动找出攻击漏洞,当协议不满足安全性质时,可以用消息序列图MSC直观地列出攻击序列。 4. 在网络安全协议验证模型生成系统中采用了多项优化策略(包括偏序归约、语法重定序以及静态分析等)解决安全协议模型检测过程中状态爆炸问题(State Explosion),实验结果证实了系统采用这些优化策略的有效性及效率。 5. 认证协议的实例分析(Needham-Schroeder协议、TMN协议、BAN-Yahalom 协议、Helsinki 协议、密钥交换协议IKEv2等),发现了这些协议已公布的安全漏洞。 关键词:安全协议;形式化分析;模型检测;算法知识逻辑;偏序归约
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/5832
Appears in Collections:中科院软件所

Files in This Item:

There are no files associated with this item.


Recommended Citation:
肖美华. 网络安全协议形式化分析及支撑工具研究[D]. 软件研究所. 中国科学院软件研究所. 2008-01-18.
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