统一的安全属性形式化描述方法的研究

On Unifying the Formal Method to Depict the Security Properties

安全属性的基于特定分析方法和限于特定属性的形式化描述严重影响了安全协议形式化分析方法的有效性和适用性。为解决这个问题,本文提出了一种统一的形式化描述方法,即通过属性动作之间的匹配关系来表达协议的安全属性。用这种方法详细分析了认证属性、保密属性以及公平性属性的形式化表达。通过比较分析,该方法与其他方法相比,具有准确、简洁和扩展性强的特点,在总体上优于其他方法。

The formal expression of security properties based on special analysis methods and used to special properties has largely affected the validity and applicability of the formal security protocol analysis. In order to solve this problem, a unifying method based on trace is been formally presented. In this method, the security properties are expressed as the match relations between property actions. This method can be used to express most kinds of security properties. As an example, it has been used to analyse the formal express of the authentication, secret, and fairness properties. Compared with other methods, this method is simpler, more expressive and has great expansibility.