| 基于应用π演算的可信平台模块的安全性形式化分析 |
| |
| 引用本文： | 徐士伟,张焕国.基于应用π演算的可信平台模块的安全性形式化分析[J].计算机研究与发展,2011,48(8). |
| |
| 作者姓名： | 徐士伟 张焕国 |
| |
| 作者单位： | 1. 武汉大学计算机学院 武汉430072;空天信息安全与可信计算教育部重点实验室(武汉大学) 武汉430072;伯明翰大学计算机科学学院 英国伯明翰B15 2TT
2. 武汉大学计算机学院 武汉430072;空天信息安全与可信计算教育部重点实验室(武汉大学) 武汉430072;软件工程国家重点实验室(武汉大学) 武汉430072 |
| |
| 基金项目： | 国家自然科学基金项目(91018008,60970115,60970116) |
| |
| 摘 要： | 可信平台模块(trusted platform module,TPM)是信息安全领域热点研究方向可信计算的关键部件,其安全性直接影响整个可信计算平台的安全性,需要对其进行安全性验证.针对已有工作对TPM规范中多类安全性问题进行形式化建模与验证过程中所存在的不足,从分析TPM和使用者的交互过程出发,使用应用π演算对TPM进行形式化建模,把TPM规范中定义的各实体行为特性抽象成为进程的并发安全性问题,在讨论并发进程中机密性、认证性和弱机密性的基础上,对交互模型进行安全性论证,提出并使用自动定理证明工具验证了对应安全属性的改进方案.
|
| 关 键 词： | 可信计算 可信平台模块 应用π演算 并发进程 安全性分析 |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
