北京交通大学学报2012，Vol.36Issue(2)：8-15,8.
SSH可信信道安全属性的形式化验证
Formal verification of SSH-based trusted channels
摘要
Abstract
A trusted channel is a secure one that is cryptographically bound with the endpoint's platform state information. The existing research about establishing trusted channels did not analyze this property theoretically. This paper firstly proposes a SSH-based trusted channel protocol. Then we formally analyze its security properties by applying model checker NuSMV. Based on the analysis results of the counter-example, this paper proposes a robust SSH-based trusted channel protocol. The methods of modeling and verification can be applied to verify the security property of the trusted channel protocols based on other secure channel techniques.关键词
SSH/TCG远程证明/可信信道/模型检测/NuSMVKey words
SSH/ TCG remote attestation/ trusted channel/ model checking/ NuSMV分类
信息技术与安全科学引用本文复制引用
常晓林,秦英,邢彬,左向晖..SSH可信信道安全属性的形式化验证[J].北京交通大学学报,2012,36(2):8-15,8.基金项目
中央高校基本科研业务费专项基金资助(2009JBM017 （）
2010YJS024) （）
