| 基于SMV的安全协议模型检验 |
| |
| 引用本文： | 刘锋,李舟军,李梦君,宋震,张艳. 基于SMV的安全协议模型检验[J]. 计算机工程与科学, 2004, 26(2): 28-31 |
| |
| 作者姓名： | 刘锋 李舟军 李梦君 宋震 张艳 |
| |
| 作者单位： | 国防科技大学计算机学院,湖南,长沙,410073;国防科技大学计算机学院,湖南,长沙,410073;武汉大学软件工程国家重点实验室,湖北,武汉,430072;四川大学数学学院,四川,成都,610064 |
| |
| 基金项目： | 国家自然科学基金资助项目(90104026)，国家863计划资助项目(2002.AA144 040)，高等学校重点实验室访问学者基金 |
| |
| 摘 要： | SMV是一个基于线性时态逻辑的符号化模型检验工具。本文利用SMV对Needham-Schroeder公钥协议的简化版本进行了验证，发现了利用消息重放进行的攻击。
|
| 关 键 词： | 模型检验 安全协议 认证 SMV |
| 文章编号： | 1007-130X(2004)02-0028-04 |
Security Protocol Model Checking Based on SMV |
| |
| LIU Feng,LI Zhou-jun,LI Meng-jun,SONG Zhen,ZHANG Yan. Security Protocol Model Checking Based on SMV[J]. Computer Engineering & Science, 2004, 26(2): 28-31 |
| |
| Authors: | LIU Feng LI Zhou-jun LI Meng-jun SONG Zhen ZHANG Yan |
| |
| Abstract: | SMV is a symbolic model checking tool based on linear temporal logic. In this paper we verify the Needham-Schroeder protocol by SMV, and finally find out an attack sequence which is achieved by replaying messages. |
| |
| Keywords: | model checking security protocol authentication SMV |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与科学》浏览原始摘要信息 |
|
点击此处可从《计算机工程与科学》下载全文 |
|
