安全协议形式化分析方法的融合性研究

The fusion research of approaches in formal analysis of security protocols

分析了BAN逻辑和串空间理论的特点与不足.为了弥补二者的不足,提出了一种融合两种理论的形式化分析方法.通过实例分析,证明该分析方法能够将BAN逻辑和串空间的优点互补综合,使安全协议的分析更可靠、稳定、高效.

Features and inadequacies of BAN logic and strand space are analysed in this paper.In order to compensate for inadequacies of the two approaches,a fusion formal analysis method is presented.Through a case study,it is demonstrated that this method can integrate the advantages of the BAN logic and strand space,and thus the analysis of security protocols become more reliable,stable and efficient.