Welcome to Journal of University of Chinese Academy of Sciences,Today is

›› 2002, Vol. 19 ›› Issue (3): 288-294.DOI: 10.7523/j.issn.2095-6134.2002.3.011

Previous Articles     Next Articles

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

LIU Yi-Wen, LI Wei-Qin   

  1. Department of Computer Science and Engineering, Beijing University of Aeronautics and Astronautics, Beijing 100083
  • Received:2002-06-06 Online:2002-05-18

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

CLC Number: