串空间模型的原理与应用

Theory and application of strand spaces model

介绍了安全协议形式化分析方法串空间模型的基本概念,给出了检查消息机密性的定理的变形公式,形式化地证明了由未泄漏私钥签字的消息起源于诚实主体串,并利用上述结论检验了BAN修改后的CCITTX.509(3)协议的机密性和认证性。

The basic notion of strand spaces model was introduced, then a equivalence formula checking secrecy of messages was given, and it was proven that a signed message by a confidential private key had its origin in a honest strand. Finally these two conclusions were used to check BAN modified version of CCITT X.509(3) protocol.