可信计算技术的基本思想是:在通用计算平台上嵌入一个防篡改的硬件可信安全芯片,利用芯片的安全特性保证系统按照预期的行为执行,从根本上提高终端的安全性^[1].作为计算平台的信任基础,可信安全芯片提供了安全的存储功能、密码学计算功能,以及构建可信计算平台和远程证明所需的功能.目前,常用的可信安全芯片有两类:国际广泛使用的是符合可信平台模块(trusted platform module,简称TPM)标准^{[2, 3]}的TPM芯片,我国普遍使用的是符合国家密码管理局发布的可信密码模块(trusted cryptography module,简称TCM)标准^[4]的TCM芯片.

TCM是我国借鉴了国际可信计算技术框架与技术理念,在可信计算领域自主研制的安全芯片,其设计原则和技术思路与TPM存在较大不同:(1) TCM以椭圆曲线密码算法和对称密码算法^[5,6,7]为基础,计算效率高于TPM;(2) TCM密钥存储保护体系允许使用对称密钥作为存储密钥,提高了密钥管理的计算效率;(3) TCM身份密钥符合双证书体制,更适用于我国的公钥基础设施^[8];(4) TCM提供了一些TPM不具备的功能,如数据对称加密和密钥协商功能;(5) 参考TPM已经暴露出的安全隐患^[9],TCM对自身的功能进行了改进,如TCM授权协议增加了对重放攻击的抵抗能力.

TCM芯片具有密码学功能和受保护的存储空间,能够为可信计算平台提供密钥管理、平台数据保护、完整性存储与报告、身份标识等功能.其中,密钥管理是TCM的一个重要功能,因为密钥的安全存储和使用是TCM能够有效地提供其他各项功能的前提和基础.TCM用存储保护体系保证其密钥的安全性,同时,为满足用户在不同平台上使用同一密钥的需求,TCM提供了密钥迁移功能,使用户能够在不同TCM之间迁移密钥.TCM接口规范^[10]详细规定了用于密钥迁移功能的命令接口,用户可以依据该类接口设计和实现不同的密钥迁移协议.

现有TCM密钥迁移协议通常以被迁移密钥在目标TCM上的新父密钥作为迁移保护密钥,用该密钥的公钥加密被迁移密钥实现迁移.本文通过分析发现,该协议存在两个问题:(1) 限制了被迁移密钥的新父密钥为非对称密钥,导致被迁移密钥不能迁移到目标TCM的对称存储密钥下,违背了TCM允许使用对称密钥作为父密钥的设计原则,不能充分利用TCM的高效性;(2) 作为协议参与方的源TCM和目标TCM未进行相互认证,导致被迁移密钥能够被敌手获得,并且敌手能够在TCM中嵌入自己的密钥,破坏了TCM存储保护体系的安全性.

针对上述问题,本文提出两个新的TCM密钥迁移协议:协议1在遵循TCM接口规范的情况下,以目标TCM的平台加密密钥作为迁移保护密钥,使源TCM能够在认证目标TCM身份之后,将密钥迁移至目标TCM任意类型的存储密钥下,保证了源TCM迁出密钥的安全性;考虑到现有TCM密钥迁移类接口无法实现源TCM身份认证的实际情况,协议2在简单修改TCM接口的情况下,以源TCM和目标TCM进行SM2密钥协商得到的会话密钥保护迁移数据,既不需要限制新父密钥的类型,又在协议交互过程中增加了参与双方TCM的相互认证,有效解决了上文提出的两个问题.此外,协议2还具有前向安全性,能够保证即使TCM用于SM2密钥协商的长期私钥泄露,也不会破坏已迁移密钥的安全性.

本文对上述两个协议进行了形式化分析:首先,用多集重写系统^[11]对协议进行建模;然后,给出协议安全属性的形式化描述,包括协议正确性、源TCM迁出密钥的机密性、目标TCM迁入密钥的机密性以及协议2的前向安全性;最后,用自动定理证明工具Tamarin^[12]对上述安全属性进行验证.安全性分析结果表明:两个协议均满足预期的安全属性.

本文第1节简介TCM密钥迁移的相关背景知识.第2节介绍现有的TCM密钥迁移协议并指出其存在的问题.第3节详述本文提出的两个新的TCM密钥迁移协议.第4节对上述两个协议进行形式化分析,验证协议的安全性.第5节介绍可信安全芯片密钥迁移的相关研究工作.第6节总结全文.

1 背景知识

本节从TCM的密钥类型和结构、存储保护体系、密钥迁移类接口和密钥协商功能这4个方面介绍本文的背景知识.

1.1 密钥类型和结构 1.1.1 TCM密钥类型

TCM密钥按用途分为6种类型,本文将会用到其中的3种类型,即:

• 密码模块密钥(endorsement key,简称EK):用于标识TCM及其所在平台的身份的一个SM2密钥.每个TCM芯片都有唯一的EK,EK私钥永久存储在芯片内部,只在少数关键操作中执行解密操作;

• 存储密钥(storage key,简称SK):该密钥用于加密保护TCM存储保护体系中的密钥.按照所采用的加密算法,SK分为采用SM2算法的非对称存储密钥和采用SMS4算法的对称存储密钥;

• 平台加密密钥(platform encryption key,简称PEK):TCM为我国的双证书体制引入的新类型密钥,是具有身份标识作用的SM2密钥.PEK由可信第三方(trusted third party,简称TTP)生成,同时生成的还有PEK的公钥证书.TCM获得PEK以及PEK证书的流程是:TTP使用EK加密的数字信封将PEK密钥以及PEK证书发送给TCM,TCM用EK私钥解密数字信封以获得PEK和PEK证书.

TCM密钥按照是否具有迁移属性(migratable)可以分为可迁移密钥和不可迁移密钥两类:可迁移密钥可以从当前TCM迁移到另一个TCM中使用;不可迁移密钥只能在生成该密钥的TCM中使用.TCM通过其内部安全机制保证用户只能对可迁移密钥实施迁移.

1.1.2 TCM密钥结构

每个TCM密钥都分为公开区域和秘密区域两部分:前者包含指明密钥属性的各种字段,后者包含需要TCM保护的敏感字段.下面简介TCM密钥结构中与本文相关的一些字段.

• 公开区域

1) keyUsage:密钥用途,该字段为TCM_SM2KEY_STORAGE或TCM_SMS4KEY_STORAGE的密钥是SK类型密钥,该字段为TCM_SM2KEY_PEK的密钥是PEK类型密钥;

2) pubKey:密钥的公钥,对称密钥该字段值为空.

• 秘密区域

1) pubDataDigest:密钥公开区域的摘要值;

2) key:密钥的机密数据,对于非对称密钥,key为其私钥,对于对称密钥,key为密钥本身.

对任意密钥k,本文用k=(keyPub,keyPri)表示其结构,其中,keyPub=(keyUsage,pubKey)为其公开区域, keyPri=(pubDataDigest,key)为其秘密区域.

1.2 存储保护体系

TCM芯片内部的存储空间非常有限,因此,将所有密钥都存储在TCM内部是不现实的.为解决密钥的安全存储问题,TCM采用存储保护体系进行密钥管理,其思想是:利用密码学手段有效拓展TCM的存储空间,将密钥加密安全存储在TCM外部.

TCM存储保护体系是一个树形结构,该结构以存储主密钥(storage master key,简称SMK)为根节点,普通的存储密钥为中间节点,受保护的密钥或数据为叶节点.SMK是TCM所有者获得TCM所有权时TCM产生的一个SMS4密钥,该密钥是特殊的存储密钥,仅在TCM内部存储和使用.除SMK之外,任何TCM密钥生成时,都必须指定存储保护体系中已存在的存储密钥作为其父密钥.当新生成的密钥需要存储到TCM外部时,TCM用其父密钥对其秘密区域加密生成密钥包,将密钥包和公开区域存储在TCM外部.值得注意的是:TCM允许使用对称密钥作为存储密钥保护子密钥,提高了密钥管理的效率,这是TCM有别于TPM的一大优势,而且这种设计原则也被下一代的TPM规范^[3]所采纳.

1.3 密钥迁移接口

密钥迁移是指将一个TCM(源TCM)生成的密钥安全地转移至另一个TCM(目标TCM)的存储保护体系中,该功能主要用于密钥复制和备份.TCM接口规范为用户提供以下3个密钥迁移类命令.本文用

Command(inputparams)→(outputparams)

表示TCM命令,其中,Command为命令名,inputparams和outputparams分别为该命令的输入和输出参数列表.

命令1. 保护密钥授权:TCM_AuthorizeMigrationKey(migMode,mpkPub)→(migAuth).

此命令以迁移模式migMode和迁移保护密钥公钥mpkPub为输入,计算迁移授权数据migAuth,表明TCM所有者同意使用该迁移保护密钥(migration protection key,简称MPK)在migMode模式下进行迁移.计算得出的migAuth包括以下内容:(1) mpkPub;(2) migMode;(3) mpkPub,migMode和tcmProof三者的摘要值.其中,tcmProof是TCM内部一个机密的随机数,只有TCM知道,即使TCM所有者也不能得到此值.

命令2. 创建迁移数据:TCM_CreateMigratedBlob(hd_PK,migAuth,keyBlob)→(sblob,ablob).

此命令使用迁移保护密钥公钥对被迁移密钥的秘密区域进行保护,生成被迁移密钥的迁移包(sblob,ablob).保护机制由迁移模式决定:若迁移模式为REWRAP,则直接用迁移保护密钥公钥migAuth.mpkPub加密被迁移密钥的秘密区域得到ablob,此模式下,sblob为空;若迁移模式为MIGRATE,则TCM首先生成对称密钥sk,然后使用sk加密被迁移密钥的秘密区域得到sblob,之后用迁移保护密钥公钥migAuth.mpkPub加密sk,得到ablob.

命令3. 转换迁移数据:TCM_ConvertMigratedBlob(hd_MPK,hd_NPK,sblob,ablob)→(keyBlob).

TCM首先获得被迁移密钥的秘密区域:如果sblob为空,表明迁移模式为REWRAP,直接使用hd_MPK指向的密钥对ablob解密,即可获得被迁移密钥的秘密区域;如果sblob不为空,表明迁移模式为MIGRATE,使用hd_MPK指向的密钥对ablob解密,得到对称密钥sk,然后使用sk解密sblob,获得被迁移密钥的秘密区域.之后,TCM用新父密钥(new parent key,简称NPK),即hd_NPK指向的密钥加密获得的秘密区域,得到一个可以载入到目标TCM存储保护体系中新父密钥下的密钥包.

利用上述命令实施密钥迁移的流程如图 1所示.

在密钥迁移前,可迁移密钥k在源TCM的存储保护体系中,受其父密钥PK的保护,而迁移保护密钥MPK和新父密钥NPK则位于目标TCM的存储保护体系中.TCM密钥迁移主要包括3个步骤:(1) 源TCM所有者利用命令1对目标TCM的迁移保护密钥公钥mpkPub授权生成迁移授权数据,从而允许源TCM用户以该密钥为迁移保护密钥将可迁移密钥迁移到目标TCM中;(2) 源TCM用户以步骤(1)生成的迁移授权数据为参数调用命令2,创建迁移数据,生成用MPK加密的k的迁移包;(3) 目标TCM用户以步骤(2)生成的迁移包为参数调用命令3,将该迁移包转换为用NPK加密的k的密钥包.此后,可迁移密钥k就被迁移到目标TCM的存储保护体系中,受新父密钥NPK的保护.

1.4 密钥协商功能

利用TCM密钥协商功能,两个计算平台可以通过执行SM2密钥协商协议^[5]建立共享的会话密钥,并保证该密钥始终处于芯片的保护之中.TCM密钥协商包括3个步骤:交互双方的TCM各自生成临时SM2密钥;交互双方利用对方的公钥和临时密钥公钥、自身的私钥和临时密钥私钥,计算出共享的会话密钥;交互双方的TCM删除生成的临时密钥.由于共享密钥由交互双方的长期密钥和临时密钥共同计算得出,因此,该密钥协商协议提供了隐式的身份认证,交互双方可以确信只有对方可以得到协商出的共享密钥.

TCM提供了3个密钥协商类命令,本文需要用到其中的两个.

命令4. 创建协商会话:TCM_CreateKeyExchange()→(X,shd_X).

此命令创建密钥协商会话,生成参与方的临时密钥(x,X=g^x),并将其存储在会话中.其输入参数为空,输出参数为参与方的临时密钥公钥X和该密钥协商会话的句柄shd_X.

命令5. 释放协商会话:TCM_ReleaseExchangeSession(shd_X)→().

此命令以密钥协商会话句柄shd_X为输入,用于释放该句柄指向的TCM密钥协商会话.

2 问题描述

TCM密钥迁移协议包括5个参与实体:源TCM、源TCM的所有者、目标TCM、源TCM所在的主机、目标TCM所在的主机,其中,前3个实体是可信的,而源和目标TCM所在的主机被认为是不可信的.

本节首先介绍现在通用的TCM密钥迁移协议,然后详细分析该协议存在的问题.表 1为本文使用的符号及函数说明.

2.1 现在通用的密钥迁移协议

与TPM密钥迁移协议类似,现有TCM密钥迁移协议以被迁移密钥在目标TCM上的新父密钥(简称新父密钥)作为MPK,其流程描述如下,协议流程图如图 2所示.

(1) 传输保护密钥

    H_B将PK_B发送给H_A.

(2) 保护密钥授权

    1) O_A调用TCM_AuthorizeMigrationKey(migMode,PK_B);

    2) T_A接到调用后,计算migAuth=(PK_B,migMode,hash(PK_B,migMode,tcmProof)),返回migAuth给H_A.

(3) 创建迁移数据

    1) H_A调用TCM_CreateMigratedBlob($h{d_{P{K_A}}},migAuth,keyBlo{b_A}$);

    2) T_A接到调用后,首先验证migAuth,然后用$h{d_{P{K_A}}}$指向的$PK_A^ - $解密keyBlob_A得到keyPri,之后,根据migMode用PK_B保护keyPri:

        若migMode=REWRAP,则计算sblob=null,ablob=aenc(keyPri,PK_B);

         若migMode=MIGRATE,则生成对称密钥k,计算sblob=senc(keyPri,k),ablob=aenc(k,PK_B);

        最后返回sblob和ablob给H_A.

(4) 传输迁移数据

     H_A将sblob,ablob和keyPub发送给H_B.

