Journal of University of Chinese Academy of Sciences >
Some Bounds on Security Protocol Analysis——Combining Model Checking and Strand Spaces
Received date: 2002-06-06
Online published: 2002-05-18
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.
LIU Yi-Wen , LI Wei-Qin . Some Bounds on Security Protocol Analysis——Combining Model Checking and Strand Spaces[J]. Journal of University of Chinese Academy of Sciences, 2002 , 19(3) : 288 -294 . DOI: 10.7523/j.issn.2095-6134.2002.3.011
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
/
| 〈 |
|
〉 |