安全属性形式化描述统一框架及其分析方法研究  

Study of unified framework of security properties and their analysis method

作　　者：谢鸿波[1,2] 谭兴烈 周明天[1] 

机构地区：[1]电子科技大学计算机科学与工程学院,成都610054 [2]重庆通信学院数据链教研室,重庆400035 [3]中国电子工业集团第30研究所,成都610041

出　　处：《计算机应用研究》2011年第4期1460-1464,共5页Application Research of Computers

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

摘　　要：在安全协议的形式化分析研究当中,如何在统一的框架下对更多的安全属性进行分析和验证是一个亟待解决的重要问题。为了解决这个问题,提出了用匹配关系来形式化地描述各种安全属性的统一框架,建立了语法和语义系统,并证明了该框架的可靠性和完备性。在此基础上,将知识推理和进程演算结合起来,提出了一个安全协议形式化分析的一般模型。最后,给出了一些安全属性的研究实例,并指出了进一步完善此模型的研究方向。In the study of the formal analysis of security protocols,it is desiderated to analysis more security properties under a unified framework.This paper presented a unified framework to formally depiction the security properties based on matching relations.Built up the syntax and the corresponding semantic of this unified framework,and also verified its soundness and completeness.Based on this framework,combining the process calculus with knowledge derivation,presented a generic model for the analysis of security protocols.Using this model and unified framework,analyzed some security properties as case study.Also pointed out some future directions at the end.

关 键 词：进程演算 知识推理 安全属性 形式化分析 安全协议 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]