安全协议形式化验证方法综述  

Overview on Security Protocol Formal Verification Methods

作　　者：项俊龙[1] 陈传峰[1] 

机构地区：[1]福州大学物理与信息工程学院,福建福州350002

出　　处：《信息安全与通信保密》2013年第5期52-54,共3页Information Security and Communications Privacy

摘　　要：安全协议作为确保网络安全的关键技术,其安全性直接决定了网络的安全性能。然而安全协议设计与分析存在着诸多困难,目前采用的主要方法是形式化方法,主要分为模态逻辑的方法、模型检测的方法、定理证明方法3种。这3种方法特性各不相同,试用范围也有所区别,而且这些方法或多或少都存在着一定的缺陷。Applied pi演算是一种专门针对安全协议设计的理论成熟的形式化方法,它的出现为安全协议的分析带来了全新的思路。Security protocol, as a critical technology in ensuring network security, directly determines safety performance of the network. However, there exist many difficulties in the design and analysis of security protocols. The formal methods are the main methods, including modal logic, model checking and theorem proving methods. These methods are different in characteristics and trial ranges, and also have, more or less, their own defects. The Applied pi calculus is designed for analysis of the security protocol, and its appearance brings about a new idea for the analysis of security protocols.

关 键 词：安全协议 形式化方法 PI演算 APPLIED PI演算 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]