一种基于πt演算的安全协议建模方法
安全协议建模是安全协议分析与验证的基础,针对目前安全协议建模方法中存在的一些缺点,如建模复杂、重用性差等,本文建立了类型化的π演算,即πt演算,并基于该演算提出了一种新的安全协议建模方法。在πt演算中,采用复杂数据类型描述协议数据,并定义了相应类型推理规则和求值规则。文中给出了基于πt演算的安全协议模型,即攻击者模型和引入攻击者后的安全协议模型。依据数据类型的定义和求值规则,本文的建模方法在建模中即可以发现一定的安全协议漏洞。分析表明,基于πt演算的建模方法可以在协议数据语义、协议知识方面实现细致的描述,能够提供多种分析支持,易于建模,且协议模型具有良好的重用性。
安全协议模型 πt演算 安全协议验证 类型化系统
韩进 谢俊元
南京大学计算机软件新技术国家重点实验室 南京 210093
国内会议
西安
中文
520
2008-09-25（万方平台首次上网日期，不代表论文的发表时间）