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

来源：软件学报杂志2015年第9期北京时间：

作者：张倩颖,冯登国,赵世军

单位：张倩颖，中国科学院 软件研究所 可信计算与信息保障实验室, 北京 100190;首都师范大学 信息工程学院, 北京 10004811,冯登国，中国科学院 软件研究所 可信计算与信息保障实验室, 北京 10019002,赵世军，中国科学院 软件研究所 可信计算与信息保障实验室, 北京 10019003

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

关键词：可信计算;可信密码模块;密钥迁移;协议设计;形式化分析

基金资助：国家自然科学基金(91118006, 61202414); 国家重点基础研究发展计划(973)(2013CB338003)