(5) 转换迁移数据

     1) H_B调用TCM_ConvertMigratedBlob($h{d_{P{K_B}}},h{d_{P{K_B}}},sblob,ablob$);

     2) T_B接到调用后,首先根据sblob用第1个参数$h{d_{P{K_B}}}$指向的$PK_B^ - $解密keyPri:

        若sblob=null,则计算$keyPri = adec(ablob,PK_B^ - )$;

        否则,计算 $k = adec(ablob,PK_B^ - ),keyPri = sdec(sblob,k)$;

        然后,用第2个参数$h{d_{P{K_B}}}$指向的PK_B保护keyPri,即,计算keyBlob_B=aenc(keyPri,PK_B);

        最后返回keyBlob_B给H_B即完成了协议.

协议执行成功后,以keyPub,keyBlob_B和新父密钥句柄$h{d_{P{K_B}}}$为参数,就可以将被迁移密钥加载到T_B的存储保护体系中.

2.2 存在的问题

• 问题1

文献^[13]指出,上述协议存在一个问题:由于SMK为对称密钥,故其无法作为被迁移密钥的新父密钥,所以被迁移密钥只能迁移到目标TCM存储保护体系的第3层或者更低层次.事实上,通过分析发现:该问题不仅只是被迁移密钥在目标TCM存储保护体系的层次问题,其实质是该协议以新父密钥作为MPK,而MPK必须是非对称密钥,因此就限制了新父密钥只能为非对称密钥,从而导致被迁移密钥不能迁移到目标TCM的对称密钥下.而TCM相比于TPM的一个优势设计原则是允许使用对称密钥作为存储密钥以提高计算效率,所以此协议没有利用到TCM的优势,有悖于TCM设计初衷.

• 问题2

我们研究发现,该协议缺少源TCM和目标TCM间的身份认证,导致密钥能够在敌手和TCM间迁移,即,图 3中的两种情况:

1) 源TCM不能认证MPK是否是目标TCM的密钥,导致敌手可以用其控制的密钥迁移源TCM的密钥并获得密钥明文;

2) 目标TCM不能认证迁移数据是否来自源TCM,使敌手可以将其控制的密钥迁移到目标TCM中.

为解决以上问题,本文提出两个新的TCM密钥迁移协议,在保证被迁移密钥可以以任意类型的存储密钥为新父密钥的基础上,最大限度的增强协议参与方间的认证性.值得一提的是:目前所有的可信安全芯片,如TPMv1.2,TCM,TPM2.0,都没有能支持以对称存储密钥为新父密钥的密钥迁移协议.

3 新的TCM密钥迁移协议

本节介绍本文提出的两个TCM密钥迁移协议.

3.1 协议1

协议1使用目标TCM的PEK作为MPK进行迁移.此协议不需要改变TCM的命令接口,只需要增加新的迁移模式就能够实现,我们称该迁移模式为PEKMIGRATE.协议1由6个阶段组成:初始化、传输保护密钥、保护密钥授权、创建迁移数据、传输迁移数据和转换迁移数据,其流程描述如下,协议流程图如图 4所示.

(1) 初始化

    1) T_B将PEK参数发送给TTP;

    2) TTP首先按照给定参数生成PEK_B,$PEK_B^ - $和PEKCert_B,然后用PEK_B和$PEK_B^ - $根据TCM密钥结构构造$ke{y_{PE{K_B}}} = (keyPu{b_{PE{K_B}}},keyPr{i_{PE{K_B}}})$,之后生成对称密钥k₁和k₂,计算:

$a = senc(ke{y_{PE{K_B}}},{k_1}),b = aenc({k_1},E{K_B}),c = senc(PEKCer{t_B},{k_2}),d = aenc({k_2},E{K_B})$

        最后,将a,b,c和d发送给T_B;

    3) T_B打开a,b和c,d两个数字信封,得到$ke{y_{PE{K_B}}}$和PEKCert_B.

(2) 传输保护密钥

    H_B将PEK_B和PEKCert_B发送给H_A.

(3) 保护密钥授权

    1) O_A验证PEK_B和PEKCert_B后,调用TCM_AuthorizeMigrationKey(migMode,PEK_B),其中,

migMode=PEKMIGRATE;

     2) T_A接到调用后,计算migAuth=(PEK_B,migMode,hash(PEK_B,migMode,tcmProof)),返回migAuth给H_A.

(4) 创建迁移数据

    1) H_A调用TCM_CreateMigratedBlob($h{d_{P{K_A}}},migAuth,keyBlo{b_A}$);

     2) T_A接到调用后,首先验证migAuth,然后用$h{d_{P{K_A}}}$指向的$PK_A^ - $解密keyBlob_A得到keyPri,之后,根据 migMode用PEK_B保护keyPri:

        a) 生成随机种子seed,导出k₁=kdf(‘encryption’,seed),k₂=kdf(‘integrity’,seed);

        b) 计算a=senc(keyPri,k₁),b=hmac(a,k₂),sblob=(b,a);

        c) 计算ablob=aenc(seed,PEK_B),

        最后,返回sblob和ablob给H_A.

(5) 传输迁移数据

    H_A将sblob、ablob和keyPub发送给H_B.

(6) 转换迁移数据

    1) H_B调用TCM_ConvertMigratedBlob($h{d_{PE{K_B}}},h{d_{P{K_B}}},sblob,ablob$);

     2) T_B接到调用后,首先用$h{d_{PE{K_B}}}$指向的$PEK_B^ - $恢复出keyPri:

        a) 计算$seed = adec(ablob,PEK_B^ - )$,导出k₁=kdf(‘encryption’,seed),k₂=kdf(‘integrity’,seed);

        b) 将sblob的前32字节赋值给b,余下字节赋值给a;

        c) 验证b=hmac(a,k₂)后,计算keyPri=sdec(a,k₁);

        然后,用$h{d_{P{K_B}}}$指向的PK_B保护keyPri:

        若PK_B为非对称密钥,则计算keyBlob_B=aenc(keyPri,PK_B);

        若PK_B为对称密钥,则计算keyBlob_B=senc(keyPri,PK_B),

        最后,返回keyBlob_B给H_B即完成了协议.

此协议在数字信封的基础上加入了HMAC校验,用于保证迁移数据的完整性.目标TCM在接收到迁移数据后,首先检查HMAC校验值:如果不能通过校验则不进行迁移数据转换,省去了后续的解密步骤.

首先,此协议的一个优势是新父密钥可以是任意类型的存储密钥,即,允许使用高效率的对称密钥作为新父密钥;此外,此协议使用PEK_B作为MPK,O_A通过验证PEK_B和PEKCert_B可以确定其来自T_B,增加了T_A对MPK来源的认证,能够有效防止图 3中的第1种攻击.

3.2 协议2

通过分析TCM密钥迁移类命令接口,发现现有的3个接口均不能提供对源TCM身份的认证,导致目标TCM不能确定其收到的迁移数据是否真正来自源TCM,因此也就无法防止图 3中的第2种攻击.另外,协议1使用PEK保护被迁移密钥,而PEK是由外部的可信第三方生成后导入TCM内部的,如果PEK在外部泄露,那么所有被迁移密钥将不再安全,敌手可以获得被迁移密钥的秘密区域.因此,需要在密钥迁移协议中增加前向安全性(perfect forward secrecy,简称PFS),以保证已经迁移过的密钥的安全性.

