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

作     者：刘欣欣 唐韶华 Liu Xin-xin;Tang Shao-hua

作者机构：华南理工大学计算机科学与工程学院广东广州510640 

出 版 物：《华南理工大学学报（自然科学版）》 (Journal of South China University of Technology(Natural Science Edition))

年 卷 期：2013年第41卷第1期

页      面：77-82,94页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

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

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