基于Strand空间的认证协议证明方法研究  

Study on the Proof Method of Authentication Protocols Based on Strand Space

作　　者：刘东喜[1] 白英彩[1] 

机构地区：[1]上海交通大学计算机科学与工程系,上海200030

出　　处：《软件学报》2002年第7期1313-1317,共5页Journal of Software

基　　金：国家S219工程资助项目(2000-A32-09)

摘　　要：Strand空间是一种新的安全协议分析模型.系统研究了使用Strand空间模型证明认证协议存在缺陷的方法.在证明过程中,使用目标细化方法证明了认证属性.通过在该模型中引入消息类型检查机制,简化了证明过程.并将该方法应用到包含三方主体的认证协议.最后得出与相关文献相同的结论.Strand space is a new model for the analysis of security protocols. In this paper, a systematic study is made on how to prove the existence of vulnerabilities in authentication protocols based on the Strand space. During the proof procedure, the authentication property is proved by using the goal-refined method. Moreover, by introducing type-check mechanism into this model, the proof procedure is simplified significantly. In addition, this method is also applied to authentication protocols involved three principals. At last, the same results are got as the relevant literatures.

关 键 词：STRAND空间 认证协议 协议证明 形式化方法 密码 信息安全 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]