基于Duplication Authority的TPM2.0密钥迁移协议

《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》规范，而且可以保证迁移密钥的完整性、机密性和认证性.     

TPM可迁移密钥安全性分析与研究

TPM密钥迁移机制使密钥按照迁移特性分为了可迁移密钥和不可迁移密钥两类,本文深入分析可迁移密钥的安全性,指出可迁移密钥存在的安全问题.首先,利用密钥迁移机制,TPM所有者能将TPM内部可迁移密钥以迁移块的形式导出,解密迁移块能获得可迁移密钥私钥.其次,TPM用户能通过密钥迁移机制将非TPM产生的用户可控密钥构造成迁移块,作为迁移密钥导入到TPM内部.此外,用户使用TPM密钥加载命令能将非TPM产生的用户可控密钥作为TPM产生的可迁移密钥加载到TPM中.在对TPM规范理论分析的基础上,本文从技术角度给出了攻击可迁移密钥安全性的实现方法,并对部分安全问题提出了解决方案.通过分析,本文指出TPM提供密钥迁移机制的同时,也降低了可迁移密钥的安全保护强度.因此,用户在使用可迁移密钥时,应增强安全意识,在安全要求高的操作中尽量不要使用TPM可迁移密钥.     

密码协议的形式化分析

在分析四类常用密码协议形式化分析方法的基础上,阐述了各自的优缺点。探讨了形式化分析所面临的挑战,指出目前在这方面所做的工作以及有待发展的方向。     

可信平台模块的形式化分析和测试

可信平台模块(Trusted Platform Module,TPM)是可信计算平台的核心和基础,可信平台模块的功能测试和验证是保证可信平台模块的实现正确性以及规范一致性的重要手段,但是目前尚不存在一种有效严格的可信平台模块测试和功能验证方法,同时可信计算组织给出的TPM规范是描述性的,不利于产品的开发和测试.文中在分析可信平台模块目前存在的一些问题的基础上,以TPM密码子系统为例给出了该子系统的形式化规格说明,并且基于该规格说明,给出了扩展有限状态机模型,最后,将该有限状态机模型应用于测试用例的自动生成,并通过实验验证了形式化测试的有效性.     

一种不可否认协议形式化设计方法

针对目前尚无不可否认协议的形式化设计方法,提出一种基于逻辑的不可否认协议形式化设计方法,包括逻辑语言、定理、推理规则及合成规则。协议设计者用逻辑语言描述协议目标,由该目标出发,运用合成规则逐步推导出一个含可信第三方的不可否认协议。实例证明该方法可以很好地用于辅助不可否认协议的设计与改进。     

下一代TCM规范及芯片设计初探

本文分析了2008年颁布并开始执行的可信密码模块（TCM）规范方案,在特定情况下即CPU和操作系统不可信情况时的安全隐患,提出了第二代可信密码模块（TCM）标准的补充建议,并给出了一种高速TCM芯片的参考设计.     

因特网密钥交换协议研究

密钥交换协议是密码协议中主要的一类协议，安全可靠的密钥交换是通信安全性的基础，因特网密钥交换协议IKE作为IPSEC协议族的关键组成部分，在因特网的安全通信和安全服务中发挥着非常重要的作用，成为密码协议分析和研究的一个热点。该文首先介绍IKE协议，然后对协议中一种具体的密钥交换模式的安全性使用逻辑方法进行证明，并得出关于协议正确性的结论。     

认证协议攻击与非形式化分析

协议的分析验证方法有形式化与非形式化之分．很多代表性的协议虽然存在着缺陷，但对这些协议的非形式化分析，却可以提出一些值得借鉴的规则，参考这些规则可以避免和减少协议逻辑的漏洞，本文针对Woo-Lam两个改进协议以及SSL协议给出了攻击方法，分析协议存在的漏洞并提出如何使协议更为安全的建议。     

可信密码模块（TCM）芯片的虚拟化设计

本文介绍了一种中国标准可信密码模块（简称TCM）芯片的虚拟化方法,借助于本方法,可以为运行在同一台物理机器上的不同虚拟机分别提供相互隔离的、完整功能特性的虚拟TCM设备,对于虚拟机而言,该设备可以视为标准的TCM硬件进行操作并实现TCM标准所定义的所有完整功能。     

基于TCM构建安全可信的网络金融系统

本文提出了一种基于TCM可信密码模块构建安全可信的网络金融系统的方法。该可信网络金融系统可有效保证网络交易的完整性、可信性以及安全性,对我国金融信息化进程的加快具有一定意义。     

一种分析Timed-Release公钥协议的扩展逻辑

在Coffey和Saidha提出的CS逻辑(CS逻辑将时间与逻辑结构相结合，可用于形式化分析Timed-release公钥协议的时间相关性秘密的安全性)的基础上，提出了CS逻辑的扩展逻辑，它更好地反映了Timed-release公钥协议的特性，并对一个协议实例进行了有效的形式化分析．     

Formal Design of Cache Memory Protocols in IBM

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.     

基于TCM的可信签名系统设计

针对普通PC环境下的电子签名可能被恶意程序篡改、不能保证电子签名的真实性的问题,提出一种基于可信计算技术和嵌入式技术的嵌入式可信签名系统。该系统基于TCM设计了一个嵌入式可信电子签名终端,通过信任链的建立和平台完整性的证明构建了可信签名环境,并设计了可信环境下的签名和验签方案。由于系统设计的信任链基于嵌入式系统的核心可信度量根CRTM,信任链在终端启动时即开始建立,而非系统硬件启动后进行,保证了信任链的完整性和签名环境的可信性。     

公钥密码体制下认证协议的形式化分析方法研究

本文通过对形式化方法中最广泛使用的类BAN逻辑进行研究发现，此方法更侧重于对称密码体制下认证协议的分析，而在分析基于公钥体制的认证协议时，该方法有很大的局限性。因此，文中针对公角密码的特点对类BAN逻辑进行了扩展。扩展后的逻辑方法能够更好地应用于分析公钥认证协议。     

可信存储的密钥迁移模型及封装方案

文章分析了关于可信存储的各种规范和在各种情况下的设备更换方式,提出了三种密钥迁移模型。结合现有的密钥迁移技术,通过采用改进的封装方案,将源平台的各种软硬件的属性参数与所要迁移的密钥相绑定并封装的新方案。介绍了密钥与属性值的封装方式以及封装后的迁移过程。该方案保证了可信存储中密钥的迁移安全。     

密码协议形式化分析的计算合理性

基于Abadi-Rowgaway的形式化加密的计算合理性定理,论文提出和证明了密码协议形式化分析的计算合理性定理。通过对群密钥分配协议的分析,说明本文的定理对协议的可选择攻击具有较强的分析能力,论文提出了群密钥分配协议的形式化方法与计算方法下安全性的形式化定义,并证明了其合理性。