| 摘要: |
| Strand空间是一种新的安全协议分析模型.系统研究了使用Strand空间模型证明认证协议存在缺陷的方法.在证明过程中,使用目标细化方法证明了认证属性.通过在该模型中引入消息类型检查机制,简化了证明过程.并将该方法应用到包含三方主体的认证协议.最后得出与相关文献相同的结论. |
| 关键词: Strand空间 认证协议 协议证明 形式化方法 |
| DOI： |
| 分类号: |
| 基金项目:国家S219工程资助项目(2000-A32-09) |
|
| Study on the Proof Method of Authentication Protocols Based on Strand Space |
|
LIU Dong-xi,BAI Ying-cai
|
| Abstract: |
| 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 prinvolved three principals.At last,the results are got as the relevant literatures. |
| Key words: Strand space authentication protocol protocol proof formal method |
