为了对自动信任协商(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 ap-proach to ATN modeling and security verification with the help of the process algebra applied π calculus. In this ap-proach, ATN is formalized as the parallel composition of two processes corresponding to two negotiators, and theprocess of a negotiator is the static modeling of its certificates and authorization policies. The ATN security is de-fined as the observational equivalence of the applied π calculus so as to verify not only the security of the authorizationpolicy 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 imple-ment automatic security verification with high feasibility and efficiency.