基于应用π演算的可信平台模块的安全性形式化分析  

Formal Security Analysis on Trusted Platform Module Based on Applied π Calculus

作　　者：徐士伟[1,2,3] 张焕国[1,2,4] 

机构地区：[1]武汉大学计算机学院,武汉430072 [2]空天信息安全与可信计算教育部重点实验室(武汉大学),武汉430072 [3]伯明翰大学计算机科学学院 [4]软件工程国家重点实验室(武汉大学),武汉430072

出　　处：《计算机研究与发展》2011年第8期1421-1429,共9页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(91018008;60970115;60970116)

摘　　要：可信平台模块(trusted platform module,TPM)是信息安全领域热点研究方向可信计算的关键部件,其安全性直接影响整个可信计算平台的安全性,需要对其进行安全性验证.针对已有工作对TPM规范中多类安全性问题进行形式化建模与验证过程中所存在的不足,从分析TPM和使用者的交互过程出发,使用应用π演算对TPM进行形式化建模,把TPM规范中定义的各实体行为特性抽象成为进程的并发安全性问题,在讨论并发进程中机密性、认证性和弱机密性的基础上,对交互模型进行安全性论证,提出并使用自动定理证明工具验证了对应安全属性的改进方案.Trusted computing is a popular paradigm to ename Computers, security than is possible in software alone. The core hardware component, named trusted platform module （TPM）, is designed to achieve this goal. As there are many relevant products on the market and some attacks have already been found, it is very necessary to carry out the security analysis of TPM. However, because TPM is a complex security component whose specification is too long to be completely covered, the existing work hasn＇t formally or fully analyzed the issues about the various security properties. An applied π calculus model of the interactive processes between TPM and its user is proposed as a solid foundation for discussing the various security properties. Based on the formal model, the secrecy, authentication and weak secrecy problems of TPM are identified and formalized, some known attacks are rediscovered and some new attacks are found via a formal way rather than descriptions in natural language. Furthermore, the fixing proposals for the corresponding security vulnerabilities are presented and verified. In order to make the analysis and verification more accurate and efficient, the automatic theorem proving tool is also used during the analysis and verification.

关 键 词：可信计算 可信平台模块 应用π演算 并发进程 安全性分析 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]