一种基于协议分析的可信信道评估方法

目前，对可信信道的评估大多局限于经验的评测，缺乏理论支持，存在着极大的不确定性和不完备性．对此基于通用安全标准CC（Common Criteria）给出了具有一定通用性和可重用性的可信信道评估框架，在此评估框架中应用了形式化的验证方法，提出了把经验分析和形式化验证相结合的评估方法．同时在对SSH的评估中对Cord演算作了适应性的扩展．

An Evaluation Method for Trusted Channel Based on Protocol Analysis

Trusted channel provides various security services for information products in the environment of insecure networks. It has become a focused problem that whether the services of trusted channel provided by security products wholly satisfy the security function requirement. Now most evaluation methods are very uncertain and incomplete because they are almost empirical and without theoretical support. This paper proposes an evaluation framework based on the Common Criteria with generalization and reusability in some sense. The formal verification methods are applied in the framework, combined with empirical analysis. As an example, SSH protocol is verified by Cord calculus with type system, cryptographic function, and extended inference rules.