串空间理论扩展.pdf

1000-9825/2005/16(10)1784 ©2005 Journal of Software Vol.16, No.10 ∗ 1+ 2 1,3 1,3 , , , 1( , 230026) 2(( ), 100080) 3( , 100083) Extending the Theory of Strand Spaces 1+ 2 1,3 1,3 SHEN Hai-Feng , XUE Rui , HUANG He-Yan , CHEN Zhao-Xiong 1(Department of Computer Science and Technology, University of Science and Technology of China, Hefei 230026, China) 2(State Key Laboratory of Information Security (Institute of Software, The Chinese Academy of Sciences), Beijing 100080, China) 3(Engineering Research Center of Computer Language Information, The Chinese Academy of Sciences, Beijing 100083, China) + Corresponding author: Phn: +86-10 Fax: +86-10 E-mail: supershf@, Received 2004-03-04; Accepted 2004-11-15 Shen HF, Xue R, Huang HY, Chen ZX. Extending the theory of strand spaces. Journal of Software, 2005,16(10):1784−1789. DOI: 10.1360/jos161784 Abstract : Current strand spaces model can not analyze some complex security protocols on account of their poor cryptographic primitives’ abstract. So it is very necessary to extend original theory of strand spaces so that it can be applied to analyze real world protocols. The penetrator’s strands are extended through adding signature, signature verification and HMAC (keyed-hashing for message authentication code) traces to them. A new notion of ideal is defined and the relevant propositions or theorems are therefore modified and proved. The extended honest ideals model not only inherits its original characters, but also is adaptive to the analysis of protocols with more cryptographic primitives such as JFK or IKE2. Key words: security protocol; strand spaces; ideal; honest