Abstract: It is the first time to prove the Miao Xianghua’s modified version of Needham-Schroeder protocol with the theory of strand space which is a rising formal analysis tool. Its authentication is analysed, the analysis contains responser’s authentication and sponsor’s authentication. Its confidentiality is analysed, and two concepts “honest” and “ideal” are used to simplify the process of verification. It indicates that K, Nb, Nb0 are secret. Result shows that the amended N-S protocol can reach the goal, and it is consistent with the result of Miao Xianghua’s analysis.

Key words: N-S protocol, strand space, authentication, confidentiality

摘要： 针对缪祥华提出的改进的Needham-Schroeder 协议，利用一种新兴的形式化分析工具——串空间模型对其进行分析。对协议的认证性，包括响应者认证、发起者认证和协议的机密性进行分析，并运用“理想”和“诚实”2个概念简化分析协议的步骤，证明了K, Nb, Nb0是保密的。结果表明改进的N-S协议能够达到协议的安全目标，并与缪祥华分析的结果一致。

关键词: N-S协议, 串空间, 认证性, 机密性

CLC Number: 

• TP309