共查询到19条相似文献,搜索用时 140 毫秒
1.
提出一种分析和设计认证协议的新逻辑,可以用来分析认证协议和设计认证协议。通过运用该逻辑,使认证协议的设计和分析可以在同一种逻辑中进行,也消除了用不同的方法来设计和分析认证协议的不一致性。在分析协议时,先用逻辑对协议进行形式化,再用推理规则对协议进行推理。如果不能推理出协议的最终目标,说明协议存在缺陷或者漏洞。在设计协议时,通过运用合成规则使协议设计者可用一种系统化的方法来构造满足需要的协议。用该逻辑对Needham-Schroeder私钥协议进行了分析,指出该协议不能满足协议目标,并重新设计了该协议。 相似文献
2.
对认证协议进行了研究,指出采用保密服务是设计认证协议是一种安全服务的误用,存在两种潜在的安全隐患。针对带密钥的单向函数提出了一种扩展的BAN逻辑。利用该逻辑对两种改进的公钥认证协议进行形式化分析,说明带密钥的单向函数所提供的两种安全服务能够保证公钥认证协议的安全。 相似文献
3.
Levente Buttyan等人提出了一种认证协议设计的简单逻辑,协议设计者可以使用该逻辑,用一种系统的方法来构造认证协议。该文把简单逻辑和串空间(Strand Space)模型结合起来,给出了简单逻辑的串空间语义,然后运用该语义证明了简单逻辑的推理规则是正确的。 相似文献
4.
在传统的串空间基础上引入带变量的串空间模型,对于未确定的消息项或其子项用变量表示,允许变量出现在消息项及其演算中,协议由参与协议运行的不同主体的带变量的串组成。以协议运行的迹语义为模型,提出了一个用于推理协议主体的各种行为的模态逻辑系统,给出了该逻辑的语法、公理及推理规则。基本的模态公式 表示主体A完成动作P, 是相应的结果,通过主体行为的各种组合并绑定相应逻辑公式,最终推断安全协议的秘密性和可鉴别性。用该方法分析Helsinki协议,能发现其中的安全漏洞Horng-Hsu攻击。 相似文献
5.
针对程序的运行时动态攻击给远程证明带来的安全威胁,设计一种动态远程证明协议DRAP,对内存中处于运行状态的程序实施实时的动态度量,并向远程验证方证明平台实时状态。针对DRAP协议所用的TPM功能对LS2逻辑进行扩展,引入重置规则、时刻规则等新的推理规则,利用扩展的LS2逻辑对DRAP协议进行分析,分析表明DRAP中可重置配置寄存器中的扩展序列能够反映平台中程序的实时运行状态,并且在TPM可信和证明代理可信的前提下,远程验证者能够有效验证平台的实时可信状态。 相似文献
6.
7.
8.
为解决当前企业云内部部门之间通信时缺乏身份认证的问题,提出基于可信计算的企业云签证方法与协议,并对其进行证明和分析。在可信云vTPM架构基础上,通过设计vAIK签证协议,建立vTPM与企业云部门终端之间的身份对应关系并保证了vTPM签名能力的合法性。通过设计vTPM远程证明协议使得企业云内部通信时的消息发送方身份可验。vAIK签证过程中的报告由云平台签名、远程证明过程中的报告由云平台和vTPM共同签名以保证消息发送方的身份真实性,并在vAIK签证和远程证明过程中加入随机数保证报告新鲜性。最后使用SVO逻辑对vTPM证书签证和远程证明协议进行了证明与分析,结果表明该设计能够达到理想目标。 相似文献
9.
《计算机科学与探索》2016,(12):1701-1710
形式化方法是分析网络安全协议的一种重要方法,网络协议安全性也是信息安全领域的研究热点。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于证明网络安全协议的安全性。以事件逻辑为基础,定义强匹配及匹配会话,结合事件逻辑公理和推理规则,提出了强认证理论。利用该理论对有3个主体的Neuman-Stubblebine协议进行了研究,分析得出发送者是安全的而接收者是不安全的,从而证明了该协议是不安全的,说明了强认证理论适用于三方的网络安全协议。该理论适用于类似多方网络安全协议的安全性证明。 相似文献
10.
11.
一种分析Timed-Release公钥协议的扩展逻辑 总被引:6,自引:0,他引:6
在Coffey和Saidha提出的CS逻辑(CS逻辑将时间与逻辑结构相结合,可用于形式化分析Timed-release公钥协议的时间相关性秘密的安全性)的基础上,提出了CS逻辑的扩展逻辑,它更好地反映了Timed-release公钥协议的特性,并对一个协议实例进行了有效的形式化分析. 相似文献
12.
13.
14.
15.
公平的非否认密码协议及其形式分析与应用 总被引:17,自引:1,他引:16
在安全数据通信中,数据发送和接收的非否认性是一个极为重要的问题.近年来,实现这种类型的密码协议主要是通过可信第三方参与数据的加密与传送,因而,可信第三方的可靠性和安全性是系统性能的瓶颈.提出了一个公平的双方不可否认的密码协议——NCP(non-repudiation cryptographic protocol).这个协议解决了可信第三方的性能瓶颈问题,是一个更为有效的、安全的密码协议.用信任逻辑对其进行了形式分析,最后探讨了它在电子邮件中的应用. 相似文献
16.
17.
针对RFID标签所有权转移协议中存在的数据完整性受到破坏、物理克隆攻击、去同步攻击等多种安全隐私问题,新提出一种基于物理不可克隆函数(PUF)的超轻量级RFID标签所有权转移协议—PUROTP.该协议中标签所有权的原所有者和新所有者之间直接进行通信完成所有权转移,从而不需要引入可信第三方,主要涉及的运算包括左循环移位变换(Rot(X,Y))和异或运算($\oplus$)以及标签中内置的物理不可克隆函数(PUF),并且该协议实现了两重认证,即所有权转移之前的标签原所有者与标签之间的双向认证、所有权转移之后的标签新所有者与标签之间的双向认证.通过使用BAN(Burrows-Abadi-Needham)逻辑形式化安全性分析以及协议安全分析工具Scyther对PUROTP协议的安全性进行验证,结果表明该协议的通信过程是安全的,Scyther没有发现恶意攻击,PUROTP协议能够保证通信过程中交互信息的安全性及数据隐私性.通过与现有部分经典RFID所有权转移协议的安全性及性能对比分析,结果表明该协议不仅能够满足标签所有权转移过程中的数据完整性、前向安全性、双向认证性等安全要求,而且能够抵抗物理克隆攻击、重放攻击、中间人攻击、去同步攻击等多种恶意攻击.在没有额外增加计算代价和存储开销的同时克服了现有方案存在的安全和隐私隐患,具有一定的社会经济价值. 相似文献
18.
公钥密码体制下认证协议的形式化分析方法研究 总被引:5,自引:0,他引:5
本文通过对形式化方法中最广泛使用的类BAN逻辑进行研究发现,此方法更侧重于对称密码体制下认证协议的分析,而在分析基于公钥体制的认证协议时,该方法有很大的局限性。因此,文中针对公角密码的特点对类BAN逻辑进行了扩展。扩展后的逻辑方法能够更好地应用于分析公钥认证协议。 相似文献
19.
针对典型的安全协议验证逻辑存在的问题,如安全属性验证存在局限性、对混合密码原语的处理能力不强等,提出一种新的验证逻辑,新逻辑能够验证安全协议的认证性、密钥保密性、非否认性、可追究性、公平性及原子性。现有多数验证逻辑缺乏形式化语义,而逻辑语义能够证明逻辑系统的正确性,因此给出新逻辑所含逻辑构件的串空间语义,并应用串空间模型证明了新逻辑主要推理规则的正 确性。 相似文献