提出了保证认证协议安全性的2个条件:主体的活现性和会话密钥的保密性、新鲜性和关联性,并形式化证明了2个条件满足基于不可区分性的安全性定义.以Needham-Schroeder认证协议和SSL协议为例,说明分析认证协议是否满足2个条件的方法,以及如何根据安全属性的缺失直接构造攻击.基于2个条件的安全性分析方法不仅能用于证明协议正确,也能用于查找协议漏洞.该分析方法与攻击者的具体行为描述和多协议运行环境无关,是安全性的精确量化指标,其简单、有效,能帮助研究人员分析和改善认证协议设计.
This paper presented the guarantee of security adequacy for an authentication protocol, the liveness of a principal and the confidentiality, freshness and association of a freshness component. The authentication protocol with this guarantee was proved SK-security based on indistinguishable approach. The paper demonstrated, via Needham-Schroeder protocol and SSL protocol, the method to achieve the security properties of an authentication protocol and how to construct but not merely discover attacks from the absence of the security properties. The guarantee of security adequacy can either establish the correctness of an authentication protocol convincingly provided that it meets the specific security adequacy, or find flaws in that which is not secure. The guarantee of security adequacy is simple and it will benefit researchers to improve their authentication protocols.