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

On Unifying the Formal Method to Depict the Security Properties

作　　者：谢鸿波[1,2] 吴远成[1] 周明天[1] 

机构地区：[1]电子科技大学计算机科学与工程学院,成都610054 [2]重庆通信学院三系数据链教研室,重庆400035

出　　处：《计算机科学》2008年第9期172-174,186,共4页Computer Science

基　　金：国家863项目863-104-03-01课题资助

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

关 键 词：协议分析 形式化分析方法 安全属性 

分 类 号：TP311.134[自动化与计算机技术—计算机软件与理论] TP316.89[自动化与计算机技术—计算机科学与技术]