为解决上述问题,本文提出了协议2.此协议使用SM2密钥协商协议得到的会话密钥保护被迁移密钥,迁移协议完成后,TCM删除临时密钥,使敌手不能再解密迁移数据.协议2需要简单修改TCM密钥迁移类接口,我们称此协议的迁移模式为KEYEXCHANGE.

3.2.1 接口修改

协议2需要修改第1.3节中的命令2、命令3,在此分别标记为命令6、命令7.

命令6. 创建迁移数据:TCM_CreateMigratedBlob($h{d_{PK}},migAuth,h{d_{PE{K_A}}},Y,keyBlo{b_A}$)→(X,sblob,ablob).

此命令使用源TCM和目标TCM进行SM2密钥协商协议得到的会话密钥对被迁移密钥的秘密区域进行保护,其保护机制与协议一的PEKMIGRATE模式相同.为计算与目标TCM共享的密钥,该命令比命令2中的原接口增加了两个输入参数:源TCM PEK密钥句柄$h{d_{PE{K_A}}}$、目标TCM临时密钥公钥Y和一个输出参数:源TCM临时密钥公钥X.

命令7. 转换迁移数据:TCM_ConvertMigratedBlob($h{d_{PE{K_B}}},sh{d_Y},PE{K_A},X,h{d_{P{K_B}}},sblob,ablob$)→(keyBlob_B).

该命令首先使用目标TCM的PEK私钥、临时密钥私钥和源TCM的PEK公钥、临时密钥公钥计算SM2密钥协商协议的共享密钥,用该密钥恢复被迁移密钥的秘密区域;然后,用新父密钥对其进行保护,得到一个可以载入目标TCM存储保护体系中新父密钥下的密钥包.为计算与源TCM共享的密钥,该命令比命令3中的原接口增加了3个输入参数:目标TCM密钥协商会话句柄shd_Y、源TCM PEK公钥PEK_A、源TCM临时密钥公钥X.

3.2.2 协议描述

协议2在原TCM密钥迁移协议5个参与实体的基础上,增加了一个参与实体:目标TCM的所有者,该实体被认为是可信的.协议2的流程描述如下,协议流程图如图 5所示.

(1) 初始化

    T_A和T_B采用与协议1中T_B相同的初始化方式进行初始化.初始化完成后,T_A得到$ke{y_{PE{K_A}}}$和PEKCert_A,T_B得到$ke{y_{PE{K_B}}}$和PEKCert_B.

(2) 传输保护密钥

     H_B将PEK_B和PEKCert_B发送给H_A.

(3) 保护密钥授权

    1) O_A验证PEK_B和PEKCert_B后,调用TCM_AuthorizeMigrationKey(migMode,PEK_B),其中:

migMode=KEYEXCHANGE;

    2) T_A接到调用后,计算migAuth=(PEK_B,migMode,hash(PEK_B,migMode,tcmProof)),返回migAuth给H_A.

(4) 传输临时密钥

    1) H_B调用TCM_CreateKeyExchange();

    2) T_B接到调用后,创建密钥协商会话,随机生成会话句柄shd_Y和临时密钥私钥y,计算临时密钥公钥Y=g^y,将临时密钥对(y,Y)存储在芯片内部与句柄shd_Y绑定,返回Y,shd_Y给H_B;

    3) H_B将Y发送给H_A.

(5) 创建迁移数据

    1) H_A调用TCM_CreateMigratedBlob($h{d_{P{K_A}}},migAuth,h{d_{PE{K_A}}},Y,keyBlo{b_A}$);

    2) T_A接到调用后,首先验证migAuth,然后用$h{d_{P{K_A}}}$指向的$PK_A^ - $解密keyBlob_A得到keyPri,之后,根据 migMode生成seed保护keyPri:

         a) 随机生成临时密钥私钥x,计算临时密钥公钥X=g^x;

        b) 计算seed=SM2KE(PEK_B,PEK_A,Y,X),导出k₁=kdf(‘encryption’,seed),k₂=kdf(‘integrity’,seed);

        c) 计算a=senc(keyPri,k₁),b=hmac(a,k₂),sblob=(b,a),ablob=null;

        最后,返回X,sblob和ablob给H_A,并删除临时密钥对(x,X).

(6) 传输迁移数据

     H_A将PEK_A,PEKCert_A,X,sblob,ablob和keyPub发送给H_B.

(7) 转换迁移数据

    1) O_B验证PEK_A和PEKCert_A后,调用:

TCM_ConvertMigratedBlob($h{d_{PE{K_B}}},sh{d_Y},PE{K_A},X,h{d_{P{K_B}}},sblob,ablob$);

     2) T_B接到调用后,首先用$h{d_{PE{K_B}}}$指向的$PEK_B^ - $、shd_Y指向的y,PEK_A,X计算seed,并恢复出keyPri:

        a) 计算seed=SM2KE(PEK_B,PEK_A,Y,X),导出k₁=kdf(‘encryption’,seed),k₂=kdf(‘integrity’,seed);

         b) 将sblob的前32字节赋值给b,余下字节赋值给a;

        c) 验证b=hmac(a,k₂)后,计算keyPri=sdec(a,k₁);

        然后,用$h{d_{P{K_B}}}$指向的PK_B保护keyPri:

        若PK_B为非对称密钥,则计算keyBlob_B=aenc(keyPri,PK_B);

        若PK_B为对称密钥,则计算keyBlob_B=senc(keyPri,PK_B);

        最后,返回keyBlob_B给H_B.

(8) 删除临时密钥

     1) O_B调用TCM_ReleaseExchangeSession(shd_Y);

    2) T_B接到调用后,删除shd_Y指向的临时密钥对(y,Y)即完成了协议.

首先,该协议不需要用新父密钥公钥保护迁移过程,从而免去了对新父密钥类型的限制,允许被迁移密钥迁移到目标TCM任意类型的存储密钥下;其次,此协议使用T_A和T_B的PEK作为长期密钥进行密钥协商,O_A和O_B通过验证PEK和PEK证书可以认证PEK的来源,从而实现了交互双方TCM的相互认证,能够防止图 3中的两种攻击;最后,此协议在迁移完成后删除参与计算SM2会话密钥的临时密钥,保证以后即使双方PEK私钥泄漏,敌手也不能计算出SM2会话密钥获得被迁移的密钥,从而保证了密钥迁移协议的前向安全性.

3.3 协议比较

对现有TCM密钥迁移协议(P0)和本文提出的协议1(P1)、协议2(P2)的比较结果见表 2.可以看出:

• 在符合TCM接口规范的情况下,P1比P0具有更好的适用性和安全性,即:既允许NPK为对称存储密钥,又能实现对目标TCM的身份认证;

• 而在修改TCM接口的情况下,P2比P1具有更强的安全性,该协议不仅增加了对源TCM身份的认证,而且满足了前向安全性.

4 形式化分析

首先介绍本文所采用的形式化分析方法,然后详细说明对协议1和协议2的正确性和安全性的证明过程.

4.1 分析方法介绍

本文用多集重写系统(multiset rewriting system)建模TCM密钥迁移协议,将协议步骤和敌手行为形式化描述为多集重写规则,并将协议的安全属性描述为一阶逻辑公式.然后,将上述模型编码为自动定理证明工具Tamarin的脚本,使用Tamarin对密钥迁移协议进行形式化分析.本节简介多集重写系统的语法、语义以及属性描述语言和证明工具Tamarin,详细介绍参见文献^[11].

