TY - GEN
T1 - Verifying anonymous credential systems in applied Pi calculus
AU - Li, Xiangxi
AU - Zhang, Yu
AU - Deng, Yuxin
PY - 2009
Y1 - 2009
N2 - Anonymous credentials are widely used to certify properties of a credential owner or to support the owner to demand valuable services, while hiding the user's 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.
AB - Anonymous credentials are widely used to certify properties of a credential owner or to support the owner to demand valuable services, while hiding the user's 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.
UR - https://www.scopus.com/pages/publications/71549173414
U2 - 10.1007/978-3-642-10433-6_14
DO - 10.1007/978-3-642-10433-6_14
M3 - 会议稿件
AN - SCOPUS:71549173414
SN - 3642104320
SN - 9783642104329
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 209
EP - 225
BT - Cryptology and Network Security - 8th International Conference, CANS 2009, Proceedings
T2 - 8th International Conference on Cryptology and Network Security, CANS 2009
Y2 - 12 December 2009 through 14 December 2009
ER -