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

Abstract:

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.

Key words: automated trust negotiation, security, formal analysis, applied π calculus, observational equivalence, ProVerif