一个基于模态逻辑的安全协议度量方法

为将量化分析方法引入安全协议分析中，以模态逻辑方法为基础定义了协议度量方法，并形式化地给出度量协议内容对协议安全目标满足度的参数和方法，同时在此基础上，进一步地给出了对安全协议冗余进行度量及化简的方法。应用该方法对实例协议进行分析，直接描述各协议内容的贡献度，显示冗余内容对目标实现的无效作用，从而可以安全化简。量化分析在安全协议形式化分析中的应用是本方法的主要特点，它具有模态逻辑方法的优点及缺陷。

A Modal Logic-Based Measurement Method of Security Protocol

In order to introduce the quantitatively analytical method into security protocol analysis, a protocol measurement method based on modal logic was defined. This method formally specifies the parameters and approaches to measure the satisfaction of security goals of the protocol contents. On this basis, approaches of mea- suring protocol redundancy and corresponding simplification were then put forward. The method was finally applied to analyze a sample protocol, describe the contribution of each protocol content and present the inefficacy of redundancy factors to protocol targets, thus achieving the safe simplification. The method is possessed of a main feature of applying quantitative analysis to the formal analysis of security protocol, and of the advantages and limitations of modal logic methods.