动态信任根协议的自动化验证（长版本）
密码学与安全
2018-07-24 v2
摘要
基于动态信任根（通常依赖如 TPM 等受保护硬件）的安全协议自动验证涉及若干挑战，我们在本文中予以解决。我们在 ProVerif 接受的经典进程演算中建模可信计算平台（包括 CPU、TPM、OS 及其他必要组件）的语义及相关协议。作为形式化工作的一部分，我们引入了新的等式理论来表示 TPM 特定平台状态和动态加载程序。由于特别是由 TPM 寄存器无界扩展产生的搜索空间，此类广泛特征的正式模型无法被 ProVerif 直接处理。在此背景下，我们引入了 TPM 进程的转换，简化了自动验证的搜索空间结构，同时保留感兴趣的安全属性。这允许在我们得到的模型上运行 ProVerif，从而可以自动推导动态信任根上下文中运行协议的安全保证。
引用
@article{arxiv.1701.08676,
title = {Automated verification of dynamic root of trust protocols (long version)},
author = {Sergiu Bursuc and Christian Johansen and Shiwei Xu},
journal= {arXiv preprint arXiv:1701.08676},
year = {2018}
}
备注
27 pages with Appendix