一种基于π^t演算的安全协议建模方法  

A New Security Protocol Modeling Approach Based on π^t Calculus

作　　者：韩进[1,2] 蔡圣闻[1,2] 王崇峻[1,2] 赖海光[1,3] 谢俊元[1,2] 

机构地区：[1]南京大学计算机软件新技术国家重点实验室,南京210093 [2]南京大学计算机科学与技术系,南京210093 [3]解放军理工大学指挥自动化学院计算机系,南京210007

出　　处：《计算机研究与发展》2010年第4期613-620,共8页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60503021;60721002;60875038);江苏省高新技术计划基金项目(BG2007038)

摘　　要：安全协议模型是安全协议分析与验证的基础,现有的建模方法中存在着一些缺点,如:建模复杂、重用性差等.为此提出了一种类型化的π演算:πt演算,并给出了相应类型推理规则和求值规则,πt演算的安全性也得到了证明.πt演算可以对安全协议、协议攻击者进行形式化建模.基于πt演算的安全协议模型及其建模过程使用NRL协议为例做出了说明.同时给出了攻击者模型,并证明了基于πt演算的安全协议攻击者模型与D-Y攻击者模型在行动能力上是一致的.这保证了基于πt演算的安全协议模型的验证结果的正确性.基于πt演算的建模方法能在协议数据语义、协议参与者知识方面实现细致的描述.与同类方法相比,该方法可提供多种分析支持,具有更好的易用性、重用性.分析表明,该方法可以在建模中发现一定的安全协议漏洞.The security protocol model is the basis of the security protocol analysis and verification. Existing modeling methods have some shortcomings, such as high complexity, bad reusability, and so on. A typed π calculus π^t calculus is presented in this paper, and its type rules and evaluation rules are also given. It is proved that ret calculus is a safely typed system. π^t calculus can be used to build formal models of security protocols and their attackers. NRL protocol is taken for an example to show how to build a security protocol model based on π^t calculus. The attacker model for a security protocol is also presented in this paper. The action ability which the attacker model based on π^t calculus has is proved the same to the D-Y attacker model. So the correctness of the results which come from verifying the security protocol models based on π^t calculus is promised. The security protocol modeling approach based on π^t calculus can give more detailed description of the semantics of protocol data and the knowledge of participators. Compared with other kinds of methods, this method has better usability and high reusability and can provide more analysis support. The analysis result shows that the method can detect flaws of a security protocol in its modeling process.

关 键 词：安全协议模型 πt演算 安全协议验证 类型化系统 形式化方法 

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