摘要： 提出绑定项理论并用该理论构建认证协议的必要条件定理，使用串空间理论证明该定理和3个典型认证协议。该理论能够迅速、有效地判定有缺陷的认证协议的认证属性，除了能够对认证协议的新鲜性、主体进行判定外，还能够对具有类型攻击缺陷的认证协议进行判定，为认证协议的安全判定提供一种简单、有效的理论方法。

关键词: 认证协议, 绑定项理论, 串空间理论, 必要条件, 形式化理论

Abstract: This paper proposes a binding term theory and constructs the proposition of the prerequisites of authentication protocols based on the binding term theory, which is proved by strand space theory. It takes three classical authentication protocols as examples to verify the proposition proposed. The proposition can decide not only the freshness and the validity of principals, but also the authentication protocols containing type attack flaw. And a simple and effective formal method is provided for deciding security properties of authentication protocols.

Key words: authentication protocol, binding term theory, strand space theory, prerequisite, formal theory

中图分类号: 

• TP301