收稿日期: 2002-06-06
网络出版日期: 2002-05-18
Some Bounds on Security Protocol Analysis——Combining Model Checking and Strand Spaces
Received date: 2002-06-06
Online published: 2002-05-18
Strand Spaces是一种用于分析安全协议的机器证明方法.简要介绍了 Strand Spaces的基本特点,分析了其优劣,提出了构造协议的理想子环的算法,并以此来约束协议入侵者的能力和协议并行运行的次数.将模型检查与 Strand Spaces结合在一起,提出了一种综合分析方法来验证协议的安全特性,该方法可充分发挥模型检查与 Strand Spaces二者的优势.
关键词： 安全协议分析; 模型检查; Strand Spaces; 定理证明
刘怡文 , 李伟琴 . 安全协议分析的界——综合模型检查与Strand Spaces(英文)[J]. 中国科学院大学学报, 2002 , 19(3) : 288 -294 . DOI: 10.7523/j.issn.2095-6134.2002.3.011
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.
1. Wilt Marrero, Edmund Clarke, Somesh Jha. A Model Checker for Authentication Protocols. In: C Meadows, H Orman, editors.Proceedings of the DIMACS Workshop on Design and Verication of Security Protocols. DIMACS, Rutgers University, 1997
2. C:[owe. Towards a Completeness Result for Model Checking of Security Protocols. Technical Report, Dept of Mathematics and Computer Science. University of f.eicester, 1998
3. F Javier Thayer Fabrega, Jonathan C Herzog, Joshua D Gunman. Strand Spaces: Proving Security Protocols Correct. Journal of Computer Security, 1999,7:191一230
4. F Javier Thayer Fabrega, Jonathan C Herzog, Joshua D (Gunman. Strand Space Pictures. In: Presented at the LICS Workshop on Formal Methods and Security Protocols, 1998
5. Lawrence C Paulson. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security, 1998
6. i.awrence C Paulson. Proving Properties of Security Protocols by Induction. In: 10th IEEE Computer Security Foundations Work-shop, IEEE Computer Society Press, 1997, 70一83
7. f.iu Yiwen, f.i Weiqin. The Model Reasoning Verifier for Cryptographic Protocols. In:Proceedings of the sixth International Confer-ence for Young Computer Scientist. 2001.290一295
8. Liu Yiwen, Li Weiqin. Hierarchy Requirements and Verification for Cryptographic Protocols (in Chinese).Journal of Beijing Univer-sity of Aeronautics and Astronautics, 2002
/
| 〈 |
|
〉 |
