改进的加密协议形式化验证模型和算法

• 作者: 张磊 桑田 黄连生
• 来源期刊: 清华大学学报(自然科学版)
• 学科: 工学
• 关键词: 状态搜索 形式化验证 加密协议 攻击者 Murφ
• 年，卷（期）: 2002,（1）
• 所属期刊栏目: 计算机科学与技术
• 页码范围: 48-51
• 页数: 4页
• 分类号: TP393.08
• 字数: 4229字
• 语种: 中文
• DOI: 10.3321/j.issn:1000-0054.2002.01.016

摘要

状态搜索技术是分析加密协议安全属性的最流行的形式化验证方法之一, Murφ是一种常用的能分析一般性协议的模型工具,它的原理简明,但缺点是容易产生状态爆炸.为了克服这一问题,针对加密协议的特点,提出了改进模型和算法.根据协议的描述定义状态空间,建立以攻击者为核心的验证模型,使用搜索算法检测是否存在攻击者能完成攻击的不安全状态.在对通信过程、消息传递方式等方面改进后,搜索空间的可达状态数减少了很多,验证系统的效率显著提高.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张磊	清华大学计算机科学与技术系	122	1621	23.0	36.0
2	黄连生	清华大学计算机科学与技术系	15	144	6.0	12.0
3	桑田	清华大学计算机科学与技术系	3	50	2.0	3.0