A Framework for Automatic Security Proof of Public-Key Cryptography in Computational Model

In this paper we present a new framework for automatically proving the security of public-key cryptographic schemes in 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 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 ElGamal encryption.