密码协议的SMV分析:实例研究

›› 1999, Vol. 25 ›› Issue (S1): 156-158.

密码协议的SMV分析:实例研究

张玉清,朱宏儒,肖国镇

西安电子科技大学信息保密研究所西安,710071,西安电子科技大学信息保密研究所西安,710071,西安电子科技大学信息保密研究所西安,710071

发布日期:1999-12-29

Using SMV for Cryptographic Protocol Analysis: A Case Study

Zhang Yuqing, Zhu Hongru, Xiao Guozhen

(Institute of Information Security, Xi'an University of EIectronic Science and Technology, Xi'an 710071)

Published:1999-12-29

摘要/Abstract

摘要： SMV是分析有限状态系统的一种工具。提出了使用SMV来分析密码协议的方法。为了说明这种方法的可村住，用SMV分析了Needham－Schroeder公钥协议。并成功地找到了对此协议的著名攻击．

关键词: 模型检测, Needham－Schroeder公钥密码协议, SMV

Abstract: SMV is a tool for checking finite state systems. In this paper, a methodology is presented for using SMV to analyzecryptographic protocols. We illustrate the feasibility of the approach by analyzing Needham-Schroeder Public-Key Protocol and discover thewell-known attack upon the Protocol.

中图分类号:

TN918.1

张玉清,朱宏儒,肖国镇. 密码协议的SMV分析:实例研究[J]. , 1999, 25(S1): 156-158.

Zhang Yuqing, Zhu Hongru, Xiao Guozhen. Using SMV for Cryptographic Protocol Analysis: A Case Study[J]. , 1999, 25(S1): 156-158.

[1]	彭程炜, 杨晋吉, 杨光. SAP-AKA二次认证协议的形式化验证与改进[J]. 计算机工程, 2025, 51(6): 204-211.
[2]	谢娜, 谭文安, 曹彦, 赵璐. 移动边缘计算中安全信息流建模与分析[J]. 计算机工程, 2022, 48(5): 35-42,52.
[3]	任胜兵,张健威,吴斌,王志健. Spark环境下基于SMT的分布式限界模型检测[J]. 计算机工程, 2017, 43(6): 19-23,29.
[4]	唐郑熠,王金水,何栋炜,薛醒思,胡文瑜. 馈线自动化算法的形式化建模与验证[J]. 计算机工程, 2016, 42(3): 89-93.
[5]	赵璐,张健沛,杨静. 收缩候选回溯集的有状态动态偏序归约方法[J]. 计算机工程, 2015, 41(5): 70-76.
[6]	劳佳琪,文中华,伍小辉,唐杰. 一种快速求强规划解的算法[J]. 计算机工程, 2015, 41(3): 162-166.
[7]	许兴旺,骆翔宇. 基于MAS 模型检测与抽象的Web 服务验证[J]. 计算机工程, 2015, 41(3): 26-31,36.
[8]	龙凤,文中华,唐杰,王进宗. 不确定规划中可达关系的快速求解算法[J]. 计算机工程, 2015, 41(1): 196-199.
[9]	伍小辉,文中华,李洋,劳佳琪. 不确定规划中的多Agent带权值强规化算法[J]. 计算机工程, 2015, 41(1): 190-195.
[10]	余莹. 组合服务交互测试研究综述[J]. 计算机工程, 2013, 39(5): 78-83.
[11]	纪明宇，王海涛，陈志远. 基于自动机的概率计算树逻辑验证方法[J]. 计算机工程, 2013, 39(12): 285-289.
[12]	张一弛, 庞建民, 范学斌, 姚鑫磊. 基于模型检测的程序恶意行为识别方法[J]. 计算机工程, 2012, 38(18): 107-110.
[13]	周清雷, 张兵, 席琳. 基于模型检测的系统生存性分析[J]. 计算机工程, 2012, 38(17): 38-41.
[14]	袁开银, 郭瑞, 陆翔升, 吴尽昭. RGPS过程层元模型正确性验证[J]. 计算机工程, 2012, 38(15): 39-42.
[15]	张磊 , 马光胜, 修建新. 任务网络到时间自动机的等价模型验证[J]. 计算机工程, 2012, 38(13): 286-288.

选择文件类型/文献管理软件名称

选择包含的内容