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

Formal Analysis and Verification of Security for Automated Trust Negotiation

作　　者：刘欣欣[1] 唐韶华[1] 

机构地区：[1]华南理工大学计算机科学与工程学院,广东广州510640

出　　处：《华南理工大学学报（自然科学版）》2013年第1期77-82,94,共7页Journal of South China University of Technology(Natural Science Edition)

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

摘　　要：为了对自动信任协商(ATN)的安全性进行形式化分析与验证,文中借鉴安全协议的形式化分析方法,提出一种用进程代数Applied π演算对ATN建模并验证其安全性的方法.该方法将ATN形式化为两个协商者进程的并发执行,其中一个协商者的进程就是对其拥有的证书及授权策略的静态建模;ATN的安全性被定义为Applied π演算的观察等价性,从而使该方法不仅能检查授权策略执行的安全性,而且能对协商者的隐私安全进行验证.借助安全协议的自动分析工具ProVerif,文中实现了对ATN安全性的自动分析.实验结果表明,用Applied π演算形式化及验证ATN的安全性是可行的,安全性验证可自动完成,并且效率较高.In order to implement the formal analysis and verification of the security for automated trust negotiation （ATN） , this paper takes the formal analysis methods of security protocols as references and proposes a novel approach to ATN modeling and security verification with the help of the process algebra applied n calculus. In this ap- proach, ATN is formalized as the parallel composition of two processes corresponding to two negotiators, and the process of a negotiator is the static modeling of its certificates and authorization policies. The ATN security is defined as the observational equivalence of the applied n calculus so as to verify not only the security of the authorization policy enforcement but also the privacy of negotiators. With the help of the automatic protocol analyzer ProVerif, the security of ATN is automatically analyzed. Experimental results show that the proposed approach helps to implement automatic security verification with high feasibility and efficiency.

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

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]