期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
3
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
TMN密码协议的SMV分析
被引量:
5
1
作者
张玉清
王春玲
冯登国
《计算机研究与发展》
EI
CSCD
北大核心
2003年第2期258-262,共5页
密码协议安全性的分析是网络安全的一个难题 ,运用形式方法对密码协议进行分析一直是该领域的研究热点 运用模型检测工具SMV对TMN密码协议进行了形式分析 在建立一个有限状态系统模型和刻画TMN密码协议安全性质的基础上 ,使用SMV对TMN...
密码协议安全性的分析是网络安全的一个难题 ,运用形式方法对密码协议进行分析一直是该领域的研究热点 运用模型检测工具SMV对TMN密码协议进行了形式分析 在建立一个有限状态系统模型和刻画TMN密码协议安全性质的基础上 ,使用SMV对TMN密码协议进行了安全分析
展开更多
关键词
tmn密码协议
SMV
分析
形式方法
网络安全
密码
体制
计算机通信网
移动通信
下载PDF
职称材料
多智体系统时态认知规范的模型检测算法
被引量:
9
2
作者
吴立军
苏开乐
《软件学报》
EI
CSCD
北大核心
2004年第7期1012-1020,共9页
模型检测技术一直以来主要是检验用时态逻辑描述的规范,人们很少注意认知逻辑的模型检测问题,而在分布式系统领域,系统和协议的规范已广泛地采用知识逻辑来描述.着重研讨了时态认知逻辑的模型检测算法.在SMV(symbolicmodelverifier)模...
模型检测技术一直以来主要是检验用时态逻辑描述的规范,人们很少注意认知逻辑的模型检测问题,而在分布式系统领域,系统和协议的规范已广泛地采用知识逻辑来描述.着重研讨了时态认知逻辑的模型检测算法.在SMV(symbolicmodelverifier)模型检测器的基础上,根据知识的语义和集合理论,提出了多种检验知识和公共知识的算法,从而使SMV的检测功能由时态逻辑扩充到时态认知逻辑.这些方法也适用于其他以状态集合作为输出的模型检测方法和工具的功能扩充.
展开更多
关键词
符号模型检测
多智体系统
协议
验证
SMV
tmn密码协议
下载PDF
职称材料
多主体系统时态认知规范的“On the Fly”模型检测算法研究
被引量:
2
3
作者
吴立军
苏开乐
+1 位作者
陈清亮
杨志华
《计算机研究与发展》
EI
CSCD
北大核心
2006年第8期1417-1424,共8页
时态认知逻辑已被广泛应用于分布式系统和协议的规范描述,模型检测时态认知规范已成为一个新的研究领域,因此着重研讨时态认知规范的“OntheFly”模型检测算法·在“OntheFly”模型检测时态逻辑描述规范的基础上,根据自动机理论、...
时态认知逻辑已被广泛应用于分布式系统和协议的规范描述,模型检测时态认知规范已成为一个新的研究领域,因此着重研讨时态认知规范的“OntheFly”模型检测算法·在“OntheFly”模型检测时态逻辑描述规范的基础上,根据自动机理论、深度优先方法和知识的语义,提出了“OntheFly”模型检测时态认知规范的算法,该算法在模型检测带有知识算子的时态规范时,在找到一个反例之前,往往只需构造系统的部分甚至小部分状态空间,从而避免了时态认知规范的模型检测中内存不足和状态爆炸等问题,实现了“OntheFly”模型检测时态认知规范,并且算法的复杂性是多项式时间的·最后,通过该方法在验证TMN密码协议中的应用来作为一个例子说明该方法的有效性·
展开更多
关键词
自动机
时态认知逻辑
模型检测
多主体系统
协议
验证
tmn密码协议
下载PDF
职称材料
题名
TMN密码协议的SMV分析
被引量:
5
1
作者
张玉清
王春玲
冯登国
机构
中国科学院研究生院信息安全国家重点实验室
中国科学院研究生院国家计算机网络入侵防范中心北京
西安工程科技学院计算机学院
出处
《计算机研究与发展》
EI
CSCD
北大核心
2003年第2期258-262,共5页
基金
国家自然科学基金 (60 10 2 0 0 460 2 73 0 2 760 2 73 0 2 9)
文摘
密码协议安全性的分析是网络安全的一个难题 ,运用形式方法对密码协议进行分析一直是该领域的研究热点 运用模型检测工具SMV对TMN密码协议进行了形式分析 在建立一个有限状态系统模型和刻画TMN密码协议安全性质的基础上 ,使用SMV对TMN密码协议进行了安全分析
关键词
tmn密码协议
SMV
分析
形式方法
网络安全
密码
体制
计算机通信网
移动通信
Keywords
formal method
tmn
cryptographic protocol
SMV
分类号
TP393.08 [自动化与计算机技术—计算机应用技术]
TN929.5 [电子电信—通信与信息系统]
下载PDF
职称材料
题名
多智体系统时态认知规范的模型检测算法
被引量:
9
2
作者
吴立军
苏开乐
机构
中山大学计算机科学与技术系
河南科技大学电子信息工程学院
出处
《软件学报》
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 [自动化与计算机技术—控制理论与控制工程]
下载PDF
职称材料
题名
多主体系统时态认知规范的“On the Fly”模型检测算法研究
被引量:
2
3
作者
吴立军
苏开乐
陈清亮
杨志华
机构
中山大学计算机科学与技术系
出处
《计算机研究与发展》
EI
CSCD
北大核心
2006年第8期1417-1424,共8页
基金
国家自然科学基金项目(60496327
10410638
+2 种基金
60473004)
德国科学研究基金项目(446CHV113/240/0-1)
广东省自然科学基金项目(04205407)~~
文摘
时态认知逻辑已被广泛应用于分布式系统和协议的规范描述,模型检测时态认知规范已成为一个新的研究领域,因此着重研讨时态认知规范的“OntheFly”模型检测算法·在“OntheFly”模型检测时态逻辑描述规范的基础上,根据自动机理论、深度优先方法和知识的语义,提出了“OntheFly”模型检测时态认知规范的算法,该算法在模型检测带有知识算子的时态规范时,在找到一个反例之前,往往只需构造系统的部分甚至小部分状态空间,从而避免了时态认知规范的模型检测中内存不足和状态爆炸等问题,实现了“OntheFly”模型检测时态认知规范,并且算法的复杂性是多项式时间的·最后,通过该方法在验证TMN密码协议中的应用来作为一个例子说明该方法的有效性·
关键词
自动机
时态认知逻辑
模型检测
多主体系统
协议
验证
tmn密码协议
Keywords
automata
temporal logics of knowledge
model checking
multi-agent system
verification of protocol
tmn
cryptographic protocol
分类号
TP309 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
TMN密码协议的SMV分析
张玉清
王春玲
冯登国
《计算机研究与发展》
EI
CSCD
北大核心
2003
5
下载PDF
职称材料
2
多智体系统时态认知规范的模型检测算法
吴立军
苏开乐
《软件学报》
EI
CSCD
北大核心
2004
9
下载PDF
职称材料
3
多主体系统时态认知规范的“On the Fly”模型检测算法研究
吴立军
苏开乐
陈清亮
杨志华
《计算机研究与发展》
EI
CSCD
北大核心
2006
2
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部