摘要
在安全协议的形式化分析研究当中,如何在统一的框架下对更多的安全属性进行分析和验证是一个亟待解决的重要问题。为了解决这个问题,提出了用匹配关系来形式化地描述各种安全属性的统一框架,建立了语法和语义系统,并证明了该框架的可靠性和完备性。在此基础上,将知识推理和进程演算结合起来,提出了一个安全协议形式化分析的一般模型。最后,给出了一些安全属性的研究实例,并指出了进一步完善此模型的研究方向。
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.
出处
《计算机应用研究》
CSCD
北大核心
2011年第4期1460-1464,共5页
Application Research of Computers
基金
国家"863"计划863-104-03-01课题资助项目
关键词
进程演算
知识推理
安全属性
形式化分析
安全协议
process calculus
knowledge derivation
security properties
formal analysis
security protocol
