共查询到16条相似文献,搜索用时 78 毫秒
1.
《TPM-Rev-2.0-Part-1-Architecture-01.38》国际标准允许用户基于密钥复制接口设计迁移协议,此复制接口通过innerwrap和outerwrap为密钥迁移提供机密性、完整性和认证性.但研究发现,基于该复制接口来设计密钥迁移协议存在3个问题:其一是缺少交互双方TPM的相互认证,会导致密钥能够在敌手和TPM间迁移;其二是当迁移密钥的属性encryptedDuplication=0且新父密钥的句柄newParentHandle=TPM_RH_NULL时,复制接口不能实施innerwrap和outerwrap,迁移密钥将以明文传输而造成泄露;其三当新父密钥是对称密钥时,innerwrap中的对称加密密钥以及outerwrap中的密钥种子如何在源TPM与目标TPM之间安全交换,《TPM-Rev-2.0-Part-1-Architecture-01.38》并没有给出具体的解决办法.针对上述问题,提出了基于Duplication Authority的密钥迁移协议.该协议以Duplication Authority为认证和控制中心,将密钥迁移过程分为初始化阶段、认证和属性获取阶段以及控制和执行阶段.Duplication Authority通过判定密钥的复制属性和类型、新父密钥的密钥类型和句柄类型来决定迁移流程.考虑了各种合理的属性组合,共设计了12种迁移流程.最后对该协议进行了安全分析和实验验证,结果显示,该协议不仅完全满足《TPM-Rev-2.0-Part-1-Architecture-01.38》规范,而且可以保证迁移密钥的完整性、机密性和认证性. 相似文献
2.
TPM密钥迁移机制使密钥按照迁移特性分为了可迁移密钥和不可迁移密钥两类,本文深入分析可迁移密钥的安全性,指出可迁移密钥存在的安全问题.首先,利用密钥迁移机制,TPM所有者能将TPM内部可迁移密钥以迁移块的形式导出,解密迁移块能获得可迁移密钥私钥.其次,TPM用户能通过密钥迁移机制将非TPM产生的用户可控密钥构造成迁移块,作为迁移密钥导入到TPM内部.此外,用户使用TPM密钥加载命令能将非TPM产生的用户可控密钥作为TPM产生的可迁移密钥加载到TPM中.在对TPM规范理论分析的基础上,本文从技术角度给出了攻击可迁移密钥安全性的实现方法,并对部分安全问题提出了解决方案.通过分析,本文指出TPM提供密钥迁移机制的同时,也降低了可迁移密钥的安全保护强度.因此,用户在使用可迁移密钥时,应增强安全意识,在安全要求高的操作中尽量不要使用TPM可迁移密钥. 相似文献
3.
在分析四类常用密码协议形式化分析方法的基础上,阐述了各自的优缺点。探讨了形式化分析所面临的挑战,指出目前在这方面所做的工作以及有待发展的方向。 相似文献
4.
可信平台模块的形式化分析和测试 总被引:9,自引:0,他引:9
可信平台模块(Trusted Platform Module,TPM)是可信计算平台的核心和基础,可信平台模块的功能测试和验证是保证可信平台模块的实现正确性以及规范一致性的重要手段,但是目前尚不存在一种有效严格的可信平台模块测试和功能验证方法,同时可信计算组织给出的TPM规范是描述性的,不利于产品的开发和测试.文中在分析可信平台模块目前存在的一些问题的基础上,以TPM密码子系统为例给出了该子系统的形式化规格说明,并且基于该规格说明,给出了扩展有限状态机模型,最后,将该有限状态机模型应用于测试用例的自动生成,并通过实验验证了形式化测试的有效性. 相似文献
5.
6.
7.
8.
认证协议攻击与非形式化分析 总被引:5,自引:0,他引:5
协议的分析验证方法有形式化与非形式化之分.很多代表性的协议虽然存在着缺陷,但对这些协议的非形式化分析,却可以提出一些值得借鉴的规则,参考这些规则可以避免和减少协议逻辑的漏洞,本文针对Woo-Lam两个改进协议以及SSL协议给出了攻击方法,分析协议存在的漏洞并提出如何使协议更为安全的建议。 相似文献
9.
10.
11.
一种分析Timed-Release公钥协议的扩展逻辑 总被引:6,自引:0,他引:6
在Coffey和Saidha提出的CS逻辑(CS逻辑将时间与逻辑结构相结合,可用于形式化分析Timed-release公钥协议的时间相关性秘密的安全性)的基础上,提出了CS逻辑的扩展逻辑,它更好地反映了Timed-release公钥协议的特性,并对一个协议实例进行了有效的形式化分析. 相似文献
12.
Steven M. German 《Formal Methods in System Design》2003,22(2):133-141
We describe the formal design techniques currently used in IBM to develop cache protocol controllers for high-end servers. In our approach to formal design, formal specification and verification methods are incorporated into the hardware design process, starting from the earliest stages of a hardware project. We describe collaborations between a formal methods expert and hardware designers on two high performance server projects. Properties of the design are verified using both manual proof techniques and model checking. We discuss the modelling and model checking techniques we have developed and indicate future directions. 相似文献
13.
针对普通PC环境下的电子签名可能被恶意程序篡改、不能保证电子签名的真实性的问题,提出一种基于可信计算技术和嵌入式技术的嵌入式可信签名系统。该系统基于TCM设计了一个嵌入式可信电子签名终端,通过信任链的建立和平台完整性的证明构建了可信签名环境,并设计了可信环境下的签名和验签方案。由于系统设计的信任链基于嵌入式系统的核心可信度量根CRTM,信任链在终端启动时即开始建立,而非系统硬件启动后进行,保证了信任链的完整性和签名环境的可信性。 相似文献
14.
公钥密码体制下认证协议的形式化分析方法研究 总被引:5,自引:0,他引:5
本文通过对形式化方法中最广泛使用的类BAN逻辑进行研究发现,此方法更侧重于对称密码体制下认证协议的分析,而在分析基于公钥体制的认证协议时,该方法有很大的局限性。因此,文中针对公角密码的特点对类BAN逻辑进行了扩展。扩展后的逻辑方法能够更好地应用于分析公钥认证协议。 相似文献
15.