A Framework for Automatically Proving the Security of Public-key Cryptographic Schemes in the Computational Model
In this paper we present a new framework for automatically proving the security of public-key cryptographic schemes in the computational model. The framework uses the sequence-of-games approach to construct security proof. A probabilistic polynomial-time process calculus is designed to describe the attack games and the game transformations are executed with the help of observational equivalence. The framework has been implemented as a automated prover in C language environment and tested on a series of examples including encryption and signature schemes. As an example, we illustrate the use of our framework with the proof of IND CPA security of EIGamal encryption.
public-key cryptographic scheme computational model automated security proving process calculus observational equivalence
Guang Yan Chen Jing-Ning Gu Chun-Xiang Zhu Yue-Fei
Zhengzhou Institute of Information Science and Technology Zhengzhou 450001, China
国际会议
成都
英文
1489-1493
2010-12-17（万方平台首次上网日期，不代表论文的发表时间）