Journal of South China University of Technology (Natural Science Edition) ›› 2013, Vol. 41 ›› Issue (1): 77-82,94.doi: 10.3969/j.issn.1000-565X.2013.01.012

• Computer Science & Technology • Previous Articles     Next Articles

Formal Analysis and Verification of Security for AutomatedTrust Negotiation

Liu Xin-xin Tang Shao-hua   

  1. School of Computer Science and Engineering, South China University of Technology, Guangzhou 510640, Guangdong, China
  • Received:2012-04-25 Revised:2012-08-03 Online:2013-01-25 Published:2012-12-03
  • Contact: 唐韶华(1970-),男,教授,博士生导师,主要从事信息安全研究. E-mail:csshtang@scut.edu.cn
  • About author:刘欣欣(1977-),女,在职博士生,讲师,主要从事信息安全研究.E-mail:csliuxx@scut.edu.cn
  • Supported by:

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

PDF

912

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