-
题名互联网密钥交换协议的SMV分析
被引量：6
- 1
-
-
作者
常亮
古天龙
郭云川
-
机构
桂林电子工业学院计算机系
-
出处
《计算机工程与应用》
CSCD
北大核心
2005年第19期154-157,173,共5页
-
文摘
该文基于SMV对新版本的互联网密钥交换协议(IKEv2)进行了分析。在对IKEv2协议进行形式建模,以及应用CTL对相应的安全性质进行形式描述的基础上,利用SMV分析了协议的认证性、秘密性和完整性,发现了两个攻击,并对这两个攻击所产生的影响进行了讨论。
-
关键词
ike协议
模型检测
smv
-
Keywords
ike protocol,model checking,smv
-
分类号
TP393.08
[自动化与计算机技术—计算机应用技术]
-
-
题名基于SMV的安全协议模型检验
被引量：4
- 2
-
-
作者
刘锋
李舟军
李梦君
宋震
张艳
-
机构
国防科技大学计算机学院
武汉大学软件工程国家重点实验室
四川大学数学学院
-
出处
《计算机工程与科学》
CSCD
2004年第2期28-31,62,共5页
-
基金
国家自然科学基金资助项目(90104026)
国家863计划资助项目(2002.AA144040)
高等学校重点实验室访问学者基金
-
文摘
SMV是一个基于线性时态逻辑的符号化模型检验工具。本文利用SMV对Needham-Schmeder公钥协议的简化版本进行了验证,发现了利用消息重放进行的攻击。
-
关键词
smv
安全协议
消息重放
计算机网络
网络安全
-
Keywords
model checking
security protocol
authentication
smv
-
分类号
TP393.08
[自动化与计算机技术—计算机应用技术]
-
-
题名密码协议的SMV分析:实例研究
被引量：1
- 3
-
-
作者
张玉清
朱宏儒
肖国镇
-
机构
西安电子科技大学信息保密研究所
-
出处
《计算机工程》
CAS
CSCD
北大核心
1999年第S1期156-158,共3页
-
基金
国家自然科学基金
-
文摘
SMV是分析有限状态系统的一种工具。提出了使用SMV来分析密码协议的方法。为了说明这种方法的可村住，用SMV分析了Needham－Schroeder公钥协议。并成功地找到了对此协议的著名攻击．
-
关键词
模型检测
Needham-Schroeder公钥密码协议
smv
-
Keywords
model checking
Needham-Schroeder public-key cryptographic protocol
smv
-
分类号
TN918.1
[电子电信—通信与信息系统]
-
-
题名基于SMV的安全协议建模及类型缺陷攻击发现
- 4
-
-
作者
李东建
陆际光
-
机构
中南民族大学计算机科学学院
-
出处
《中南民族大学学报（自然科学版）》
CAS
2005年第2期68-71,共4页
-
文摘
在分析安全协议模型的基础上,探讨了基于SMV工具的安全协议的建模及发现类型缺陷攻击的方法,对Otway-Rees协议的建模和分析表明,该方法对于发现类型缺陷攻击是有效的.
-
关键词
类型缺陷
模型检验
安全协议
符号模型检验
-
Keywords
type flaw
model checking
security protocol
smv
-
分类号
TP393
[自动化与计算机技术—计算机应用技术]
-
-
题名IKEv2协议的SPIN模型检测
被引量：9
- 5
-
-
作者
陈大伟
董荣胜
郭云川
古天龙
-
机构
桂林电子工业学院计算机系
-
出处
《计算机工程》
CAS
CSCD
北大核心
2006年第5期164-166,246,共4页
-
基金
广西省自然科学基金资助项目(0542052)
-
文摘
基于模型检测技术,使用SPIN对IKEv2协议进行了建模和分析。应用Promela语言描述了协议模型,并用LTL规约了该协议需要满足的认证性和秘密性,最后对检测结果进行了分析。
-
关键词
ike协议
模型检测
SPIN
PROMELA
-
Keywords
ike protocol
model checking
SPIN
Promela
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名一种适合于低成本标签的RFID双向认证协议
被引量：7
- 6
-
-
作者
赵跃华
王益维
李晓聪
-
机构
江苏大学计算机科学与通信工程学院
-
出处
《计算机应用研究》
CSCD
北大核心
2010年第5期1885-1888,共4页
-
文摘
在分析现有一些RFID认证协议的基础上,提出了一种新的适合低成本标签的双向认证协议,并对其进行了SMV模型检测形式化证明和性能分析。结果表明该认证协议具有认证性、保密性和完整性,能够满足低成本标签的安全需求,并且在安全性能提高的同时仍具有较好的执行性能。
-
关键词
低成本标签
射频识别
安全协议
认证
smv模型检测
-
Keywords
low-cost tags
RFID（radio frequency identification）
security protocol
authentication
smv model checking
-
分类号
TN915.08
[电子电信—通信与信息系统]
-
-
题名安全支付协议的设计与验证研究
被引量：3
- 7
-
-
作者
彭勋
董荣胜
郭云川
蔡国永
-
机构
桂林电子工业学院计算机系
-
出处
《计算机工程与应用》
CSCD
北大核心
2005年第6期139-143,共5页
-
基金
广西自然科学基金(编号:0229051)的资助
-
文摘
安全支付协议是实现电子商务在线支付的关键。目前缺乏同时支持电子商品和实物商品的在线支付协议,基于此,该文给出了一种同时支持这两类商品交易的安全支付协议,最后使用SMV工具对协议的原子性进行了分析并验证了其可行性。
-
关键词
安全支付协议
SEP安
全性
原子性
符号模型验证
smv
-
Keywords
secure payment protocol,SEP,security,atomicity,symbolic model checking,smv
-
分类号
TP393.04
[自动化与计算机技术—计算机应用技术]
-
-
题名多智体系统时态认知规范的模型检测算法
被引量：9
- 8
-
-
作者
吴立军
苏开乐
-
机构
中山大学计算机科学与技术系
河南科技大学电子信息工程学院
-
出处
《软件学报》
EI
CSCD
北大核心
2004年第7期1012-1020,共9页
-
基金
国家自然科学基金
广东省自然科学基金~~
-
文摘
模型检测技术一直以来主要是检验用时态逻辑描述的规范,人们很少注意认知逻辑的模型检测问题,而在分布式系统领域,系统和协议的规范已广泛地采用知识逻辑来描述.着重研讨了时态认知逻辑的模型检测算法.在SMV(symbolicmodelverifier)模型检测器的基础上,根据知识的语义和集合理论,提出了多种检验知识和公共知识的算法,从而使SMV的检测功能由时态逻辑扩充到时态认知逻辑.这些方法也适用于其他以状态集合作为输出的模型检测方法和工具的功能扩充.
-
关键词
符号模型检测
多智体系统
协议验证
smv
TMN密码协议
-
Keywords
symbolic model checking
multi-Agent system
verification of protocol
smv
TMN cryptographic protocol
-
分类号
TP18
[自动化与计算机技术—控制理论与控制工程]
-
-
题名密码协议的符号模型检测及分析
被引量：3
- 9
-
-
作者
龙士工
罗文俊
李祥
-
机构
贵州大学计算机软件与理论研究所
-
出处
《计算机应用》
CSCD
北大核心
2005年第1期138-140,共3页
-
基金
贵州省自然科学基金资助项目(20043029)
贵州工业大学校内基金资助项目(2004402)
-
文摘
对密码协议模型检测的方法作了理论上的研究,并用SMV检测工具给出了一个实际分析的例子。结果表明,利用符号模型检测方法分析并发现密码协议重放攻击的漏洞是一种行之有效的方法。
-
关键词
密码协议
符号模型检测
smv
-
Keywords
cryptographic protocol
symbolic model checking
smv
-
分类号
TP309
[自动化与计算机技术—计算机系统结构]
-
-
题名基于四方的安全电子商务支付协议分析与验证
被引量：6
- 10
-
-
作者
肖仕成
李开
甘早斌
-
机构
华中科技大学计算机学院
-
出处
《计算机科学》
CSCD
北大核心
2012年第3期75-78,92,共5页
-
基金
国家自然科学基金(70672041)
湖北省自然科学基金(2007ABA307)
中央高校基本科研业务费(2010MS112)资助
-
文摘
以基于四方的安全电子商务支付协议为研究对象,建立了协议的有限状态模型以及安全计算树逻辑CTL公式,利用符号模型检测工具SMV对协议的原子性进行检测验证。验证结果证明,基于四方的安全电子商务支付协议满足电子支付的金钱原子性、商品原子性以及确认发送原子性,协议符合电子支付的原子性安全要求。
-
关键词
电子商务支付协议
模型检测
smv
原子性
-
Keywords
E-commerce payment protocol, model checking, smv, Atomicity
-
分类号
TP309
[自动化与计算机技术—计算机系统结构]
-
