摘要
可信平台模块(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.
出处
《计算机研究与发展》
EI
CSCD
北大核心
2011年第8期1421-1429,共9页
Journal of Computer Research and Development
基金
国家自然科学基金项目(91018008
60970115
60970116)
关键词
可信计算
可信平台模块
应用π演算
并发进程
安全性分析
Key words trusted computing
trusted platform module （TPM）
applied π calculus
concurrentprocesses
security analysis
