摘要：针对密码认证协议的类型缺陷问题,细粒度地刻画了该类协议的消息类型结构特征,提出并证明了类型缺陷攻击存在性定理,基于原子消息加密数据结构及串空间模型提出了检测类型缺陷的形式化构造攻击方法,应用于密码认证协议的形式化分析,找到了一系列关于该类协议的类型缺陷攻击,指出了产生类型缺陷的根本原因以及修正措施,为了使密码协议设计渐趋精细化、标准化、科学化,给出了无消息-类型同态性、相似性、等价性等密码协议设计准则,突破了消息类型复杂多样、类型缺陷难以检测的密码协议设计关键技术.以Yahalom-Paulson协议为例,分析说明该方法的具体应用,检测出了该协议存在的两类类型缺陷攻击.理论推导和实例分析表明,经过该方法分析修正过的密码认证协议在Dolev-Yao模型规范的攻击者能力下能达到可证明安全,与其它的密码协议形式化工具方法相比较,该方法有明显的代数结构特征,而且形式化格式特征突出,极易判别,在全面检测密码协议的类型缺陷方面有优势,发现了一个在公开文献中未曾出现的Wide-Mouth Frog协议的新攻击.