| 运用ASM描述安全协议 |
| |
| 引用本文： | 薛锐,冯登国.运用ASM描述安全协议[J].中国科学院研究生院学报,2002,19(3):263-270. |
| |
| 作者姓名： | 薛锐 冯登国 |
| |
| 作者单位： | 1. 中国科学院软件所信息安全国家重点实验室,北京,100080;山西师范大学数学与计算机科学学院,临汾,041004
2. 中国科学院软件所信息安全国家重点实验室,北京100080 |
| |
| 基金项目： | 国家973重点研究发展规划项目（G1999035802），山西省归国留学生基金资助 |
| |
| 摘 要： | 介绍了抽象状态机（ASM）,建立了基于这种形式化方法的协议描述于验证的环境,并建立了一般意义上的入侵者模型.作为应用实例,给出了 Helsinki协议的 ASM规约,说明利用这个规约可以直观的演绎 Horng-Hsu攻击.
|
| 关 键 词： | 抽象状态机 密码协议 形式化方法 形式归约 |
| 修稿时间： | 2002年6月6日 |
Specifying Security Protocols with ASM |
| |
| XUE Rui,FENG Deng-Guo.Specifying Security Protocols with ASM[J].Journal of the Graduate School of the Chinese Academy of Sciences,2002,19(3):263-270. |
| |
| Authors: | XUE Rui FENG Deng-Guo |
| |
| Abstract: | The primary elements of Gurevich's Abstract State Machines(ASM)are introduced. A verification enviroment is proposed for analying of security protocols in ASM,and a general penetrator model is presented so that much of security properties could be dealed with. As a case, Helsinki protocol are specified in the model,a direct mathematical proof of its weakness is given. |
| |
| Keywords: | abstract state machine cryptographic protocol formal method formal specification |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
