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

摘要：

安全协议模型是安全协议分析与验证的基础,现有的建模方法中存在着一些缺点,如:建模复杂、重用性差等.为此提出了一种类型化的π演算:πt演算,并给出了相应类型推理规则和求值规则,πt演算的安全性也得到了证明.πt演算可以对安全协议、协议攻击者进行形式化建模.基于πt演算的安全协议模型及其建模过程使用NRL协议为例做出了说明.同时给出了攻击者模型,并证明了基于πt演算的安全协议攻击者模型与D-Y攻击者模型在行动能力上是一致的.这保证了基于πt演算的安全协议模型的验证结果的正确性.基于πt演算的建模方法能在协议数据语义、协议参与者知识方面实现细致的描述.与同类方法相比,该方法可提供多种分析支持,具有更好的易用性、重用性.分析表明,该方法可以在建模中发现一定的安全协议漏洞.

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

所属期刊栏目：47

分类号：TP309.7(计算技术、计算机技术)

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

在线出版日期：2010-06-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：613-620