verifying anonymous credential systems in applied pi calculus

ISCAS OpenIR > 2009年期刊/会议论文

	verifying anonymous credential systems in applied pi calculus
	Li Xiangxi; Zhang Yu; Deng Yuxin
	2009
会议名称	8th International Conference on Cryptology and Network Security, CANS 2009
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	209-225
会议日期	40878
会议地点	Kanazawa, Japan
收录类别	ei,acm
出版地	Germany
ISSN	3029743
ISBN	3642104320
部门归属	(1) Department of Computer Science and Engineering, Shanghai Jiao Tong University, Shanghai, China; (2) Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
摘要	Anonymous credentials are widely used to certify properties of a credential owner or to support the owner to demand valuable services, while hiding the users identity at the same time. A credential system (a.k.a. pseudonym system) usually consists of multiple interactive procedures between users and organizations, including generating pseudonyms, issuing credentials and verifying credentials, which are required to meet various security properties. We propose a general symbolic model (based on the applied pi calculus) for anonymous credential systems and give formal definitions of a few important security properties, including pseudonym and credential unforgeability, credential safety, pseudonym untraceability. We specialize the general formalization and apply it to the verification of a concrete anonymous credential system proposed by Camenisch and Lysyanskaya. The analysis is done automatically with the tool ProVerif and several security properties have been verified. © 2009 Springer-Verlag.
关键词	Cryptography Internet
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/8536
专题	2009年期刊/会议论文
推荐引用方式 GB/T 7714	Li Xiangxi,Zhang Yu,Deng Yuxin. verifying anonymous credential systems in applied pi calculus[C]. Germany,2009:209-225.