tcm密钥迁移协议设计及形式化分析

为增强tcm芯片间密钥的互操作性,tcm提供了密钥迁移相关命令接口,允许用户设计密钥迁移协议以实现芯片间密钥的共享.通常,tcm密钥迁移协议以目标tcm上的新父密钥作为迁移保护密钥.研究发现,该协议存在两个问题:对称密钥不能作为被迁移密钥的新父密钥,违背了tcm的初始设计思想;缺少交互双方tcm的相互认证,导致源tcm的被迁移密钥可以被外部敌手获得,并且敌手可以将其控制的密钥迁移到目标tcm中.针对上述问题,提出两个新的密钥迁移协议:协议1遵循tcm目前的接口规范,以目标tcm的pek(platformencryptionkey)作为迁移保护密钥,能够认证目标tcm,并允许对称密钥作为新父密钥;协议2简单改动了tcm接口,以源tcm和目标tcm进行sm2密钥协商,得到的会话密钥作为迁移保护密钥,解决了上述两个问题,并且获得了前向安全属性.最后,使用形式化分析方法对上述协议进行安全性分析,分析结果显示,协议满足正确性和预期的安全属性.