4.1.1 基本语法

定义1. 项(term)用于建模密码学消息,由以下语法定义:

$ \begin{array}{l} t,{t_i}\quad : = \quad \;x\;\;\;\;\;\quad \quad \quad \;\;\;\,{\kern 1pt} {\kern 1pt} \;x \in V\\ \quad \quad {\rm{ }}\;|\;\;\quad n\quad \;\;\;\;\quad \quad \quad \;\;\;n \in FN \cup PN\\ \quad \quad \;\;|\;\;\quad f({t_1},...,{t_n})\quad \quad {\rm{ }}f \in {\Sigma _T} \end{array} $

其中,V是变量集合;FN是新鲜值集合;PN是公开值集合;∑_T是以下函数符号的集合:

$ \begin{array}{l} {\Sigma _T} = \{ aenc(\_,\_),\quad senc(\_,\_),\quad sign(\_,\_),\quad hash(\_,\_),\quad smke(\_,\_,\_,\_),\quad \langle \_,\_\rangle ,\\ \quad \quad \;\;adec(\_,\_),\quad sdec(\_,\_),\quad verify(\_,\_,\_),\quad hmac(\_,\_),\quad pk(\_),\quad kdf(\_),\quad true,\quad null\} . \end{array} $

其中,$\langle \_,\_\rangle $表示二元组,后文将 $\langle \langle a,b\rangle ,c\rangle $和$\langle a,\langle b,c\rangle \rangle $简写为$\langle a,b,c\rangle $;函数smke用于计算SM2密钥协商协议的共享秘密.

我们将∑_T中函数符号的代数性质形式化为等价理论E_T,E_T包含以下等式:

${E_T} = \left\{ \begin{array}{l} adec(aenc(m,pk(k)),k) \simeq m,\quad verify(sign(m,k),m,pk(k)) \simeq true,\\ sdec(senc(m,k),k) \simeq m,\quad smke(a,pk(b),x,pk(y)) \simeq smke(pk(a),b,pk(x),y) \end{array} \right\} $.

定义2. 事实(fact)定义为f:=F(t₁,…,t_n),t_i∈T,F∈∑_F.其中:T是项集合;∑_F是以下事实符号的集合:

$\begin{array}{l} {\Sigma _F} = \{ K(\_),\quad Out(\_),\quad In(\_),\quad Fr(\_),\quad !Cert(\_,\_),\quad !TTPKpair(\_,\_),\quad RequestPEK(\_),\\ \quad \quad \;\;{\kern 1pt} SHandle(\_,\_,\_,\_),\quad !Handle(\_,\_,\_,\_,\_),\quad !TCMEK(\_,\_),\quad !TCMProof(\_,\_)\} . \end{array} $

事实符号分为线性的和持久性的:前者建模只能使用一次的资源;后者除K(_)外均以“!”为前缀,用于建模可以任意使用的无穷资源.第1行符号分别建模敌手知识、输出消息、输入消息、新鲜值信息、实体公钥证书、TTP公私钥对和TCM的PEK请求;第2行符号分别建模TCM密钥协商会话句柄、TCM密钥句柄、TCM的EK公钥和TCM的tcmProof.例如:

• !Handle(A,hd,keyUsage,pubKey,key)是一个持久性事实,表明TCM A中存在一个密钥句柄,该句柄值为hd,指向一个用途为keyUsage的密钥,其公钥为pubKey,私钥为key;

• SHandle(A,shd,pubKey,key)表明TCM A中存在一个密钥协商会话句柄,该句柄值为shd,绑定的临时密钥对为(pubKey,key).该事实是一个线性事实,可以通过执行TCM_ReleaseExchangeSession命令被消耗.

本文用G表示不包含变量的事实的集合.

定义3. 一个多集重写规则由前提l、动作a和结论r组成,表示为l-[a]→r,其中,l,a和r是事实序列.对于多集重写规则集合R,ginst(R)表示R中不包含变量的实例的集合.

定义4. 消息推理规则MD由以下规则组成:

$\begin{array}{l} MD = \{ Out(x) - [\;] \to K(x),\quad K(x) - [K(x)] \to In(x),\quad Fr(x:fresh) - [\;] \to K(x:fresh),\\ \quad \quad \quad \,[\;] - [\;] \to K(x:pub),\quad K\left( {{x_1}} \right),...,K({x_k}) - [\;] \to K(f({x_1},...,{x_k}))|f \in {\Sigma _T}\} . \end{array} $

其中,x:s表示x是类型为s的变量.第1行规则分别建模敌手能够从公开信道接收消息、向公开信道发送消息和获得公开值;第2行规则分别建模敌手能够获得自己产生的新鲜值和对自己已知的消息应用∑_T中的函数.

定义5. 规则FRESH=([ ]-[ ]→Fr(x:fresh))表示生成新鲜值.所有新鲜值都由FRESH规则的唯一实例生成,即,该规则总是产生不同的新鲜值.

4.1.2 操作语义

多集重写规则的语义由一个转换系统(transition system)给出,转换系统的状态S是事实的多集.

记法:对于集合A,P(A)表示A的幂集,A^#表示A中元素的有限多集组成的集合.对于运算符,上标“#”表示多集上的运算,如 $ \cup $ ^#表示两个多集的并运算,Φ^#表示空多集.

