期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到4篇文章
< 1 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
安全协议形式化分析工具比较研究 被引量：3
1
作者 陆思奇 程庆丰 赵进华 《密码学报》 2014年第6期568-577,共10页
形式化分析方法已经成为协议分析的主流方法之一.目前,国内针对形式化分析工具的研究很少,工具之间的比较研究也不够充分.一方面,当前比较研究存在参比工具较少以及参比性能不全面的问题,另一方面,大部分比较研究仅停留在理论比较,并没... 形式化分析方法已经成为协议分析的主流方法之一.目前,国内针对形式化分析工具的研究很少,工具之间的比较研究也不够充分.一方面,当前比较研究存在参比工具较少以及参比性能不全面的问题,另一方面,大部分比较研究仅停留在理论比较,并没有提供实验数据.因此,本文首先对AVISPA、Pro Verif、Maude-NPA、Scyther、Tamarin等当前主流形式化分析工具的背景、工具性能、应用范围等方面进行介绍,然后以SSH协议为目标协议,利用不同的形式化工具对SSH协议进行分析.根据实验分析结果,对比研究工具在运行性能、运行效率、底层算法、使用界面、安全模型等方面的优势和劣势.在对比研究结果的基础上,从形式化分析工具的使用和开发两方面进行讨论:在工具使用方面,通过工具比较研究,用户可以根据目标协议特性挑选合适的工具,对协议实现准确高效的分析;在工具开发方面,通过工具比较研究,指出代数性质扩展以及状态空间的限制和搜索算法是当前工具性能提升的重点和难点,突出了工具开发者需要掌握的用户需求,为工具开发提供理论基础. 展开更多
关键词 形式化分析工具 比较研究 SSH协议 安全模型
下载PDF
形式化工具Scyther优化与实例分析 被引量：5
2
作者 韩旭 陆思奇 程庆丰 《信息安全研究》 2016年第3期272-279,共8页
当前安全协议形式化分析工具发展迅速,针对不同的安全协议、不同的安全模型挑选合适的工具进行分析,不仅可以提高分析结果的可信度和准确性,还可以大大提高协议分析的效率.为此,对当前主流的9种形式化分析工具的性能进行梳理,从使用界... 当前安全协议形式化分析工具发展迅速,针对不同的安全协议、不同的安全模型挑选合适的工具进行分析,不仅可以提高分析结果的可信度和准确性,还可以大大提高协议分析的效率.为此,对当前主流的9种形式化分析工具的性能进行梳理,从使用界面、分析效率、安全模型等综合角度来看,Scyther工具有着较大的优势;为方便国内协议分析者使用和研究,剖析Scyther的底层算法,将其交互界面进行汉化,并增添了时间计算功能,对分析时间进行计算和输出;最后以网络安全协议TLS为例,利用优化后的Scyther工具分别在Delov-Yao模型和强安全模型下对其进行形式化分析.对研究工作者准确、有效地选择和使用形式化分析工具有着理论意义和实践价值. 展开更多
关键词 形式化分析工具 Scyther工具 比较研究 安全模型 TLS协议
下载PDF
eXtended Triple Diffie-Hellman协议的安全性分析 被引量：1
3
作者 刘佳路 刘璟 +3 位作者 杨佳宁 宋恒贤 雷欣雨 陈慧 《计算机应用》 CSCD 北大核心 2022年第S01期160-165,共6页
针对X3DH(eXtended Triple Diffie-Hellman)协议安全性的问题,使用形式化分析工具OFMC(On-the-Fly Model-Checker)和协议建模语言AnB对协议进行验证。首先,在Types部分对协议涉及到的通信实体进行了建模;然后,在Knowlegde部分规定了各... 针对X3DH(eXtended Triple Diffie-Hellman)协议安全性的问题,使用形式化分析工具OFMC(On-the-Fly Model-Checker)和协议建模语言AnB对协议进行验证。首先,在Types部分对协议涉及到的通信实体进行了建模;然后,在Knowlegde部分规定了各通信实体的先验知识;其次,在Actions部分对协议的协商流程进行了建模;最后,在Goals部分对协议的机密性、完整性、双向鉴别性等安全目标进行了建模。实验结果表明,X3DH协议作为Signal协议的核心,实现了密钥协商协议所要求的机密性、完整性、双向鉴别性等安全目标,并且形式化分析工具既可以减少工作量,又可以发现人工不易发现的协议漏洞,从而更加全面、高效地验证协议的安全性。 展开更多
关键词 X3DH协议 形式化分析工具 OFMC Signal协议
下载PDF
两个认证密钥协商协议的前向安全性分析 被引量：1
4
作者 程庆丰 马玉千 《电子与信息学报》 EI CSCD 北大核心 2022年第12期4294-4303,共10页
目前,网络安全及隐私受到广泛关注。前向安全性是Günther在1989年提出的一种认证密钥协商协议(AKA)的安全属性(doi:10.1007/3-540-46885-4_5),该性质经过30年的蓬勃发展已经成为研究领域的热点之一。该文主要分析了MZK20和VSR20两... 目前,网络安全及隐私受到广泛关注。前向安全性是Günther在1989年提出的一种认证密钥协商协议(AKA)的安全属性(doi:10.1007/3-540-46885-4_5),该性质经过30年的蓬勃发展已经成为研究领域的热点之一。该文主要分析了MZK20和VSR20两个AKA协议。首先在启发式分析的基础上,利用BAN逻辑分析了MZK20协议不具有弱前向安全性;其次利用启发式分析和Scyther工具证明了VSR20协议不具备前向安全性。最后,在分析VSR20协议设计缺陷的基础上,提出了改进方案,并在eCK模型下证明了改进后协议的安全性;并且,结合Scyther软件证明了改进VSR20协议与VSR20协议相比明显提高了安全性。 展开更多
关键词 安全协议形式化工具分析 认证密钥协商协议 前向安全性
下载PDF
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 下一页 到第 页
使用帮助 返回顶部