改进型Helsinki协议的串空间模型分析

Formal analysis to revised Helsinki protocol based on strand spaces

Helsinki协议是ISO/IECDIS11770-3中提出的重要认证协议,由于协议受到来自内部的攻击,Mithcell-Yeun对其进行了改进。但改进后协议的安全性仍未得到确认,为了验证改进协议是否满足其安全目标,利用串空间模型对协议进行了建模和分析。通过分析极小元所在串与其它串的关系说明协议的一致性,通过对理想的分析说明协议的保密性。结果表明改进型协议满足其安全要求,原协议存在安全缺陷的原因是最小元可能存在Mt串上,这为Mithcell-Yeun的改进提供了理论的证明与依据。

The Helsinki protocol is a key establish protocol contained in the ISO/IEC DIS 11770-3, MithcellandYenuproposearevised version of the protocol for the former attacked from the inner. However, the security of the revised protocol hasn＇t confirmed yet, to verify the security of the revised protocol, a modeling and analysis is proposed based on the strand space. The agreement of the protocol is determined by the relationship between the 〈_c minimal member and the other strand, the secret of the protocol is analysis based on the idea. The analysis proved the correctness of the protocol, and the cause of the formal protocol＇ s weakness is that the minimal member maybe on the M, strand, a theoretic support is provided to the revision.