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

摘要

在安全协议的形式化分析研究当中,如何在统一的框架下对更多的安全属性进行分析和验证是一个亟待解决的重要问题.为了解决这个问题,提出了用匹配关系来形式化地描述各种安全属性的统一框架,建立了语法和语义系统,并证明了该框架的可靠性和完备性.在此基础上,将知识推理和进程演算结合起来,提出了一个安全协议形式化分析的一般模型.最后,给出了一些安全属性的研究实例,并指出了进一步完善此模型的研究方向.%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.