SSH可信信道安全属性的形式化验证

Formal verification of SSH-based trusted channels

可信信道是一个与终端的系统平台状态信息安全绑定的安全信道.现有的关于可信信道的研究工作都没有从理论上对所设计的可信信道的安全属性进行分析.本文首先提出一个基于SSH安全信道协议的可信信道协议,然后利用形式化模型检测器NuSMV分析该协议的安全属性,最后基于检测器执行轨迹所构成的反例,提出了一个强壮的SSH可信信道协议.本文提出的建模和验证方法具有通用性,可用于分析其他基于安全信道协议的可信信道协议的安全属性.

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.