共查询到18条相似文献，搜索用时 328 毫秒
1.
分析了模型检测技术和逻辑推证技术的优点与不足,并在此基础上提出了一种混合的形式化分析技术的说明,该技术可提供更为完全的安全协议形式化分析. 相似文献
2.
给出用PVS对密码协议进行形式化规范的一种方法.该方法以高阶逻辑为规范语言,利用trace模型来描述协议的行为,并假设系统中存在强攻击者和理想加密系统.重要的结构如消息、事件、协议规则等都通过语义编码方式定义. 相似文献
3.
随着互联网的应用和发展,各种类型的安全协议,包括具有多个角色、多种密码运算的复杂密码协议,已广泛应用于分布式系统中解决各种安全需求.在大规模分布式网络环境下,参与协议运行的主体是大数量的甚至是动态的,密码协议运行环境极为复杂,这使得密码协议的安全性描述和分析变得非常复杂.引入了一个新的代数系统刻画具有多种密码运算的消息代数,并提出了一个新的密码协议模型,描述了无边界网络中的攻击模式,通过建立形式语言规范了无边界网络环境下密码协议的运行环境和安全性质 该协议模型描述了一种“协同攻击”模式,并讨论了密码协议的安全性分析约简技术,给出一个新的安全自动分析过程的简要描述. 相似文献
4.
TCP是Internet最常见的传输控制协议.本文首先介绍TCP协议的传输控制原理;然后讨论为什么传统TCP协议不适合移动无线网络,并分析移动无线网络中改善TCP协议的三种典型方法;最后总结出针对移动无线网络TCP协议改进的思路. 相似文献
5.
针对网络通讯软件的Fuzzing技术受限于协议格式,尤其是未知协议难以保证测试效果,提出了基于符号表达式的协议分析方法.将数据包关键处理代码翻译为符号表达式,利用符号表达式的丰富含义加快未知协议格式分析,并依此开发了协议格式分析及漏洞挖掘框架PAVD.通过对亿邮客户端的漏洞测试,验证了PAVD能有效提升协议分析效率,为网络通讯软件Fuzzing测试提供良好的支持. 相似文献
6.
本文用BR模型对TLS握手协议进行了计算分析与安全性证明. TLS握手协议作为典型的认证密钥交换协议,可以自然结合到BR认证协议计算模型分析框架当中. 本文对该协议主要通信过程进行了总结、建模和分析,证明当协议所采用的公钥加密函数和消息认证函数均满足计算模型安全性要求时,TLS握手协议在BR计算模型下是安全的. 相似文献
7.
Strand Spaces是一种用于分析安全协议的机器证明方法.简要介绍了 Strand Spaces的基本特点,分析了其优劣,提出了构造协议的理想子环的算法,并以此来约束协议入侵者的能力和协议并行运行的次数.将模型检查与 Strand Spaces结合在一起,提出了一种综合分析方法来验证协议的安全特性,该方法可充分发挥模型检查与 Strand Spaces二者的优势. 相似文献
8.
依照下一代网络协议的发展趋势,分析IETF提出的SIP协议和P2P网络结合的P2P-SIP网络的特点,针对其优势和不足提出一个基于椭圆曲线算法并适用于IPv6的P2P-SIP无证书匿名通信协议,使用CK安全模型对方案的安全性进行了证明. 对协议的安全性分析表明,该协议具有相互认证、完美前向保密性、匿名性、已知密钥安全、非密钥泄露伪装等安全属性;协议可抵御已知密钥攻击、中间人攻击、SYBIL攻击等攻击. 通过与已知协议的比较可知,该协议有更好的安全性和效率. 相似文献
9.
谢定华 《厦门广播电视大学学报》2006,(2)
SIP作为下一代互联网中的核心协议之一,其应用领域不断扩大.本文概述了SIP协议的重要内容,分析了一个基于SIP协议的IP电话的呼叫流程,并探讨SIP协议的扩展应用,最后提出SIP协议亟待解决的一些问题. 相似文献
10.
给出了应用于不同系统的不变式的概述, 分析了彼此之间的关系, 进行了分类, 并探讨了其未来发展趋势.密码协议的形式化分析日渐引起人们的广泛关注.这导致了不变式生成与描述技术的发展.不变式是对入侵者可知和不可知消息的定义, 可用于协议认证和秘密性的证明, 从而成为许多协议形式化分析工具和技术的核心 相似文献
11.
在两方密码协议运行模式分析法的基础上,利用模型检测的理论结果,提出了三方密码协议运行模式分析法。用这种方法对DavisSwick协议进行了分析,成功地验证了此协议的安全性,说明了所提出的三方密码协议运行模式分析法的有效性。 相似文献
12.
提出一个基于混合密码体制的抗否认密码协议 :可以运行在不安全信道上实现交易的公平性与通信双方的不可否认性;在通常情况下只需通信双方进行 3次信息的交互,且保证传递数据的机密性与收发方交易的隐私权;避免了可信第三方可能成为系统瓶颈的问题.最后给出该协议的形式化分析,证明了它的公平性、安全性与可行性. 相似文献
13.
以生成随机共享值、安全共享乘法与加法的常数轮协议为基础,给出有限域K上多项式的Shamir共享,并构造常数轮协议,使得网络可以安全判定K[x]中两个多项式是否互素.所构造协议的安全性基于已知基本协议的安全性. 相似文献
14.
针对密码模块API的形式化验证,提出一种基于项重写形式化模型的检测算法. 该算法利用符号化及广度优先搜索方法,使用项重写规则对敌手的初始知识集不断进行匹配和扩展,直到找到攻击路径或者搜索完状态空间. 以密码模块API标准PKCS#11为例具体实现了该检测算法,通过5个实验完成了对PKCS#11对称密钥管理部分API的形式化验证. 实验结果表明,该方法能有效检测针对PKCS#11的攻击,并找到一个新的攻击序列. 相似文献
15.
公平交换协议与传统的安全协议有所不同,导致公平交换协议的设计原则与传统的安全协议设计原则有所区别,因此,必须根据公平交换协议的特点重新考虑一些要素。本文根据公平交换协议的特点,另外给出了4条针对公平交换协议的设计原则,并以攻击为实例来说明这些原则的重要性。这些原则与传统的安全协议的设计原则结合起来,使得公平交换协议从设计的开始就能够考虑各种可能会出现的错误与漏洞,从而大大提高协议设计的质量。 相似文献
16.
Ad hoc网络的密钥管理技术是影响Ad hoc网络发展的重要因素,本文对Ad hoc现存密钥管理技术进行了研究。在基于身份密码系统的基础上,提出了UCKG（User Contributed Key Generation）密钥生成策略及分布式密钥管理协议,克服了身份密码系统存在PGC欺骗以及需要安全信道分发密钥的缺陷。对UCKG分布式密钥管理协议使用NS工具进行了性能仿真,当网络具有较好的连通性时,提出的密钥管理协议具有较好的性能。 相似文献
17.
利用码分多址技术的保密性、抗干扰性和多址通信能力,结合认证密钥和Hash函数,设计了一种适用于RFID系统且具有防碰撞功能的安全认证协议. 理论和分析表明:与常用的安全认证协议相比,新协议在保证一定复杂度基础上,不仅能有效地解决标签的碰撞问题,而且可抵抗包括重传、跟踪、阻断和篡改在内的多种攻击手段,尤其针对来自系统内安全威胁,具有一定的安全性和实用性. 相似文献
18.
综述目前安全协议形式化分析的理论与方法,包括安全协议的分类与模型,安全协议形式化分析的 3种典型方法 (基于推理的结构性方法,基于攻击的结构性方法,基于证明的结构性方法 ),安全协议分析的形式化语言,安全协议设计的形式化方法,以及安全协议形式化分析面临的挑战. 相似文献