安全协议分析的界——综合模型检查与Strand Spaces(英文)

doi:10.7523/j.issn.2095-6134.2002.3.011

中国科学院大学学报 ›› 2002, Vol. 19 ›› Issue (3): 288-294.DOI: 10.7523/j.issn.2095-6134.2002.3.011

安全协议分析的界——综合模型检查与Strand Spaces(英文)

刘怡文, 李伟琴

北京航空航天大学计算机科学与工程系, 北京 100083

收稿日期:2002-06-06 发布日期:2002-05-18
作者简介:LIU Yi-Wcn, female, born in November 1966, ph. D. candidate; E-mail: lywlyw(}163.com，lwq(]buaa.edu.cn

Some Bounds on Security Protocol Analysis——Combining Model Checking and Strand Spaces

LIU Yi-Wen, LI Wei-Qin

Department of Computer Science and Engineering, Beijing University of Aeronautics and Astronautics, Beijing 100083

Received:2002-06-06 Published:2002-05-18

摘要/Abstract

摘要：

Strand Spaces是一种用于分析安全协议的机器证明方法.简要介绍了 Strand Spaces的基本特点,分析了其优劣,提出了构造协议的理想子环的算法,并以此来约束协议入侵者的能力和协议并行运行的次数.将模型检查与 Strand Spaces结合在一起,提出了一种综合分析方法来验证协议的安全特性,该方法可充分发挥模型检查与 Strand Spaces二者的优势.

关键词: 安全协议分析, 模型检查, Strand Spaces, 定理证明

Abstract:

Strand Spaces serve as a model of security protocol analysis. In this paper, the main characteristics of Strand Spaces are briefly introduced, and its advantages and disadvantages are presented. An algorithm of building an ideal model of a protocol is proposed, which is used to bound both the abilities of the penetrator and the number of concurrent protocol runs. Combining Model Checking and Strand Spaces, a method is proposed to use both the automatic reasoning mechanism of the Model Checking and the bounds on security protocol analysis to achieve effective analysis of security protocols, avoiding state explosion problems.

Key words: security protocol analysis, model checking, Strand Spaces, theorem prover CLC TP309

中图分类号:

TP393.08

刘怡文, 李伟琴. 安全协议分析的界——综合模型检查与Strand Spaces(英文)[J]. 中国科学院大学学报, 2002, 19(3): 288-294.

LIU Yi-Wen, LI Wei-Qin. Some Bounds on Security Protocol Analysis——Combining Model Checking and Strand Spaces[J]. , 2002, 19(3): 288-294.

[1]	赖训飞, 梁旭文, 谢卓辰, 李宗旺. 基于实体嵌入和长短时记忆网络的入侵检测方法[J]. 中国科学院大学学报, 2020, 37(4): 553-561.
[2]	方喆君, 刘奇旭, 张玉清. Android应用软件功能泄露漏洞挖掘工具的设计与实现[J]. 中国科学院大学学报, 2015, 32(1): 127-135.
[3]	蔡权伟, 林璟锵, 荆继武, 尚铭. PKI应用系统互操作性检测工具的设计与实现[J]. 中国科学院大学学报, 2012, (6): 799-804.
[4]	刘涛, 聂晓峰, 荆继武, 王跃武. 基于小型对象分配技术的 GTNetS蠕虫仿真内存管理[J]. 中国科学院大学学报, 2012, 29(1): 131-135.
[5]	刘书明, 刘建伟, 毛剑. 一种改进的AODV安全路由协议[J]. 中国科学院大学学报, 2011, 28(6): 801-805.
[6]	杨晓晖, 赵鹏远, 石强, 田俊峰. 基于主观逻辑扩展的实体行为动态可信模型[J]. 中国科学院大学学报, 2011, 28(6): 818-825.
[7]	王鹏. 一个关于MAC伪随机性与不可伪造性的注记[J]. 中国科学院大学学报, 2010, 27(2): 263-266.
[8]	孔(王莹), 张玉清. 一种改进的网络可生存需求分析方法[J]. 中国科学院大学学报, 2009, 26(4): 555-562.
[9]	吴晶晶, 荆继武, 王跃武, 林璟锵, 刘怡聪. 真实应用环境下的PKI信任模型[J]. 中国科学院大学学报, 2009, 26(3): 389-399.
[10]	施妍冯登国赵险峰. 基于Gabor小波特征确认多媒体消息数字水印版权标识[J]. 中国科学院大学学报, 2007, 24(4): 494-500.
[11]	卢凤清，林东岱. 认证测试的一个扩展[J]. 中国科学院大学学报, 2007, 24(4): 488-493.
[12]	王卫平; 朱卫未; 陈文惠; 梁樑. 基于网络的入侵检测系统数据包采样策略研究[J]. 中国科学院大学学报, 2006, 23(4): 534-542.
[13]	王大印; 林东岱; 吴文玲; 姜中华. XOR-MAC消息认证码的安全性新证明[J]. 中国科学院大学学报, 2006, 23(2): 257-262.
[14]	刘海蛟; 荆继武; 林璟锵; 杜皎. 一种入侵容忍的资料库[J]. 中国科学院大学学报, 2006, 23(1): 46-51.
[15]	莫燕, 张玉清, 李学干. SSL3.0基本握手协议的运行模式分析[J]. 中国科学院大学学报, 2005, 22(4): 511-517.

安全协议分析的界——综合模型检查与Strand Spaces(英文)

Some Bounds on Security Protocol Analysis——Combining Model Checking and Strand Spaces

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

访问统计

联系我们