自动信任协商安全性的形式化分析与验证

摘要：

为了对自动信任协商(ATN)的安全性进行形式化分析与验证,文中借鉴安全协议的形式化分析方法,提出一种用进程代数Appliedπ演算对ATN建模并验证其安全性的方法.该方法将ATN形式化为两个协商者进程的并发执行,其中一个协商者的进程就是对其拥有的证书及授权策略的静态建模；ATN的安全性被定义为Appliedπ演算的观察等价性,从而使该方法不仅能检查授权策略执行的安全性,而且能对协商者的隐私安全进行验证.借助安全协议的自动分析工具ProVefif,文中实现了对ATN安全性的自动分析.实验结果表明,用Applied π演算形式化及验证ATN的安全性是可行的,安全性验证可自动完成,并且效率较高.

关键词：自动信任协商、安全性、形式化分析、Applied π演算、观察等价、ProVerif

所属期刊栏目：41

分类号：TP31(计算技术、计算机技术)

资助基金：广东省自然科学基金团队项目9351064101000003;广东省高等学校珠江学者岗位计划资助项目2011;广东省高等学校高层次人才项目2012;广州市科技计划项目2011J4300028

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

页数：共7页

页码：77-82,94