定义6. 对于多集重写系统R和等价理论E_T,转换关系${ \to _{R,{E_T}}} \subseteq {G^\# } \times P(G) \times {G^\# }$由以下转换规则定义:

$\frac{l-[a]\to r{{\in }_{{{E}_{T}}}}ginsts(R\cup \{FRESH\})\text{ }\quad lfacts(l){{\subseteq }^{\#}}S\ \quad pfacts(l)\subseteq set(S)}{S{{\xrightarrow{set(a)}}_{R,{{E}_{T}}}}((S{{\backslash }^{\#}}lfacts(l)){{\cup }^{\#}}mset(r))}$.

其中,lfact(l)是l中线性事实的多集,pfact(l)是l中持久性事实的集合,set表示多集或序列所对应的集合,mset表示序列所对应的多集,${ \in _{{E_T}}}$表示模E_T的属于关系.

该转换规则建模一个重写规则实例重写状态S的过程:首先,${{\subseteq }^{\#}}$检查lfact(l)中的线性事实在S中发生足够多次,$\subseteq $检查pfact(l)中的持久性事实都在S中发生;然后,通过去掉S中已消耗的线性事实并增加新产生的事实,得到S的后继状态.转换关联的标记set(a)是规则实例对应的动作集合.

定义7. 迹(trace)集合用于建模协议执行,其定义为

$\begin{align} & trace{{s}_{{{E}_{T}}}}(R):=\{[{{A}_{1}},...,{{A}_{n}}]|\exists {{S}_{1}},...,{{S}_{n}}\in {{G}^{\#}}.\quad {{\Phi }^{\#}}{{\xrightarrow{{{A}_{1}}}}_{R,{{E}_{T}}}}{{S}_{1}}{{\xrightarrow{{{A}_{2}}}}_{R,{{E}_{T}}}}...{{\xrightarrow{{{A}_{n}}}}_{R,{{E}_{T}}}}{{S}_{n}}\wedge \\ & \quad \quad \quad \quad \quad \ \ \text{ }\forall i\ne j.\quad \forall x.\quad ({{S}_{i+1}}{{\backslash }^{\#}}{{S}_{i}})={{\{Fr(x)\}}^{\#}}\Rightarrow ({{S}_{j+1}}{{\backslash }^{\#}}{{S}_{j}})\ne {{\{Fr(x)\}}^{\#}}\}. \\ \end{align} $.

其中,第2个条件确保迹中FRESH规则的每个实例都不同.

4.1.3 属性描述语言

协议的安全属性建模为转换系统的迹属性,由一阶逻辑公式描述.

定义8. 迹公式(trace formula)是由迹原子(trace atom)产生的一阶公式.迹原子有以下5种类型:1) 恒假$ \bot $;2) 项相等t₁$ \approx $t₂;3) 时间点排序i时间点相等表示事实f在时间点i发生的动作f@i.

定义9. 对于等价理论E_T,迹tr、赋值θ和迹公式φ间的可满足关系定义为:

其中,idx(tr)表示tr索引的集合,tr_θ(i)表示tr的第θ(i)个元素,D_s表示类型s的定义域,θ[xau]表示将x映射到u、将a(a $ \ne $x)映射到θ(a)的函数.

定义10. φ是R,E可满足的(R,E-satisfiable),记为,当且仅当存在迹$tr \in trace{s_{{E_T}}}(R)$和赋值θ,使得成立.

定义11. φ是R,E有效的(R,E-valid),记为,当且仅当对任意$tr \in trace{s_{{E_T}}}(R)$和任意赋值θ都成立.

4.1.4 证明工具Tamarin

Tamarin^[12]是一个符号化的验证工具,支持安全协议的证伪和验证.该工具以描述为多集重写系统的协议作为输入,将其翻译为依赖图,然后用约束求解算法来验证表示为一阶逻辑公式的协议安全属性.对于可满足性断言,Tamarin验证协议迹集合中是否存在满足φ的迹;对于有效性断言,Tamarin验证协议迹集 合中是否存在不满足φ的迹.Tamarin不仅能验证Dolev-Yao模型下的安全属性,而且能验证复杂模型下的安全属性,如密钥协商协议中eCK模型下的安全属性^[14].

4.2 协议1分析

本节在Dolev-Yao模型下证明协议1的正确性和安全性.

4.2.1 协议描述

协议1中不可信实体可以被敌手控制,其行为和敌手行为一样,都通过第4.1节中的规则集合MD描述.协议1中可信实体的形式化描述如图 6所示,我们称该规则集合为P1.

规则1、规则2建模可信第三方的行为.规则1描述TTP初始化,该规则生成TTP私钥,发送TTP公钥.事实!TTPKpair(tk,pk(tk))表示TTP的私钥和公钥分别为tk和pk(tk);事实!Cert(TTP,pk(tk))表示TTP持有pk(tk)的公钥证书;动作OneTime()表示TTP仅初始化1次,被用在安全属性中的迹公式 $ {\alpha _{OT}}: = \left( {\forall ij.OneTime()@i \wedge OneTime()@j \Rightarrow i = j} \right)$中,该公式表示发生动作OneTime()的时间点都是相同的,从而限制规则1只能实例化1次,即,TTP只能产生唯一的证书颁发密钥和对应的公钥证书.规则2描述TTP为TCM生成PEK和颁发PEK证书,该规则接收TCM A的PEK请求,查找TCM A的EK公钥和TTP的公私钥对,然后为TCM A生成PEK和PEK证书,计算用TCM A的EK公钥加密的两个数字信封,两个数字信封分别包含生成的PEK密钥和PEK证书,并发送这两个数字信封.

规则3~规则5建模源和目标TCM的行为,事实符号!Handle中变量A的取值用以区分该规则实例发生在哪一个TCM中.规则3描述TCM激活和加载PEK,该规则接收包含PEK密钥和PEK证书的两个数字信封、TCM的EK密钥句柄和SMK密钥句柄,读取上述句柄对应的密钥信息,然后为PEK密钥生成句柄,发送该句柄、PEK的公开区域、SMK加密的PEK密钥包和PEK证书,并存储PEK密钥句柄对应的密钥信息.规则4、规则5分别描述TCM用对称和非对称父密钥加载子密钥,这两个规则接收父密钥句柄、子密钥的公开区域和密钥包,读取父密钥句柄对应的密钥信息,然后为子密钥生成句柄,存储子密钥句柄对应的密钥信息,并发送该句柄.两个规则的区别在于父密钥句柄对应的密钥类型和子密钥密钥包的加密方式不同:规则4中为对称密钥和对称加密,规则5中为非对称密钥和非对称加密.规则4中动作TCMLoadKey(A,‘SMS4’,k,snpk)表示TCM A以SMS4密钥snpk为父密钥加载了密钥k;类似地,规则5中动作TCMLoadKey(A,‘SM4’,k,anpk)表示TCM A以SM2密钥anpk为父密钥加载了密钥k.

规则6~规则8建模源TCM的行为.规则6描述源TCM初始化,该规则生成源TCM的tcmProof、存储密钥、存储密钥句柄和可迁移密钥,发送可迁移密钥的公开区域、存储密钥加密的可迁移密钥的密钥包和存储密钥句柄,并存储tcmProof值和存储密钥句柄对应的密钥信息.规则7描述源TCM授权保护密钥,该规则接收迁移模式、目标TCM的PEK公钥和PEK证书,查找TTP的公钥证书和源TCM的tcmProof值,计算迁移授权数据,并发送该迁移授权数据.动作$ Eq\left( {verify(cert,\langle B,pk(pek)\rangle ,pk(pek)\rangle ,pk\left( {tk} \right)} \right),true)$描述源TCM所有者验证目标TCM的PEK和PEK证书,即,用TTP公钥pk(tk)验证证书cert是对身份标识B和PEK公钥pk(pek)的签名,该动作被用在安全属性中的迹公式 ${\alpha _{Eq}}: = \left( {\forall x\;y\;i.\;\;\;\;Eq\left( {x,y} \right)@i \Rightarrow x = y} \right) $中. ${\alpha _{Eq}} $过滤掉分析过程中包含Eq(x,y)且 $x \ne y $的迹,从而保证只有PEK证书验证成功,源TCM所有者才会授权该PEK为迁移保护密钥.规则8描述源TCM创建迁移数据,该规则接收被迁移密钥的父密钥句柄、迁移授权数据和被迁移密钥的密钥包,查找源TCM的tcmProof值和被迁移密钥的父密钥句柄对应的密钥信息,生成随机种子,计算迁移包,并发送该迁移包.动作TCMCreate MigratedBlob(A,B,k,pk(pek))表示TCM A以TCM B的pk(pek)为迁移保护密钥创建了密钥k的迁移包.

规则9~规则11建模目标TCM的行为.规则9描述目标TCM初始化,该规则生成目标TCM的EK、EK密钥句柄、SMK、SMK密钥句柄、对称存储密钥、对称存储密钥句柄、非对称存储密钥和非对称存储密钥句柄,发送上述4个句柄,产生PEK请求,并存储EK公钥和4个密钥句柄对应的密钥信息.规则10、规则11分别描述目标TCM将密钥迁移至对称和非对称密钥下,这两个规则接收目标TCM的PEK密钥句柄、被迁移密钥的新父密钥句柄和迁移包,查找上述两个句柄对应的密钥信息,计算新父密钥加密的被迁移密钥的密钥包,并发送该密钥包.两个规则的区别在于,新父密钥句柄对应的密钥类型和被迁移密钥密钥包的加密方式不同:规则10中是对称密钥和对称加密,规则11中是非对称密钥和非对称加密.规则10中动作TCMConvertMigratedBlob (B, ‘SMS4’,k,snpk)表示TCM B以SMS4密钥snpk为新父密钥转换了密钥k的迁移数据;类似地,规则11中动作TCMConvertMigratedBlob(B,‘SM2’,k,anpk)表示TCM B以SM2密钥anpk为新父密钥转换了密钥k的迁移数据.

4.2.2 安全属性验证

定理1(key migration correctness). ,其中,

定理1表示在假设${\alpha _{OT}}$和${\alpha _{Eq}}$成立的情况下,存在P1的执行满足φ₁和φ₂,即:在TTP仅初始化一次,并且只有目标TCM的PEK证书验证成功时,源TCM所有者才授权该PEK为迁移保护密钥的情况下,存在协议1的执行满足安全属性${\varphi _1}$和φ₂.安全属性φ₁表示存在TCM A在时间点i以TCM B的pk(pek)为迁移保护密钥创建密钥mk的迁移包,TCM B在i之后的时间点j以SMS4密钥npk为新父密钥转换了mk的迁移数据,并在j之后的时间点k以npk为父密钥加载了mk,且TCM A和TCM B为不同的TCM.安全属性φ₂表示存在TCM A在时间点i以TCM B的pk(pek)为迁移保护密钥创建密钥mk的迁移包,TCM B在i之后的时间点j以SM2密钥npk为新父密钥转换了mk的迁移数据,并在j之后的时间点k以npk为父密钥加载了mk,且TCM A和TCM B为不同的TCM.因此,定理1表明:存在协议1的执行满足源TCM迁出的密钥能够被迁移到目标TCM的对称(φ₁)和非对称(φ₂)密钥下,并且目标TCM能够用新父密钥加载被迁移的密钥.该定理用于验证协议1的正确性.

定理2(key migration security). ,其中,

$\begin{array}{l} {\varphi _3}: = \forall A\;B\;mk\;pek\;i.\quad \quad TCMCreateMigratedBlob(A,B,mk,pk(pek))@i \Rightarrow \neg (\exists \,j.\quad K(mk)@j),\\ {\varphi _4}: = \forall A\;type\;mk\;npk\;i.\quad TCMConvertMigratedBlob(A,type,mk,npk)@i \Rightarrow \neg (\exists \,j.\quad K(mk)@j). \end{array}$

定理2表示在假设${\alpha _{OT}}$和${\alpha _{Eq}}$成立的情况下,P1的所有执行都满足φ₃和φ₄.即:在TTP仅初始化1次,并且只有目标TCM的PEK证书验证成功时,源TCM所有者才授权该PEK为迁移保护密钥的情况下,协议1的所有执行都满足安全属性${\varphi _3}$和φ₄.安全属性φ₃表示TCM A在时间点i以TCM B的pk(pek)为迁移保护密钥创建密钥mk的迁移包,那么不存在时间点j,在该时间点mk被敌手获得.安全属性φ₄表示TCM A在时间点i以任意类型的密钥npk为新父密钥转换了mk的迁移数据,那么不存在时间点j,在该时间点mk被敌手获得.因此,定理2表明,协议1的所有执行都能够保证从源TCM迁出的密钥(φ₃)和迁移到目标TCM的密钥(φ₄)不会被敌手获得.该定理用于验证协议1能够保证源TCM迁出密钥和目标TCM迁入密钥的机密性,即,验证协议一能够保证密钥迁移的安全性.

以规则集合P1和定理1、定理2的安全属性编码为脚本作为Tamarin的输入,经过Tamarin验证得出如图 7所示的结果.图中第1行文字提示后续输出为Tamarin的验证结果,第2行文字表示验证的协议文件名为Tcm_Key_Migration_Protocol1.spthy,之后的4行输出即是协议安全属性的验证结果,其格式为:序号_安全属性名称(安全属性类型):安全属性验证结果(验证执行的步骤数).安全属性有两种类型:exists-trace表示该安全属性是可满足性断言,all-traces表示该安全属性是有效性断言.验证结果同样有两种:verified表示该安全属性验证为真,falsified-found trace表示该安全属性验证为假,Tamarin发现不满足该安全属性的迹.图中的4行输出分别对应定理1、定理2中φ₁~φ₄的验证结果.与协议1预期的安全属性一致,φ₁~φ₃验证为真,φ₄验证为假.Tamarin给出的对安全属性φ₄的攻击流程与图 3中的第2种攻击相同,即:由于目标TCM不能认证迁移数据的来源,使敌手能将其已知的密钥迁移到目标TCM中.

4.3 协议2分析

文献^[15]给出了一个可证明安全性的SM2密钥协商协议,本节在此基础上证明协议2的安全属性.限于篇幅,本节将重点介绍第4.2节中未涉及的内容.而对于协议2与协议1在分析过程中的共同之处,只做简要说明.

4.3.1 协议描述

描述协议2的规则集合为P2.P2是以下两个集合的并集:图 6中规则1~规则5和规则7组成的集合;图 8所示的规则集合.

下面简介图 8中各规则的语义.

规则1、规则2建模源TCM的行为.规则1描述源TCM初始化,该规则生成源TCM的tcmProof、EK、EK密钥句柄、SMK、SMK密钥句柄、存储密钥和存储密钥句柄,发送上述3个句柄,存储tcmProof值,产生PEK请求,并存储EK公钥和3个密钥句柄对应的密钥信息.规则2描述源TCM创建迁移数据,该规则接收被迁移密钥的父密钥句柄、迁移授权数据、源TCM的PEK密钥句柄、目标TCM的临时密钥公钥和被迁移密钥的密钥包,查找源TCM的tcmProof值和上述两个密钥句柄对应的密钥信息,生成源TCM的临时密钥私钥,计算迁移包,发送源TCM的临时密钥公钥和该迁移包.动作TCMCreateMigratedBlob(A,B,k,pk(bpek))表示TCM A以TCM B的pk(pek)为迁移保护密钥创建了密钥k的迁移包.

规则3~规则6建模目标TCM的行为.规则3描述目标TCM创建协商会话,该规则生成目标TCM的临时密钥私钥和密钥协商会话句柄,发送目标TCM的临时密钥公钥和该密钥协商会话句柄,并将生成的临时密钥对存储在该密钥协商会话句柄对应的会话信息中.规则4、规则5分别描述目标TCM迁移密钥至对称和非对称密钥下,这两个规则接收目标TCM的PEK密钥句柄、目标TCM的密钥协商会话句柄、源TCM的PEK公钥、源TCM的临时密钥公钥、被迁移密钥的新父密钥句柄、被迁移密钥的迁移包和源TCM的PEK证书,查找TTP的公钥证书和上述3个句柄对应的信息,计算新父密钥加密的被迁移密钥的密钥包,发送该密钥包,并重新存储该密钥协商会话句柄对应的会话信息.与图 6中的规则7类似,这两个规则中的动作Eq描述目标TCM所有者验证源TCM的PEK和PEK证书,被用在安全属性中的迹公式 $ {\alpha _{Eq}}$中,从而保证只有PEK证书验证成功,目标TCM所有者才会允许迁移数据转换至目标TCM的存储保护体系中.两个规则的区别在于新父密钥句柄对应的密钥类型和被迁移密钥的密钥包加密方式不同:规则4中为对称密钥和对称加密,规则5中为非对称密钥和非对称加密.规则4中动作TCMConvertMigratedBlob(B,‘SMS4’,k,snpk,y)表示TCM B以SMS4密钥snpk为新父密钥y为临时密钥私钥转换了密钥k的迁移数据;类似地,规则5中动作TCMConvertMigratedBlob(B,‘SM2’, k,anpk,y)表示TCM B以SM2密钥anpk为新父密钥y为临时密钥私钥转换了密钥k的迁移数据.规则6描述目标TCM释放协商会话,该规则接收目标TCM的密钥协商会话句柄,查找该句柄对应的会话信息,释放该句柄指向的密钥协商会话,并发送表示密钥协商会话释放成功的信息.动作TCMReleaseExchangeSession(y)表示目标TCM释放了临时密钥私钥y对应的密钥协商会话.

规则7建模敌手行为,该规则接收TCM的PEK证书,查找TTP的公钥证书,发送PEK私钥.动作RevealLtk(A)表示敌手获得了TCM A的PEK私钥.该规则允许敌手获得SM2密钥协商协议两个参与方的长期密钥,也就是源TCM和目标TCM的PEK私钥.

4.3.2 安全属性验证

除了验证协议2满足第4.2节中的安全属性外,还要验证其满足前向安全性.

定理3(perfectforward secrecy). ,其中,

定理3表示在假设${\alpha _{OT}}$和${\alpha _{Eq}}$成立的情况下,P2的所有执行都满足φ₅,即:在以下3个条件成立的情况下,协议1的所有执行都满足安全属性${\varphi _5}$:(1) TTP仅初始化1次;(2) 只有目标TCM的PEK证书验证成功时,源TCM所有者才授权该PEK为迁移保护密钥;(3) 只有源TCM的PEK证书验证成功时,目标TCM所有者才会允许迁移数据转换至目标TCM的存储保护体系中,协议2的所有执行都满足安全属性${\varphi _5}$.安全属性φ₅表示TCM A在时间点i以TCM B的pk(pek)为迁移保护密钥创建密钥mk的迁移包,TCM B在i之后的时间点j以任意类型的密钥npk为新父密钥y为临时密钥私钥转换了mk的迁移数据,并在j之后的时间点k释放了临时密钥私钥y对应的密钥协商会话,且TCM A和TCM B为不同的TCM,那么即使敌手在k之后的时间点获得了TCM A和TCM B的PEK私钥,也不存在时间点t,在该时间点mk被敌手获得.因此,定理3表明:协议2执行成功后,即使敌手获得源TCM和目标TCM的长期密钥,也不能得到之前迁移的密钥.该定理用于验证协议2满足前向安全性.

将规则集合P2和定理1~定理3的安全属性编码为脚本作为Tamarin的输入,经过Tamarin验证得出如图 9所示的结果.

与图 7中验证结果的输出形式类似,图中第1行文字提示后续输出为Tamarin的验证结果,第2行文字表示验证的协议文件名为Tcm_Key_Migration_Protocol2.spthy,之后的5行输出是协议安全属性的验证结果.图中的5行输出分别对应定理1~定理3中φ₁~φ₅的验证结果.与协议2预期的安全属性一致,φ₁~φ₅均验证为真.

5 相关工作

在可信安全芯片密钥迁移方面,研究人员对TPM密钥迁移机制的研究较多,但目前还没有TCM密钥迁移机制的相关研究成果.

在TPMv1.2芯片密钥迁移机制的分析方面,文献^[16]用一阶逻辑语言建立TPM API的形式化模型对TPM API进行了全面的逻辑推理分析,分析结果给出了针对TPM密钥迁移和授权机制的多种攻击,其中,对密钥迁移机制的攻击使TPM的所有者可以破解TPM内部存储的其他用户拥有的密钥使用授权信息.文献^[17]应用π演算对TPM进行形式化建模,并使用自动定理证明工具ProVerif验证其安全属性.作者分析了TPM CMK (certifiable migratable key)的RESTRICT_MIGRATE迁移模式,分析结果表明:若作为第三方的迁移权威(migration authority,简称MA)用软件处理迁移数据,则敌手能获得被迁移密钥的私钥.作者建议TPM规范强制要求MA使用TPM代替软件处理迁移数据,但是TPM规范对该迁移模式的设计思想是:迁移密钥的保护方式由MA决定,即MA可以制定自己的安全策略决定对迁移密钥的保护强度,因此,强制MA使用TPM芯片处理迁移数据会违背该原则.文献^[18]对TPM可迁移密钥的安全性进行了分析,指出TPM提供密钥迁移机制的同时,降低了可迁移密钥的安全保护强度,敌手能够利用TPM的密钥迁移类接口和密钥加载接口破坏TPM可迁移密钥的安全性.文中给出的针对密钥迁移类接口的攻击与本文图 3中的两种攻击类似,导致该类攻击的原因同样是由于缺少源TPM和目标TPM间的身份认证.但是由于TPM缺少具有身份标识作用的加解密密钥,因此目前该类攻击在TPM密钥迁移过程中难以避免.

2012年,可信计算组织发布了TPM2.0规范^[3],虽然目前还没有符合该规范的芯片产品,但是学术界已经对该规范展开了研究.在TPM2.0规范中,密钥迁移被包含在密钥复制机制中.文献^[19]建立了TPM2.0保护存储API的抽象模型,并利用类型系统证明了TPM2.0保护存储的安全性.证明结果表明,TPM2.0保护存储中的密钥复制类接口是安全的.文献^[20]对TPM2.0密钥管理API的安全性进行了形式化分析,证明了密钥存储和使用类接口能够保证TPM不可迁移密钥的安全性,并发现了针对密钥复制类接口的两种攻击.作者提出了该类接口的改进方案,并证明了利用改进的接口实施密钥复制能够保证被复制密钥的安全性.

6 结束语

本文首次对TCM密钥迁移协议进行了研究和分析,指出现有以新父密钥为迁移保护密钥的密钥迁移协议应用到TCM时存在的两个问题:密钥不能被迁移到目标TCM的对称存储密钥下;参与协议的两个TCM间缺乏相互认证,敌手能够利用该安全缺陷获得源TCM的被迁移密钥和将其控制的密钥迁移到目标TCM中.针对上述问题,本文提出两个新的密钥迁移协议:协议1遵循TCM接口规范,允许被迁移密钥以目标TCM上任意类型的存储密钥为新父密钥,并解决了源TCM对目标TCM的身份认证问题;协议2需要简单修改TCM接口,不仅能完全解决上述两个问题,而且具有前向安全性.本文对上述两个协议进行了形式化分析,论证了协议的正确性并验证了协议满足预期的安全属性.

本文为TCM密钥迁移机制提供了新的思路,有助于下一代TCM芯片的设计.目前,很多研究工作都针对TPM芯片展开,而我国具有自主知识产权的TCM芯片具有许多不同于TPM的安全特性,同样是一个值得深入研究的对象.我们的下一步工作是研究TCM授权协议、TCM对称密钥管理和其他各种安全机制是否安全、是否存在问题,以完善和改进TCM.